A Rigorous Framework for Verification & Validation of Dynamic Aspect of Safety Critical System
Monika Singh, Ashok Kumar Sharma, Ruhi Saxena · 2016
Being rich in the graphical notation, Unified Modeling Language (UML) is regarded as a de facto standard for visualizing, constructing and analyzing the software artifacts in both the domain i.e. in industries as well as in academia. Although UML has numerous good attributes yet not accepted for designing the safety critical system alone. One of the reasons is lack of preciousness in semantic used in graphical model. Consequently, ambiguities are introduced. In case of safety critical system, even a minor ambiguity may cause serious hazards or even loss of life. Therefore there is an utter need of improvement in informality of software models especially in safety critical domain. This paper proposed a framework for verification and validating the dynamic aspect of safety critical system. The proposed framework takes UML sequence diagram of safety critical system as input and refashions this by incorporating Z notation; a formal method. Moreover, this formal model is validated by one of the theorem prover Z notation tool i.e.by Z/EVES.