A translation contract is a binary predicate corrTransl(S,T) for source programs S and target programs T. It precisely specifies when T is considered to be a correct translation of S. A certifying compiler generates --in addittion to the target T-- a proof for corrTransl(S,T). Certifying compilers are important for the development of safety critical systems to establish the behavioral equivalence of high-level programs with their compiled assembler code. In this paper, we report on a certifying compiler, its proof techniques, and the underlying formal framework developed within the proof assistent Isabelle/HOL. The compiler uses a tiny C-like language as input, has an optimization phase, and generates MIPS code. The underlying translation contract is based on a trace semantics. We investigate design alternatives and discuss our experiences.
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.
The feature interaction problem in telecommunications systems increasingly ob-structs the evolution of such systems. We develop formal detection criteria whichrender a necessary (but less than sufficient) condition for feature interactions. It can be checked mechanically and points out all potentially critical spots. Thesehave to be analysed manually. The resulting resolution decisions are incorporatedformally. Some prototype tool support is already available. A prerequisite forformal criteria is a formal definition of the problem. Since the notions of featureand feature interaction are often used in a rather fuzzy way, we attempt a formaldefinition first and discuss which aspects can be included in a formalization (andtherefore in a detection method). This paper describes ongoing work.