In: Lecture Notes in Computer Science : Computer Safety, Reliability, and Security, Volume 4166, 2006, pages 344-357. 2006. URL: http://dx.doi.org/10.1007/1187556726.
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.