[00101174]一种基于Coq的机器人控制系统时序安全性的验证方法
联系人：
所在地：
- 服务承诺
- 产权明晰
-
资料保密
对所交付的所有资料进行保密
- 如实描述
技术详细介绍
本发明公开了基于Coq的机器人控制系统时序安全性的验证方法,包括以下步骤：S10,抽象系统行为；S20,制定语义模型；S30,变量的形式化、转移规则的形式化、期望性质的形式化和性质的验证。本发明解决利用定理证明器验证基于C语言的嵌入式系统时序安全性的问题。
