主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公English
2022年专刊出版计划 微信服务介绍 最新一期:2021年第2期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
陆芝浩,王瑞,孔辉,关永,施智平.Ptolemy离散事件模型形式化验证方法.软件学报,2021,32(6):27-0
Ptolemy离散事件模型形式化验证方法
Formal Verification of Ptolemy Discrete Event Model
投稿时间:2020-08-30  修订日期:2020-10-26
DOI:10.13328/j.cnki.jos.006252
中文关键词:  形式化验证  Ptolemy离散事件模型  模型自动转换  时间自动机
英文关键词:formal verification  Ptolemy DE model  automatic model translation  timed automata
基金项目:国家自然科学基金(61877040,61876111);首都师范大学交叉研究院项目(19530012005)
作者单位E-mail
陆芝浩 轻型工业机器人与安全验证北京市重点实验室(首都师范大学 信息工程学院), 北京 100048  
王瑞 轻型工业机器人与安全验证北京市重点实验室(首都师范大学 信息工程学院), 北京 100048 rwang04@cnu.edu.cn 
孔辉 华为上海研究院, 上海 201206  
关永 电子系统可靠性与数理交叉学科国家国际科技合作示范基地(首都师范大学 信息工程学院), 北京 100048  
施智平 轻型工业机器人与安全验证北京市重点实验室(首都师范大学 信息工程学院), 北京 100048  
摘要点击次数: 54
全文下载次数: 25
中文摘要:
      Ptolemy是一个广泛应用于信息物理融合系统的建模和仿真工具包,主要通过仿真的方式保证所建模型的正确性.形式化方法是保证系统正确性的重要方法之一.本文提出了一种基于形式模型转换的方法来验证离散事件模型的正确性.离散事件模型根据不同事件的时间戳触发组件,时间自动机模型能够表达这个特征,因此选用Uppaal作为验证工具.首先定义了离散事件模型的形式语义,其次设计了一组从离散事件模型到时间自动机的映射规则.然后在Ptolemy环境中实现了一个插件,可以自动将离散事件模型转换为时间自动机模型,并通过调用Uppaal验证内核完成验证.最后以一个交通信号灯控制系统为例进行了成功的转换和验证,实验结果证实了该方法能够验证Ptolemy离散事件模型的正确性.
英文摘要:
      Ptolemy is a modeling and simulation toolkit widely used in cyber physical systems, which ensures the correctness of the models through simulation. Formal verification is one of the important methods to guarantee the correctness of systems. In this paper, we present a model translation based approach to verify the Ptolemy discrete event model. The discrete event model fires according to the timestamp of different events, and the timed automaton can express this feature. Therefore, Uppaal is a suitable verification tool. First, the semantic of discrete event model is defined. And a set of mapping rules are designed to represent the discrete event model with a network of timed automata. Then, a plug-in is implemented in the Ptolemy environment that automatically translated the discrete event model into a network of timed automata, and verifies the network of timed automata by calling the Uppaal validation kernel. Finally, a case of traffic light control system is successfully translated and verified, and the experimental results confirm that our approach is reliable and effective for the verification of Ptolemy discrete event model.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利