专利名称：一种基于模型翻译的Ptolemy离散事件模型形式化验证方法 专利类型：发明专利
发明人：王瑞，陆芝浩，关永，孔辉，李晓娟，施智平
申请号：CN202011078298.X
申请日：20201010
公开号：CN112163343A
公开日：
20210101
专利内容由知识产权出版社提供
摘要：本发明公开一种基于模型翻译的Ptolemy离散事件模型形式化验证方法，包括：S1：获取Ptolemy离散事件模型；S2：将Ptolemy离散事件模型翻译成适合模型验证的形式化Uppaal模型；S3：对所述Uppaal模型中功能逻辑的性质进行形式化描述；S4：改进Ptolemy模型验证界面；S5：将步骤S2翻译生成的Uppaal模型与步骤S4获得的验证界面结合，完成对Ptolemy离散事件模型的验证，并将验证结果返回到验证界面。本发明可以使用Uppaal进行仿真分析，同时可以黑盒的进行安全性、可达性的分析；避免了状态空间爆炸；保证了模型一致性，同时降低了验证的复杂度；可以降低模型验证的复杂度。
申请人：首都师范大学
地址：100048 北京市海淀区西三环北路56号
国籍：CN
代理机构：北京慧泉知识产权代理有限公司
代理人：李娜
豫公网安备41160202000603
站长QQ:729038198
关于我们
投诉建议