【摘 要】
：
利用时间自动机对嵌入式系统进行建模是一种有效方式,但由于时间自动机引入时间维度,导致状态空间是无限的,增加了系统分析验证的难度,为此提出一种时间自动机压缩方法,即条
【机 构】
：
大连理工大学软件学院,广东电网有限责任公司信息中心,广东电网有限责任公司信息化评测实验室,中国航天软件评测中心
论文部分内容阅读
利用时间自动机对嵌入式系统进行建模是一种有效方式,但由于时间自动机引入时间维度,导致状态空间是无限的,增加了系统分析验证的难度,为此提出一种时间自动机压缩方法,即条件符号化状态压缩法,对自动机模型进行压缩;在此基础上提出一种时间自动机形式化表示方法,采用有界模型检测的思想形式化表示线性时态逻辑（linear temporal logic,LTL）性质,将需要验证的性质输入可满足性模理论（satisfiability modulo theories,SMT）求解器进行验证,在一定程度上解决了时间自动机＂状态
其他文献
从Pardoux和Peng[58]的基础性工作以来,倒向随机微分方程（BSDE）和正倒向随机微分方程（FBSDE）由于其良好的结构和在随机控制、偏微分方程、金融数学等领域的广泛应用而备受关注.本
针对一起数字化计量系统故障,遵循一定分析步骤,逐步分析故障原因。发现故障源于合并单元计量绕组接线错误及数字电能表配置错误。针对故障原因各自采取措施后,电能计量系统
针对软件测试中功能测试用例集的数量较大且覆盖率较低的问题,提出一种基于支持向量机的测试用例自动生成方法。利用PICT测试工具产生输入参数的两组合或三组合的数据集作为
在实时数字仿真系统RTDS上建立了实验仿真工作站和搭建了110 kV及以上系统的等值仿真模型。基于RTDS系统的测试比其他测试方法更全面,主要通过RTDS系统模拟及搭建不同的故障
大气边界层是直接受地表影响并在短时间内对地表强迫做出响应的对流层底层,与人类活动及整个生态系统密切相关。边界层高度作为表征边界层结构的长度尺度以及中小尺度大气或
川藏铁路杰德秀1#隧道,施工工期长、安全系数小、技术含量高,保障隧道施工顺利实施需要加强多方面的管理工作,从而确保工程有序可控,提升经济效益。尤其是复杂地质隧道施工中
随着社会的进步和自动驾驶技术的发展,自动驾驶公交车已经开始在多地试运营,市场化也成为自动驾驶公交车面临的重要问题。自动驾驶公交车智能化、信息化、群体性出行的优势,
为提高＂软件人＂构件动态演化失败时的容错能力,提出一种基于事务的＂软件人＂构件动态演化容错机制。通过在＂软件人＂构件的管理外壳中扩展事务元接口,使＂软件人＂构件具备事务操作能力,
随着油气勘探开发的不断深入,旋转导向钻井技术得到广泛应用,下行通讯技术作为旋转导向钻井系统的重要组成部分,承担向井下工具发送地面控制指令的工作。目前,有关旋转导向下
电力行业要求定期对充SF6气体的断路器、互感器或气体绝缘金属封闭开关（GIS）内的SF6气体密度进行人工巡检、抄表,人为因素较大,每个运维人员抄的数据也有偏差,一般的密度表有温