期刊名称：Journal of Software Engineering and Applications
印刷版ISSN：1945-3116
电子版ISSN：1945-3124
出版年度：2015
卷号：08
期号：10
页码：531-538
DOI：10.4236/jsea.2015.810050
语种：English
出版社：Scientific Research Publishing
摘要：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.
