A Case Study on Specifikation,Detection and Resolution of IN Feature Interactions with Estelle
(1994)
We present an approach for the treatment of Feature Interactions in Intelligent Networks. The approach is based on the formal description technique Estelle and consists of three steps. For the first step, a specification style supporting the integration of additional features into a basic service is introduced . As a result, feature integration is achieved by adding specification text, i.e . on a purely syntactical level. The second step is the detection of feature interactions resulting from the integration of additional features. A formal criterion is given that can be used for the automatic detection of a particular class of feature interactions. In the third step, previously detected feature interactions are resolved. An algorithm has been devised that allows the automatical incorporation of high-level design decisions into the formal specification. The presented approach is applied to the Basic Call Service and several supplementary interacting features.
Correctness and runtime efficiency are essential properties of software ingeneral and of high-speed protocols in particular. Establishing correctnessrequires the use of FDTs during protocol design, and to prove the protocolcode correct with respect to its formal specification. Another approach toboost confidence in the correctness of the implementation is to generateprotocol code automatically from the specification. However, the runtimeefficiency of this code is often insufficient. This has turned out to be amajor obstacle to the use of FDTs in practice.One of the FDTs currently applied to communication protocols is Es-telle. We show how runtime efficiency can be significantly improved byseveral measures carried out during the design, implementation and run-time of a protocol. Recent results of improvements in the efficiency ofEstelle-based protocol implementations are extended and interpreted.
AbstractOne main purpose for the use of formal description techniques (FDTs) is formal reasoningand verification. This requires a formal calculus and a suitable formal semantics of theFDT. In this paper, we discuss the basic verification requirements for Estelle, and howthey can be supported by existing calculi. This leads us to the redefinition of the stanADdard Estelle semantics using Lamport's temporal logic of actions and Dijkstra's predicatetransformers.