Qualitative formal method for requirements specification and validation of hybrid real-time safety systems

The difficulties that engineers have in understanding and applying the quantitative methods in an abstract requirements phase are major obstructions in using formal methods for hybrid real-time safety systems. While formal methods technology in safety-critical systems can help increase confidence of software, the difficulty and complexity in using them can cause another hazard. The authors have proposed a framework for requirements engineering, called the qualitative formal method (QFM) for the specification and validation of hybrid real-time safety systems. The QFM emphasizes the idea of a causal and qualitative reasoning in formal methods to reduce the difficulty of specifying and validating the software requirements of hybrid safety systems. They use the qualitative formal languages, Compositional Modelling Language, and Causal Functional Representation Language in particular, to specify hybrid system dynamics and the required behaviour, respectively. The system behaviour has been simulated by the Device Modelling Environment, and validated against the required behaviour. Using the Shutdown System 2 of Wolsong nuclear power plants as a realistic example, they demonstrate the effectiveness of their approach.