Supporting Validation and Verification of State-Based Formal Models
Daniel Plagge · 2016
The four presented articles in this work address distinct aspects of supporting the development, validation and verification of state-based systems with formal models. State-based models describe a system by defining what constitutes a state and when and how a transition to a new state can be performed. Software tools play a central role in supporting system development. ProB is such a tool that visualises and analyses the behaviour of a formal specified system via “animation” and that performs automated model checking to discover errors in the specification. Animation and model checking contribute to the development of critical software systems and the validation of systems under development. Each of the presented researches had lead to an implementation of an extension to the development and validation tool ProB that has been written originally for the B method. The first presented article explains how ProB has been extended to support the widely-used specification language Z. It shows how errors were found just by animating specifications written in Z. Another extension to ProB covers also a specification language, Event-B, a successor of the B method. A main characteristic of Event-B is its refinement mechanism and the main challenge was to support refinement and allow a user to identify problems in refined models. With formulas in temporal logic it is possible to express requirements with dependencies between a sequence of states. The extension presented in the third part verifies whether a model fulfils the given properties and therefore it allows to validate if the model meets the requirements. The last presented article applies a SAT solver via an external library to specifications loaded into ProB. SAT solving is used as a complementary technique in ProB to improve its capability to animate specifications. A specific aspect of this translation is that the target formalism is less expressive than the formalism supported by ProB and not all encountered parts of a problem statement can be translated effectively. For every presented article it is shown how it contributes to validation and verification of systems and which of ProB’s components are affected by the implementation of the corresponding extension.