Automating Verification of Cooperation, Control, and Design in Traffic Applications - Formal Methods and Hybrid Real-Time Systems - page 117

project AVACS ( www.avacs.org ) on automatic verification and analysis of com-
plex systems. The range of employed verification techniques invoked to span
this verification space includes application of pre-verified design patterns, auto-
matic synthesis of Lyapunov functions, constraint generation for parameterized
designs, model-checking in rich theories, and abstraction refinement.
The verification of the correctness of collision avoidance system has been stud-
ied extensively, e. g., within the PATH project [36], by Leveson [31], Sastry et al.
[53], Lynch et al. [32], Clarke [47], and Damm et al. [14] for various versions of
the TCAS system, or by Peleska et al. [24] and Damm et al. [6] for train system
applications. Sastry et al. presents in [53] a general approach of developing such
distributed hybrid systems. More recently, R-Charon [30], a semi-conservative ex-
tension of Charon [1,2] has been proposed for modular specification and dynamic
reconfiguration of large distributed hybrid system based on hybrid automata.
This paper is structured as follows. We give a suciently detailed presenta-
tion of the variant of the ETCS level 3 protocol used as running example in
Section 2. As unifying underlying formal model we use communicating hybrid
automata presented in Appendix 8. Section 3 describes the overall verification
methodology as well as the underlying assumptions for each modelling layer.
Section 4 shows how a pre-verified design pattern for collision avoidance pro-
tocols can be instantiated for our ETCS application. The focus of Section 5 is
on generating constraints on design parameters for collision avoidance protocols
ensuring collision freedom. Sections 6 and 7 discuss automatic verification meth-
ods for proving stability and safety, respectively, using as running example the
drive train controller for maintaining the operator selected speed. Both sections
discuss the local control as well as the design layer. We finally wrap by pointing
out directions for further work in Section 8.

2 Extending ETCS Level 3 for Rail-Road Crossings

In this section we describe the model of a train system running under a variant
of the ETCS level 3 protocol. We have extended the protocol to deal with the
protection of track segments before a train gets access to enter this segment. As
an example of an unsafe element inside a track segment we have chosen a rail road
crossing. To be able to evaluate the different aspects of an embedded system we
have developed a dynamic system model extended with different control levels.
The system dynamics are modelled in Matlab-Simulink and the control parts of
the ETCS protocol are modelled in Stateflow. The model of the dynamics consists
of three parts. The first is the mechanical transmission, which converts the input
torque into the angular velocities of the wheels. The second part consists of
the outer conditions, used to produce the present train velocity. This velocity
depends on the angular velocity of the wheels, the present adhesion between
wheel and track, and other losses such as air resistance, rolling resistance etc.
The third part of the model contains the control part of the ETCS protocol and
communicates to the crossing station and to the radio control block.