【摘 要】
：
Ptolemy是一个广泛应用于信息物理融合系统的建模和仿真工具包,主要通过仿真的方式保证所建模型的正确性.形式化方法是保证系统正确性的重要方法之一.提出了一种基于形式模型
【机 构】
：
首都师范大学信息工程学院,轻型工业机器人与安全验证北京市重点实验室（首都师范大学）,华为技术上海研发中心,电子系统可靠性与数理交叉学科国家国际科技合作示范基地（首都师范大学）
【基金项目】
：
国家自然科学基金(61877040,61876111),首都师范大学交叉研究院项目(19530012005)。
论文部分内容阅读
Ptolemy是一个广泛应用于信息物理融合系统的建模和仿真工具包,主要通过仿真的方式保证所建模型的正确性.形式化方法是保证系统正确性的重要方法之一.提出了一种基于形式模型转换的方法来验证离散事件模型的正确性.离散事件模型根据不同事件的时间戳触发组件,时间自动机模型能够表达这个特征,因此选用Uppaal作为验证工具.首先定义了离散事件模型的形式语义;其次设计了一组从离散事件模型到时间自动机的映射规则;然后在Ptolemy环境中实现了一个插件,可以自动将离散事件模型转换为时间自动机模型,并通过调用Uppaal
其他文献
中央财经委员会第六次会议做出推动成渝地区双城经济圈建设重大决策部署,成渝地区双城经济圈建设上升为国家重大战略,宜宾迎来前所未有的重大发展机遇。本文旨在分析宜宾融入
随着信息物理融合系统CPS(cyber physical system)研究的深入,CPS的安全性问题越来越受到人们的广泛关注,如何验证CPS时空不一致的安全性问题已经成为研究热点.针对该问题,提
近年来,宜宾市全面贯彻落实党的路线方针政策和国家的法律法规,坚持工业经济与环境保护融合发展,相得益彰。本文在全面了解宜宾市工业绿色发展现状、存在主要问题基础上,进一
PolarFS是阿里巴巴开发的分布式文件系统,它实现了分布式共识协议Raft的一种变体,称为ParallelRaft.ParallelRaft突破了Raft中顺序提交、顺序执行的限制,允许状态机乱序执行
机器人操作系统(robot operating system,简称ROS)是一种开源的元操作系统,能够在异种计算簇上提供基于消息机制的结构化通信层.为改善ROS1中存在的数据分发实时性、可靠性问
【目的】揭示我国农业面源污染物排放对地表水质量的影响,为改善地表水质量提供理论依据。【方法】总结了1999—2018年我国主要面源污染指标排放量变化趋势,并采用水质指数(W
智能合约是运行在区块链上的计算机协议,被广泛应用在各个领域中,但是其安全问题层出不穷,因此在智能合约部署到区块链上之前,需要对其进行安全审计.然而,传统的测试方法无法
【目的】优化广西地区甘蔗灌溉制度,提升甘蔗产量。【方法】分别在甘蔗苗期(T1—T4处理)、分蘖期(T5—T8处理)、伸长期(T9—T12处理)、成熟期(T13—T16处理)设定10、20、30、
传统的委托计算需要额外开销验证计算结果的正确性,导致委托计算效率较低、开销较大.针对此问题,结合博弈论与理性信任建模(rational trust modeling,简称RTM)的思想,提出了
水利水电工程建设过程中人力资源管理有重要作用,需要高效优化人力资源,选择合适的人才在合适的岗位中工作,且采用一系列高效管理手段,激励员工始终围绕水利水电建设工程目标