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

distance warnings are automatically displayed, and hydraulic pressure for the
braking system is built up, reducing the response time to a driver's reaction to
such warnings. Full automation using brake-by-wire/steer-by-wire technology is
technically feasible, and has been demonstrated early in research vehicles, e.g.,
within the California Path project. Anticipated future trac scenarios include
communication between cars and cars, and roadside infrastructure to guide co-
ordinated maneuvers for collision avoidance. We use as running example in this
paper a variant of the European Train Control System standard, which provides
collision avoidance through a fully automated coordinated movement of trains,
based on information obtained from track-side infrastructure called Radio Block
Centers (RBC). An RBC is responsible for monitoring the position of all trains in
its track segment, and provides authorities for trains to freely move ahead until
so-called End-of-Authority points (EoA) are reached. As soon as the on-board
Automatic Train Protection system ATP detects that a train risks to move be-
yond the current EoA, the ATP system takes control of the train's speed and
enforces a braking curve leading to a complete stop of the train ahead of the
EoA. Under ETCS level 3, EoAs are moved ahead by the RBCs, as soon as it
has gained safe knowledge of the fact that the train ahead has reached a safe
distance to the successor train. This “moving block principle”, where each train
is protected by an envelope surrounding and moving with the train, contrasts
to classical interlocking principles, where tracks are partitioned statically into
blocks, and trains are guaranteed exclusive access to blocks by interlocking pro-
tocols. Our running application is an extension of the moving block principle to
include rail-road crossings, see Section 2 for more details.
In the avionics domain, the Trac Alert and Collision Avoidance System
(TCAS) provides directives to pilots how to avoid a near-collision situation us-
ing combined ascend/descent maneuvers, or through recently investigated “go-
around” maneuvers, see [22].
This paper provides a formal verification methodology addressing such appli-
cation classes. Specifically, we provide dedicated verification methods for estab-
lishing safety and stability requirements for three key design layers:
1. The cooperation layer addresses inter-vehicle (and infrastructure) coopera-
tion, where trac-agents and infrastructure elements negotiate and agree on
maneuvers executed jointly to enforce safety while optimizing throughput.
2. The control layer focuses on the design of control-laws implementing the suit
of maneuvers supported by a trac agent.
3. The design layer focuses on the implementation of control-laws through dig-
ital controllers.
Jointly, the techniques presented here combine to a holistic system verification
approach, ensuring that system-level requirements are guaranteed by the imple-
mentation of control-laws supporting the maneuver capabilities of cooperating
trac agents.
Technically, the verification methodology rests on techniques for the veri-
fication of hybrid systems developed by the large-scale foundational research