本发明公开了一种面向RoboSim模型实时系统的模型检测方法,其特点是通过预先定义转换规则,将RoboSim模型转换为UPPAAL能识别的时间自动机网络模型,自动生成相应的TCTL性质,使用模型检测工具UPPAAL对机器人仿真模型进行模拟、验证及分析。本发明与现有技术相比具有验证效率高,且适合对机器人的物理平台和环境进行建模和验证,支持将RoboSim模型转换为时间自动机网络模型,为形式化验证RoboSim机器人仿真模型提供了一套有效的方法。
科研之友
微信
新浪微博
Facebook
分享链接
