Verifiable Design of a Satellite-based Train Control System with Petri Nets.
Dissertation, Technische Universität Braunschweig, Juli 2014.
Nowadays model-based techniques are widely used in system design and development, especially
for safety-critical systems such as train control systems. Given a design model, executable
codes could be generated automatically from the model following certain transformation
rules. A high-quality model of a system provides a good understanding, a favourable
structure, a reasonable scale and abstraction level as well as realistic behaviours with respect
to the concurrent operation of independent subsystems. Motivated by this principle, a first
Coloured Petri Net (CPN) model of a satellite-based train control system (SatZB) with the
capability of continuous simulation is developed employing the BASYSNET method which
adopts Petri nets as the means of description during the whole development process.
After establishing the system model, the verification tasks are identified based on the hazard
analysis of the train control system. To verify the identified tasks for quality assurance, verification
by means of simulation, formal analysis and testing is carried out considering the four
representing system properties: function, state, structure and behaviour. For structural analysis,
the concept of open nets is proposed to check the reproducibility of empty markings of
scenario nets, the existence of dead transitions in the scenario nets, and the terminating states
of the scenario nets. The system behaviour, in which states are involved, is investigated by
reachability analysis. Unlike the conventional method of reachability analysis by calculating
the state space of the Petri net, techniques based on Petri net unfoldings are introduced in
this thesis. As to the functional verification, two model-based test generation techniques, i.e.,
CPN-based and SPENAT (Safe Place Transition Nets with Attributes)-based techniques, are
In this thesis, the proposed methods are exemplified by the application to the on-board module
of SatZB model. According to the verification results, no errors were found in the module.
Therefore, the confidence in the quality of the on-board module has been significantly