Formal Specification of Railway Control Systems
Train control systems must provide a high level of safety as they are a very important component and responsible for the safe operation of a train. To meet safety and reliability requirements, formal techniques must be used to specify train control system
- PDF / 363,655 Bytes
- 11 Pages / 439.37 x 666.142 pts Page_size
- 18 Downloads / 272 Views
Abstract Train control systems must provide a high level of safety as they are a very important component and responsible for the safe operation of a train. To meet safety and reliability requirements, formal techniques must be used to specify train control systems. In this paper, we uses CSP, Object-Z and Clock to specify the Railway Control System concerning both the linear track and crossing area, especially the time delay between any two aspects of the railway system. Keywords Railway control systems specification
Object-Z CSP Clock theory Formal
Introduction Train control systems must provide a high level of safety as they are a very important component and responsible for the safe operation of a train. To meet safety and reliability requirements, the relative international standards recommend the application of formal methods in specifying development specifications and design for train control systems [1, 2]. Complicated system such as railway control system is a system with many complex behavioral aspects. And the mechanism of communication between different aspects is hard to define. With help of formal methods, we now find a way to construct a detailed specification of each aspect and the link mechanism among various aspects. While a communication mechanism is not enough to describe the state change and data change in the system. Above all, the author tends to use Communicating Sequential Processes (CSP) [3] to specify the communication part of the Railway Control System. Concerning the B. Xu L. Zhang (&) Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, China e-mail: [email protected]
Y.-M. Huang et al. (eds.), Advanced Technologies, Embedded and Multimedia for Human-centric Computing, Lecture Notes in Electrical Engineering 260, DOI: 10.1007/978-94-007-7262-5_46, Ó Springer Science+Business Media Dordrecht 2014
389
390
B. Xu and L. Zhang
time characteristics in the system, Clock [4–7] specifies the system time requirements better. For the state and data changes, Object-Z is ideal for analysis in data change in a schema box form. In this paper, we uses CSP, Object-Z and Clock to specify the Railway Control System concerning both the linear track and crossing area, especially the time delay between any two aspects of the railway system.
Relative Works Hoenicke [8–12] uses a combination of three techniques for the specification of processes, data and time: CSP, Object-Z and Duration Calculus. The basic building block in our combined formalism CSP-OZ-DC is a class. First, the communication channels of the class are declared. Every channel has a type which restricts the values that it can communicate. There are also local channels that are visible only inside the class and that are used by the CSP, Z, and DC parts for interaction. Second, the CSP part follows; it is given by a system of (recursive) process equations. Third, the Z part is given which itself consists of the state space, the Init schema and communication schemas. For each com
Data Loading...
