Why Formal Methods Are Considered for Safety Critical Systems?

Monika Singh¹, Ashok Kumar Sharma¹, Ruhi Saxena²

¹Faculty of Engineering & Technology (FET), Mody University of Science & Technology, Sikar, India.
²Computer Science & Engineering, Thapar University, Patiala, India.

DOI: 10.4236/jsea.2015.810050                

Abstract

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.

Keywords

Formal Methods, Safety Critical System, Z Notation, Z/EVES, Syntax & Type Checking, Domain Checking

Conflicts of Interest

The authors declare no conflicts of interest.

References

[1]	Woodcock, J.C.P. (1989) Structuring Specifications in Z. IEE/BCS Software Engineering Journal, 4, 51-66. http://dx.doi.org/10.1049/sej.1989.0007
[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. http://dx.doi.org/10.1007/3-540-45614-7_13
[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. http://dx.doi.org/10.3923/jse.2011.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. http://dx.doi.org/10.1007/978-3-540-73210-5_18
[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. http://dx.doi.org/10.1007/3-540-48249-0_31
[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. http://dx.doi.org/10.1109/SNPD.2007.508
[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.