Specifying and validating train control systems using an appropriate component-based petri nets model

摘要

The purpose of this paper is to emphasize the adequacy of the Co-NETS approach in specifying and validating a substantial part of the European train control system, namely the generalized railroad crossing system (GRC). This adequacy is particualrly expressed by handling in a satisfactory way the following GRC aspects. First, due to the Co_NETS capabilities for modeling components as a hierarchy of object oriented classes using different forms of inheritance, it is possible to cope with the size complexity in each component, namely train, gate and control system. Second, as the Co-NETS approach provides explicit interfaces for communicating different components, interaction of components in this application becomes very manageable by hiding the complex internal behaviour of each component. Third, by providing a full exhibition of intra- as well inter-object concurrency through Co-NETS semantics expressed in rewrite logic, real (concurrent0 scenarios of this application are captured. Fourth, real-time constraints which characterize this application are dealt with straightforwardly by adopting timed rewite logic for time-dependent transitions. Last but not least, an intrinsic methodology is built for deriving Co-NETS comonents from a given informal OO description.