Rest of the paper is organized as follow: Section 2 presents the methodology and
Figure 1. Formal model for developing safety critical systems.
components of augmented framework. Section 3 presents the Formal Model of SCSs. Section 4 represents the simulation and section 5 presents the conclusion.
2. Methodology and Components
The components of this holistic approach are: Unified Modeling Language and Z Notation  ; a Formal Method and described briefly as follow.
2.1. Unified Modeling Language (UML)
UML  is a modeling technique that combines object oriented methods and concepts. It enhances the analysis and design of software system by allowing more cohesive relationships b/w objects. It has been observed that graphical representation of model is easily accessible and understandable to the user. The primary gap between the developer and the user has been easily fulfilled by the graphical description.UML composed of nine diagrams: Use case diagram, class diagram, sequence diagram, state diagram, activity diagram, interaction diagram, component diagram, deployment diagram and package diagram. Graphical representation always gives a better understanding of proposed system.
2.2. Z Notation
The proposed framework is presented in Figure 1 which helps in:
1) Capturing and improving the readability of requirements of Safety Critical Systems.
2) Model and verify the correctness of Safety Critical Systems.
3) Construct and test the Safety Critical Cases.
The requirements are captured by using graphical modeling language i.e. Unified Modeling language (UML). Once the requirements are captured, Stereotypes are used in order to improve their readability. Formal model had been developed for Use case, Class and Sequence diagram of UNL in order to depict various systems’ level properties. For example, Formal Model of use case diagram ensures that the functional requirements are complete, consistent and unambiguous. The Formalization of Class Diagram provide us the correct design specification and formal transformation of testing criteria’s helps us to assure that the test specifications are complete and consistent.
Figure 1 presents an overview of the proposed approach. The following steps are associated with this approach: 1) capturing and improving readability of informally defined requirements of safety critical systems, 2) formalization of various aspects of critical systems and formal verification of correctness―by construction as well as 3) validate the required safety properties are met.
3. Formal Analysis of Safety Critical Systems (SCSs)
This section is divided into three segments.
3.1. Capturing and Improving the Readability of Requirements of Safety Critical Systems
The requirements are usually written in natural language. To get a better understanding of system functionality, graphical languages such a Unified Modeling Language (UML) are used. Graphical representation always gives a better understanding of proposed system. The UML―use case diagram defines the behaviour of a system i.e. the functionality of the system. Therefore one can get better understanding of system behaviour by making use case diagram of the system which further forms the root of Software Requirement Specification (SRS). 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. To improve the readability of requirements, Extension Mechanism  such as Stereotype, Tagged values and Constraints are used. The UML Extension Mechanisms are used to extend UML by:
1) Adding new model elements, 2) Creating new properties and 3) specifying new semantics.
} Tagged Value
In the context of this paper, Stereotype is used to sever the purpose. A stereotype is a model element that denotes additional values, additional constraint and optionally a new graphical representation. Moreover, a stereotype allows us to attach a new semantic meaning to a model element. The two type of sterotypes are used in this paper:
・ “Include”―Include is used to extract use case fragments that are duplicated in multiple use cases. The included use case cannot stand alone and the original use case is not complete without the included one.
・ “Extend”―Extend is used when a use case adds steps to another first class use case.
3.2. Model and Verify the Correctness of Safety Critical Systems
Since class diagram is the basis for system structure and helps in designing modules of a system, but due to component of UML family, lack preciousness in semantic. To address this problem, we construct formal model for class diagram and sequence diagram in order to capture static and dynamic aspect of the system respectively. It guides the developer starting from the informal representation of class and sequence diagram (with UML) to building the corresponding parts of system module via formal modeling and verification in Z Notation and accompany toolsets. In the scope of this approach, we propose the automated Theorem Prover for demonstrating that formal system models are themselves are well defined. Moreover, in order to assure that there is no logical inconsistency and no model element contains any infeasible mathematical definition, simulation of Z specification has been done with Z/EVES  tool.
3.3. Construct and Test the Safety Critical Cases
Testing  plays an important role for checking the correctness of system implementations. To test system, test cases are formed and system behavior has been observed during execution. Based on test execution, the decision is made for the correctly functioning of the system. However, the criterion for the correctness of test cases has been specified in the system specification. A specification prescribes “What” part of the system i.e. the function that a system supposes to do and accordingly forms the foundation for testing criteria. As system specifications are documented in natural language (informal), which is generally incomplete and ambiguous in nature, due to this many problems may occur in testing processes such as incompleteness, ambiguous and inconsistency in test specifications. With an unclear specification, it is next to impossible to predict how the implemented system will behave; consequently testing will be difficult as it is not clear what to test. This become more severs specifically in case of Safety Critical System. We propose an approach to rigorous construction of structured test cases by formalization of test-specification. In other words, formal transformation of testing criteria  such as white box and black box is done by refinement pattern. Formal model of each testing criteria such as statement coverage (SC), path coverage (PC), decision coverage (DC), boundary value analysis (BV), equivalence partition class (EPC) and cause & effect is formed. This approach helps the tester to completeness and correctness of test specification in automated environment by Theorem Prover toolset. Z/EVES serve the purpose of simulation in automated environment. Moreover, formal methods are rich in mathematics axioms, supporting the argument that all the model elements definitions are consistent and feasible.
4. Simulation Results
This section is divided into two parts: section 4.1 presents the formal model for safety Critical systems and section 4.2 represents the verification of results with automated Theorem Prover.
4.1. Formal Model
Figure 2 shows the formal model for requirements and design of SCSs by formal transforming the use case, class diagram, and sequence diagram into Z notation element; Schema―a notion for structuring the formal specification written in Z notation. Moreover the formal model for testing specification is depicted in Figure 3.
The testing strategies are broadly divided into two categories: White box testing and Black box testing. White box testing focuses on internal structure of
Figure 2. Formal model for system design.
Figure 3. Formal aspect of testing criteria’s.
software artifact. One of the ways to test internal structure is to use either of following scenarios: Statement coverage (SC), decision coverage (DC) or path coverage (PC). Black box testing focuses on the input and output irrespective of internal structure. The famous black box testing criteria’s are: Equivalence partitions class (EPC), Boundary Value Analysis (BV), Cause & Effect (C&E). The formal model for all these testing criteria’s are formed with Z notation.
To validate the proposed framework, case study of Road Traffic Management System has been discussed and formal model is shown in Figure 4. RTMS make use of real-time data acquired from the road network in order to reduce traffic congestion and accidents, and to save energy and preserve the environment. The Road Traffic management System (RTMS) has three active actors i.e. Admin, Vehicle Owner, Traffic police. Traffic police maintains the information which is provided by the users (Admin, vehicle owners).
The UML model of RTMS consists of Use Case diagram, Class Diagram and Sequence Diagram in Figure 5.
Figure 4. Formal model for RTMS elements.
Figure 5. UML model for RTMS.
To ensure the correctness and completeness of specification, design draft and test specification; the formal model is further verified on automated Theorem Prover i.e. Z/EVES in Figure 6.
The RTMS elements are further verified on Z/EVES in order to enrich the validation of proposed framework which is shown in Figure 9.
The Table 1 presents the overall model analysis results on automated Theorem Prover and the parameters are: Syntax & Type checking, Domain checking and Proof by Reduction.
The proposed framework is a complete, formal, framework which can be used to develop the safety-critical system, with a combination of graphical modeling language. This framework poses the following characteristics:
・ Complete―The proposed method covers all the phases of the software development process i.e. starting from specification to design followed by verification and validation.
・ Formal―This method uses rigorous mathematics for specification, verification and validation. Consequently, provides high level of confidence as compared to conventional manual and informal methods.
Figure 6. Verification of Z specification on Z/EVES.
Figure 7. Z/EVES result for Statement Coverage (SC).
Figure 8. Z/EVES result for Equivalence Partition Class (EPC).
Figure 9. Z/EVES model analysis for RTMS elements.
Table 1. Overall model analysis results on automated theorem prover.
・ Framework―Framework presents a 2-step verification and validation approach, helps in detecting errors in early phases of development process.
・ Scalable―The approach is proficient in verifying the system (safety properties) of industrial size by allowing inductive reasoning and model checking together.
・ Facilitate the safety assurance process of formally developed safety-critical systems, by an established link between formal specification and safety cases.
・ Enhance the processes of Requirements Elicitation, Formal modeling and Verification.
・ Facilitate the system certification by showing how to incorporate safety requirements into Formal model.
・ Allows using the verification results of formal models as the evidence for construction of safety cases.