Formal Specification and Verification of Interactive Systems with Plasticity: Applications to Nuclear-Plant Supervision
250 pages. 2015.
Abstract
Plasticity provides users with different versions of a UI. Although it enhances UI capabilities, plasticity adds complexity to the development of user interfaces: the consistency between multiple versions of a given UI should be ensured. This complexity is further increased when it comes to UIs of safety-critical systems. Safety-critical systems are systems in which a failure has severe consequences. Given the large number of possible versions of a UI, it is time-consuming and error prone to check these requirements by hand. Some automation must be provided to verify plasticity. Formal verification provides a rigorous way to perform verification, which is suitable for safety-critical systems. Our main contribution is an approach to verifying safety critical interactive systems provided with plastic UIs using formal methods. Using a powerful tool support, our approach permits: (1) the verification of sets of properties over a model of the system. Using model checking, our approach permits the verification of properties over the system formal specification. Usability properties verify whether the system follows ergonomic properties to ensure a good usability. Validity properties verify whether the system follows the requirements that specify its expected behavior; (2) the comparison of different versions of UIs. Using equivalence checking, our approach verifies to which extent UIs present the same interaction capabilities and appearance. We can show whether two UI models are equivalent or not. When they are not equivalent, the UI divergences are listed, thus providing the possibility of leaving them out of the analysis. We also present three industrial case studies in the nuclear power plant domain to which the approach was applied.