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, raction 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.

• Type: Conference
• Year: 2007
• Where: BIRTHDAY
• Authors: Werner Damm, Alfred Mikschl, Jens Oehlerking, Ernst-Rüdiger Olderog, Jun Pang, André Platzer, Marc Segelken, Boris Wirtz
• Keywords: Applied Computing, BIRTHDAY 2007, Layer Specific Verification, Verification Methodology, Verification Techniques