Information Technology Reference
In-Depth Information
Automating Verification of
Cooperation, Control, and Design in
Trac Applications
Werner Damm 1 , 2 , Alfred Mikschl 1 , Jens Oehlerking 1 , Ernst-Rüdiger Olderog 1 ,
Jun Pang 1 , André Platzer 1 , Marc Segelken 2 ,andBorisWirtz 1
1 Carl von Ossietzky Universität Oldenburg, Ammerländer Heerstraße 114-118, 26111
Oldenburg, Germany
2 OFFIS, Escherweg 2, 26121 Oldenburg, Germany
Abstract. We present a verification methodology for cooperating trac
agents covering analysis of cooperation strategies, realization of strate-
gies through control, and implementation of control. For each layer, we
provide dedicated approaches to formal verification of safety and stability
properties of the design. The range of employed verification techniques
invoked to span this verification space includes application of pre-verified
design patterns, automatic synthesis of Lyapunov functions, constraint
generation for parameterized designs, model-checking in rich theories,
and abstraction refinement. We illustrate this approach with a variant
of the European Train Control System (ETCS), employing layer specific
verification techniques to layer specific views of an ETCS design.
1
Introduction
Our society at large depends on the transportation sector to meet the increased
demands on mobility required for achieving sustained economic growth. Major
initiatives such as ERTRAC 1 ,eSAFETY 2 and the car2car consortium in auto-
motive, ACARE 3 in avionics, and ERRAC 4 , ETCS/ERMTS 5 in rail drive stan-
dards for inter-vehicle and vehicle to infra-structure cooperation, are thriving to
push safety by enforcing cooperation principles between tra c agents.
Automatic collision avoidance systems form an integral part of such systems,
with domain specific variants ranging from fully automatic protection to partial
automation combined with warning/alerting, to warning combined with direc-
tives. For example, in the automotive domain, based on pre-crash sensing, close
This work was partly supported by the German Research Council (DFG) as part of
the Transregional Collaborative Research Center “Automatic Verification and Analy-
sis of Complex Systems” (SFB/TR 14 AVACS, http://www.avacs.org/ ).
1 European Road Transport Research Advisory Council ( www.ertrac.org )
2 http://ec.europa.eu/information_society/activities/esafety/
3 Advisory Council for Aeronautics Research in Europe ( www.acare4europe.com/ )
4 European Rail Research Advisory Council ( www.errac.com/ )
5 European Rail Trac Management System ( www.ertms.com )
Search WWH ::




Custom Search