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

@INPROCEEDINGS{DBLP:conf/birthday/DammMOOPPSW07,
	pdf = {pub/avccdta.pdf},

  author    = {Werner Damm and
               Alfred Mikschl and
               Jens Oehlerking and
               Ernst-R{\"u}diger Olderog and
               Jun Pang and
               Andr{\'e} Platzer and
               Marc Segelken and
               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{\o}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 and
               Zhiming Liu and
               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.},
}```