| Railway interlock software is a kind of typical security software. Its invalidation probably caused loss of life and property, and serious damage to environment. Among the current software exploring methods are usually described in unformed pictures and text. They are not able to describe expectable interface between components in the system, and the combination of different systems. It is difficult for the explorer to understand. Furthermore, it can not be used to analyze such features as consistency and integrity. The adoption of formalization method in modeling railway interlock software principles can be a good way to solve the problems above. Besides, it plays a vital role in assuring security and reliability of software.This paper majored in 'HJ04A Railway Signal Computer Interlock System' explored by Hefei University of Technology, mainly described and analyzed the interlock software principles formally and managed to find more suitable formalization methods to describe interlock software principles. That is Timed Automata. Lastly, UPPAAL was used to model and to prove it.The paper presented the background and present situation, put forward to the importance of formalization methods in requirements analysis of railway signal system interlock software, then introduced the concept of formalization methods, some common definitions and principles of formalization, the relative concepts of railway signals and the principles of computer interlock software. Besides, UML and Petri were both used to describe interlock software principles formally and to analyze its advantages and disadvantages. Therefore, it was concluded that Timed Automata was more suitable for modeling interlock software principles. Finally, it mainly introduced UPPAAL. As a automatic verification tool based on Timed Automata, UPPAAL can be used to model and verify interlock software principles. |
PDF Full Text Request