Verification of autonomous underwater vehicles using formal logic
Verification of autonomous underwater vehicles using formal logic
复制标题
DOI：
10.23919/ecc.2009.7074579
复制
发表时间：
2009-08
期刊：
影响因子：
--
通讯作者：
L. Molnar;S. Veres
中科院分区：
文献类型：
--
作者：
L. Molnar;S. Veres
研究了自主水下航行器（AUV）的形式化系统验证问题.验证包括混合系统建模，离散抽象，控制系统抽象，通过形式化模型检查检查的可达性的不良状态。本文的主要贡献是展示如何首先多层混合系统建模，然后在Stateflow™中表示和离散化，可以自动编译成多代理模型检查器系统（MCMAS）的解释脚本（ISPL）进行验证。使用这种技术，建模和模型检查可以包括自动驾驶汽车的完整物理系统，其车载多智能体软件以及表示为智能体的人机界面。
Formal systems verification of autonomous underwater vehicles (AUV) is addressed in this paper. Verification includes hybrid system modelling, discrete abstractions, control systems abstractions, checking of reachability of undesirable states by formal model checking. The main contribution of the paper is to show how first multilayered hybrid system modelling, then its representation and discretisation in Stateflow™, can be automatically compiled into interpreted script (ISPL) of the multi-agent model checker system (MCMAS) for verification. Using this technique, modelling and model checking can include the complete physical system of the autonomous vehicle, its multi-agent software on board and also the human interface represented as an agent.