Abstract
RTCP-nets are a subclass of timed coloured Petri nets. They use transitions’ priorities and different time model than timed CP-nets. The subclass has been defined for modelling and analysis of embedded real-time systems and the ability of analysis of timing properties is one of the most important features of RTCP-nets. The paper discusses a formal, based on RTCP-nets, approach to verification of automatic train protection systems. Two examples of train protection systems are considered in the paper. A simple model of an automatic train stop system is used to introduce formal definition of RTCP-nets. A more complex model of automatic driver is used to present advanced aspects of modelling and verification with RTCP-nets. (The work is carried out within KBN Research Project, Grant No. 4 T11C 035 24.)
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
Bacherini, S., Bianchi, S., Capecchi, L., Becheri, C., Felleca, A., Fantechi, A., Spinicci, E.: Modelling a railway signalling system using SDL. In: Proc. of FORMS 2003 Symposium on Formal Methods for Railway Operation and Control Systems, Budapest, Hungary, pp. 107–113 (2003)
Banci, M., Fantechi, A., Gnesi, S.: The role of format methods in developing a distributed railway interlocking system. In: Proc. of the 5th Symposium on Formal Methods for Automation and Safety in Railway and Automotive Systems (FORMS/FORMAT 2004), Braunschweig, Germany, pp. 220–230 (2004)
Cheng, A.M.K.: Real-time Systems. Scheduling, Analysis, and Verification. Wiley Interscience, New Jersey (2002)
Haxthausen, A.E., Peleska, J.: A domain specific language for railway control systems. In: Proc. of the Sixth Biennial World Conference on Integrated Design and Process Technology, IDPT 2002, Pasadena, California (2002)
Jensen, K.: Coloured Petri Nets. In: Basic Concepts, Analysis Methods and Practical Use, vol. 1-3. Springer, Heidelberg (1992-1997)
Sommerville, I.: Software Engineering. Pearson Education Ltd., London (2004)
Szpyrka, M.: Fast and flexible modelling of real-time systems with RTCP-nets. Computer Science 6, 81–94 (2004)
Szpyrka, M., Szmuc, T.: Application of RTCP-nets for design and analysis of embedded systems. In: Proc. of Mixdes 2005, the 12th International Conference Mixed Design of Integrated Circuits and Systems, Kraków, Poland, pp. 565–570 (2005)
Szpyrka, M.: Practical aspects of development of embedded systems with RTCP-nets and ADDER Tools. In: Proc. of Mixdes 2006, the 13th International Conference Mixed Design of Integrated Circuits and Systems, Gdynia, Poland (2006)
Szpyrka, M.: Analysis of RTCP-nets with reachability graphs. Fundamenta Informaticae (to appear, 2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Szpyrka, M., Szmuc, T. (2006). Verification of Automatic Train Protection Systems with RTCP-Nets. In: Górski, J. (eds) Computer Safety, Reliability, and Security. SAFECOMP 2006. Lecture Notes in Computer Science, vol 4166. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11875567_26
Download citation
DOI: https://doi.org/10.1007/11875567_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-45762-6
Online ISBN: 978-3-540-45763-3
eBook Packages: Computer ScienceComputer Science (R0)