Automating Verification of Cooperation, Control, and Design in Traffic Applications
Automating Verification of Cooperation, Control, and Design in Traffic Applications
复制标题
DOI：
10.1007/978-3-540-75221-9_6
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
W. Damm;A. Mikschl;Jens Oehlerking;E. Olderog;Jun Pang;André Platzer;Marc Segelken;Boris Wirtz
中科院分区：
文献类型：
--
作者：
W. Damm;A. Mikschl;Jens Oehlerking;E. Olderog;Jun Pang;André Platzer;Marc Segelken;Boris Wirtz
我们提出了一个验证方法合作交通代理合作策略的分析，通过控制实现的战略，并实施控制。对于每一层，我们都提供了专门的方法来正式验证设计的安全性和稳定性。所采用的验证技术的范围调用跨越这个验证空间，包括应用预先验证的设计模式，自动合成的李雅普诺夫函数，参数化设计的约束生成，模型检查在丰富的理论，和抽象细化。我们说明了这种方法与欧洲列车控制系统（ETCS）的变体，采用层特定的验证技术层特定的视图的ETCS设计。
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.