Bridging Formal Models – An Engineering Perspective
Frank Stappers
Promotores: prof.dr.ir. J.F. Groote (TU/e) and prof.dr. M.G.J. van den Brand (TU/e)
Co-promotor: dr. M.A. Reniers (TU/e)
Technische Universiteit Eindhoven
Date: 8 November, 2012.
Summary
The thesis presents different techniques that can be used to build formal behavioral models. If modal properties are formulated, the models can be subjected to verification techniques to determine whether a odel possesses the desired properties. However many native environments do not facilitate tools or techniques to verify them. Hence, these models need to be transformed into other models that provide suitable techniques for a formal analysis. The transformations are classified into two engineering approaches, namely syntactically engineered models and semantically engineered models. Syntactically engineered models are constructed from input specifications without explicitly considering the semantics. Semantically engineered models are constructed from input specifications by explicitly considering the semantics.
The syntactic engineering approach presents four dedicated modeling techniques that construct or disseminate verification results for formal models.
The first modeling technique describes a way to create models from system descriptions that specify concurrent behavior. Here, we model three variations of a 2×2 switch, for which the models are subsequently compared to models created in the specification languages: TLA+, Bluespec, Statecharts, and ACP. The comparison validates that mCRL2 is a suitable specification language to model descriptions or specify the behavior for prototype systems.
The second syntactic technique constructs an mCRL2 model from a software implementation that operates a printer for printing Printed Circuit Boards. The model is used to advise (other) software engineers on dangerous language constructs in the control software. Hence, the model is model checked for various safety properties. The implementation is modeled through an over-approximation on the behavior by abstracting from program variables, such that only interface calls between processes and non-deterministic choices in procedures remain.
The third modeling technique describes a language transformation from the language Chi 2.0 language to the mCRL2 language. The purpose of the transformation is to facilitate model checking techniques to the discrete part of the Chi 2.0 language. The transformation illustrates that even though the languages reside in the (same) timed discrete event domain, it is not trivial to translate all syntactic notions.
The fourth technique offers a visual solution to disseminate verification result from formal models to different disciplines using native physical designs for industrially sized systems. We demonstrate the dissemination for a practical situation, showing that these solutions add value to the validation and verification of functional behavior.
By applying these modeling techniques, we observe that all techniques require human ingenuity, which can potentially introduce unintended behavior. To reduce the chances of introducing unintended behavior and rule out the human ingenuity effort as much as possible, we propose a semantic engineering approach, that constructs formal models based on the formal semantics of a language.
We first formalize the behavior of an (informal) industrial Domain Specific Language, using a Transition System Specification (TSS). By performing the formalization in a compositional way, we show that it is possible to formalize an industrial language, and that behavioral ambiguities can be resolved when informed choices are made.
The second step describes the transformation of a TSS to a Linear Process Specification (LPS). The transformation is specified for deduction rules that are in deSimone format, including predicates. The LPSs are specified in the syntax of the mCRL2 language, that, with the help of the underlying (higher-order) re-writer/tool-set, can be used for simulation, exhaustive labeled transition system generation and verification of behavioral properties.
The applicability of the approach is finally demonstrated by taking on the formal definition of the (untimed) mCRL2 language. To validate that the implementation corresponds to its formal semantics we directly model the corresponding TSS. Despite its formal characterization, thorough study and broad use in many areas, the approach reveals a number of (subtle) differences between the mCRL2’s intended semantics, the defined semantics and the actual implementation.