Portal de Periódicos da CAPES

Verification of Automatic Train Protection Systems with RTCP-Nets

2006; Springer Science+Business Media; Linguagem: Inglês

10.1007/11875567_26

1611-3349

Marcin Szpyrka, Tomasz Szmuc,

Model-Driven Software Engineering Techniques

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.)