• 新闻详情头部banner

基于HybridUML和定理证明的CPS自适应性验证方法

发布日期: 2016-09-08     发布人: 方达     来源:

技术成果简介:

本发明提出一种基于HybridUML和定理证明的CPS自适应性验证方法,主要用于解决形式化验证方法理论性过强所带来的难以普遍应用的难题。本发明步骤包括:首先利用HybridUML视图对CPS建模;然后将HybridUML规约转换为定理证明器KeYmaera的输入-量化混合程序QHP;结合生成的QHP,以量化微分动态逻辑QdL公式的形式对待验证的属性进行规约,然后利用KeYmaera进行自动验证;进行模型转换之前,需要定义HybridUMLQHP的元模型,转换时首先消除顶层Mode具有的层次性,转换后得到的模型称为FlatMode,然后根据FlatModeQHP之间宏观语义以及元语义的一致性确定转换规则,然后利用ATL语言描述转换规则,实现FlatMode模型到QHP媒介模型的转换,然后利用自定义模板语言实现QHP媒介模型到QHP代码的转换。


热门文章

  • Email:seu-sp@pub.seu.edu.cn
  • 地址:中国南京市玄武区长江后街6号
  • 电话:025-84526670
  • 传真:025-84526670-811

东大科技园微博

东大科技园公众号

版权所有©东南大学国家大学科技园( 江苏东大科技园发展有限公司 )

苏ICP备15012805号