Automating verification of cooperation, control, and design in traffic applications

We present a verification methodology for cooperating
traffic agents covering analysis of cooperation
strategies, realization of strategies 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.

@inproceedings{DBLP:conf/birthday/DammMOOPPSW07,
	pdf = {pub/avccdta.pdf},
	author = {['Werner Damm', 'Alfred Mikschl', 'Jens Oehlerking', 'Ernst-Rüdiger Olderog', 'Jun Pang', 'André Platzer', 'Marc Segelken', 'Boris Wirtz']},
	title = {Automating Verification of Cooperation,
               Control, and Design in Traffic
               Applications},
	booktitle = {Formal Methods and Hybrid Real-Time
               Systems},
	longbooktitle = {Formal Methods and Hybrid Real-Time
               Systems, Essays in Honor of Dines Bjørner
               and Chaochen Zhou on the Occasion of Their
               70th Birthdays},
	year = {2007},
	pages = {115-169},
	doi = {10.1007/978-3-540-75221-9_6},
	editor = {['Cliff B. Jones', 'Zhiming Liu', 'Jim Woodcock']},
	publisher = {Springer},
	series = {LNCS},
	volume = {4700},
	isbn = {978-3-540-75220-2},
	keywords = {},
	abstract = {
    We present a verification methodology for cooperating
    traffic agents covering analysis of cooperation
    strategies, realization of strategies 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.}
}