Abstract
Just as what the public pursue, we need a much safer railway system with a higher level of automation in control. To achieve this goal, the author aims to specify the Train Control System by formal methods which can specify the communication of various processes in the system clearly. This paper applies Timed-CSP which concerns the time-delay to the specification of the control flow and communication among flows in Train Control System, and specifies the state and data change by Object-Z. By Timed-CSP and Object-Z, the specification of a simplified Train Control System especially the time constraints is more concrete.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Davies, J.: Specification and Proof in Real-Time Systems, Oxford, England (1993) ISBN 0-902928-71-6
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall, Pearson (2005)
Ouaknine, J.: Timed CSP: A Retrospective. Electronic Notes in Theoretical Computer Science 162, 273–276 (2006)
Hoenicke, J.: Combination of Process, Data, and Time, Oldenburg, Germany (2006) ISSN 0946-2910
Sühl, C.: An Integration of Z and Timed CSP for Specifying Real-Time Embedded Systems (2002)
Faber, J., Jacobs, S., Sofronie-Stokkermans, V.: Verifying CSP-OZ-DC Specifications with Complex Data Types and Timing Parameters. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 233–252. Springer, Heidelberg (2007)
Hoenicke, J.: Specification of Radio Based Railway Crossings with the Combination of CSP, OZ, and DC. LNCS (2001)
Hoenicke, J., Olderog, E.-R.: Combining specification techniques for processes, data and time. In: Butler, M., Petre, L., Sere, K. (eds.) IFM 2002. LNCS, vol. 2335, pp. 245–266. Springer, Heidelberg (2002)
Faber, J., Ihlemann, C., Jacobs, S., Sofronie-Stokkermans, V.: Automatic Verification of Parametric Specifications with Complex Topologies. In: Méry, D., Merz, S. (eds.) IFM 2010. LNCS, vol. 6396, pp. 152–167. Springer, Heidelberg (2010)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Xu, B., Zhang, L. (2014). Specification of Train Control Systems Using Formal Methods. In: Park, J., Adeli, H., Park, N., Woungang, I. (eds) Mobile, Ubiquitous, and Intelligent Computing. Lecture Notes in Electrical Engineering, vol 274. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40675-1_21
Download citation
DOI: https://doi.org/10.1007/978-3-642-40675-1_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40674-4
Online ISBN: 978-3-642-40675-1
eBook Packages: EngineeringEngineering (R0)