TITLE:
Why Formal Methods Are Considered for Safety Critical Systems?
AUTHORS:
Monika Singh, Ashok Kumar Sharma, Ruhi Saxena
KEYWORDS:
Formal Methods, Safety Critical System, Z Notation, Z/EVES, Syntax & Type Checking, Domain Checking
JOURNAL NAME:
Journal of Software Engineering and Applications,
Vol.8 No.10,
October
16,
2015
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.