Why Formal Methods Are Considered for Safety Critical Systems?


Formal methods are the mathematically techniques and tools which are used at early stages of software development lifecycle processes. The utter need of using formal methods in safety critical system leads to accuracy, consistency and correctness in proposed system. In safety critical real time application, requirements should be unambiguous and very accurate which can be achieved by using mathematical theorems. There is utter need to focus on the requirement phase which is the most critical phase of SDLC. This paper focuses on the use of Z notation for incorporating the accuracy, consistency, and eliminates ambiguity in safety critical system: Road Traffic Management System as a case study. The syntax, semantics, type checking and domain checking are further verified by using Z/EVES: a Z notation type checker tool.

Share and Cite:

Singh, M. , Sharma, A. and Saxena, R. (2015) Why Formal Methods Are Considered for Safety Critical Systems?. Journal of Software Engineering and Applications, 8, 531-538. doi: 10.4236/jsea.2015.810050.

Conflicts of Interest

The authors declare no conflicts of interest.


[1] Woodcock, J.C.P. (1989) Structuring Specifications in Z. IEE/BCS Software Engineering Journal, 4, 51-66.
[2] Hall, A. (2002) Correctness by Construction: Integrating Formality into a Commercial Development Process. Proceedings of International Symposium of Formal Methods Europe, 2391, 139-157.
[3] Spivey, J.M. (1989) The Z Notation: A Reference Manual. Prentice-Hall, Englewood Cliffs.
[4] Hamdy, K.E., Elsoud, M.A. and El-Halawany, A.M. (2011) UML-Based Web Engineering Framework for Modeling Web Application. Journal of Software Engineering, 5, 49-63.
[5] Hasan, O. and Tahar, S. (2007) Verification of Probabilistic Properties in the HOL Theorem Prover. Proceedings of the Integrated Formal Methods, 4591, 333-352.
[6] He, X. (2000) Formalizing UML Class Diagrams: A Hierarchical Predicate Transition Net Approach. Proceedings of 24th Annual International Computer Software and Applications Conference, Taipei, 25-28 October 2000, 217-222.
[7] Zafar, N.A., Khan, S.A. and Araki, K. (2012) Towards the Safety Properties of Moving Block Railway Interlocking System. International Journal of Innovative Computing, Information and Control (ICIC International), 5677-5690.
[8] Heiner, M. and Heisel, M. (1999) Modeling Safety Critical Systems with Z and Petri-Nets. Proceedings of International Conference on Computer Safety, Reliability and Security, London, 26-28 October 1999, 361-374.
[9] The Z/EVES 2.0 User’s Guide: Mark Saaltink. October 1999 ORA Canada.
[10] Mostafa, A.M., Manal, A.I., Hatem, E.B. and Saad, E.M. (2007) Toward a Formalization of UML2.0 Meta-Model Using Z Specifications. Proceedings of 8th ACIS International Conference on Software Engineering, Artificial Intelligence, Networking and Parallel/Distributed Computing, 3, 694-701.
[11] Jacobson, R.I. and Booch, G. (2006) The Unified Modeling Language Reference Manual. 2nd Edition.
[12] Selic, B. and Rumbaugh, J. (1998) UML for Modeling Complex Real-Time Systems. Technical Report, Object Time.

Copyright © 2023 by authors and Scientific Research Publishing Inc.

Creative Commons License

This work and the related PDF file are licensed under a Creative Commons Attribution 4.0 International License.