期刊文献+
共找到129篇文章
< 1 2 7 >
每页显示 20 50 100
基于UPPAAL的发电厂控制系统网络物理建模与安全验证
1
作者 路羚涛 刘镇瑜 《信息记录材料》 2025年第2期224-228,共5页
随着信息技术的发展,发电厂控制系统从传统的机械控制逐渐转向自动化和网络物理系统(cyber-physical systems,CPS),为电力生产和输送带来了新的机遇和挑战。CPS的引入使得系统能够实时监控和控制物理过程,但同时也引发了网络安全问题,... 随着信息技术的发展,发电厂控制系统从传统的机械控制逐渐转向自动化和网络物理系统(cyber-physical systems,CPS),为电力生产和输送带来了新的机遇和挑战。CPS的引入使得系统能够实时监控和控制物理过程,但同时也引发了网络安全问题,攻击者利用系统漏洞进行攻击可能导致严重的经济损失和社会影响。本研究旨在通过UPPAAL和可编程逻辑控制器(programmable logic controller,PLC)代码对发电厂控制系统进行建模与验证,提升其安全性。具体而言,本研究建立了发电厂控制系统的形式化模型,验证其安全属性,并基于PLC代码实现了系统的实际运行环境。此外,使用Python编写代码模拟攻击场景和防御机制,评估系统在不同攻击下的表现及防御效果。本研究旨在为发电厂控制系统的安全性提升提供理论基础和实践指导。 展开更多
关键词 网络物理系统(CPS) uppaal PLC代码 攻击与防御
在线阅读 下载PDF
基于UPPAAL的DIMA组合可调度分析方法
2
作者 刘晨 杨志斌 +1 位作者 胡乔乔 周勇 《小型微型计算机系统》 CSCD 北大核心 2024年第12期3063-3072,共10页
为了满足不断复杂化的机载任务需求,分布式综合化航空电子系统(DIMA)中任务交互行为随之激增,使其任务调度系统的设计与分析难度进一步增加.针对这一问题,提出基于UPPAAL的DIMA组合可调度分析方法.首先,给出基于UPPAAL的DIMA建模方法,... 为了满足不断复杂化的机载任务需求,分布式综合化航空电子系统(DIMA)中任务交互行为随之激增,使其任务调度系统的设计与分析难度进一步增加.针对这一问题,提出基于UPPAAL的DIMA组合可调度分析方法.首先,给出基于UPPAAL的DIMA建模方法,包括分区调度、任务、分区间通信、FC网络延迟、多核处理器资源共享等行为建模;其次,给出基于契约的组合可调度分析方法;最后,基于工业界DIMA系统案例验证所提方法的有效性. 展开更多
关键词 分布式综合化航空电子系统 组合可调度分析 时间自动机 uppaal
在线阅读 下载PDF
基于UML与UPPAAL的高铁列控临时限速切换场景建模与验证
3
作者 周翔 《山东交通学院学报》 CAS 2024年第3期31-38,共8页
为提高高速铁路列控临时限速命令在临时限速服务器(temporary speed restriction server, TSRS)与无线闭塞中心(radio block center, RBC)跨界重叠区域信息传递过程的时效性和安全性,建立TSRS切换与RBC切换跨界重叠区域限速流程的数学模... 为提高高速铁路列控临时限速命令在临时限速服务器(temporary speed restriction server, TSRS)与无线闭塞中心(radio block center, RBC)跨界重叠区域信息传递过程的时效性和安全性,建立TSRS切换与RBC切换跨界重叠区域限速流程的数学模型,根据中国列车运行控制系统(Chinese train control system, CTCS)CTCS-2/CTCS-3高铁列控系统间临时限速命令交互的特点,采用统一建模语言(unified modeling language, UML)与时间自动机模型理论相结合的方法,采用形式化验证工具UPPAAL寻找临时限速命令在跨界重叠区域信息传递的不足和漏洞。研究结果表明:列控临时限速是高铁安全运行的重要组成部分,其与高铁列控高铁调度集中(centralized traffic control, CTC)、RBC、列控中心(train control center, TCC)等相关子系统有频繁的信息交互,不同子系统间信息传递过程不同,Timer(时间控制器)、Resend(重发控制器)、TSRS和RBC时间自动机数学模型验证结果为TSRS切换与RBC切换信息在跨界重叠区域的传递时间小于3 s,且时间自动机模型信息通道无锁死情况,大大提高高铁列车运行的时效性和安全性。 展开更多
关键词 临时限速 时间自动机 UML uppaal 高铁列控
在线阅读 下载PDF
多处理器实时系统可调度性分析的UPPAAL模型 被引量:19
4
作者 代声馨 洪玫 +3 位作者 郭兵 杨秋辉 黄蔚 徐保平 《软件学报》 EI CSCD 北大核心 2015年第2期279-296,共18页
随着多处理器实时系统在安全性攸关系统中的广泛应用,保证这类系统的正确性成为一项重要的工作.可调度性是实时系统正确性的一项关键性质.它表示系统必须满足的一些时间要求.传统的可调度性分析方法结论保守或者不完备,为了避免这些方... 随着多处理器实时系统在安全性攸关系统中的广泛应用,保证这类系统的正确性成为一项重要的工作.可调度性是实时系统正确性的一项关键性质.它表示系统必须满足的一些时间要求.传统的可调度性分析方法结论保守或者不完备,为了避免这些方法的缺陷,提出使用模型检测的方法来实现可调度性分析.提出了一个用于多处理器实时系统可调度性分析的模板,将与系统可调度性相关的部分包括实时任务、运行平台和调度管理模块都用时间自动机建模,并使用UPPAAL验证可调度的性质是否总被满足.符号化模型检测方法被用于推断可调度性,但是由于秒表触发的近似机制,符号化模型检测方法不能用于证明系统不可调度.作为补充,统计模型检测方法被用于估算系统不可调度的概率,并在系统不可调度时生成反例.此外,在系统可调度时,通过统计模型检测方法获取一些性能相关的信息. 展开更多
关键词 可调度性 模型检测 uppaal 多处理器实时系统 时间自动机
在线阅读 下载PDF
基于UPPAAL的城市轨道交通CBTC区域控制子系统建模与验证 被引量:15
5
作者 吕继东 唐涛 +1 位作者 燕飞 徐天华 《铁道学报》 EI CAS CSCD 北大核心 2009年第3期59-64,共6页
CBTC(Communication Based Train Control)系统可有效提高轨道交通的列车运营效率,降低系统建设和维护费用。在系统研发过程中需对系统进行建模、仿真和验证,发现系统设计缺陷,以保证系统的安全性。CBTC区域控制子系统是一实时控制系统... CBTC(Communication Based Train Control)系统可有效提高轨道交通的列车运营效率,降低系统建设和维护费用。在系统研发过程中需对系统进行建模、仿真和验证,发现系统设计缺陷,以保证系统的安全性。CBTC区域控制子系统是一实时控制系统,它要求控制时间的精确性和控制过程的准确性。本文通过分析城市轨道交通CBTC区域控制子系统的结构,给出满足该子系统安全性的功能和性能要求,并结合时间自动机理论方法提出包含列车、速度距离控制器、区域控制器和多车控制队列的时间自动机网络模型。同时,应用UPPAAL验证工具对CBTC区域控制子系统进行仿真建模,并验证该子系统功能和性能要求,从而保证了系统模型的安全性和受限活性。 展开更多
关键词 区域控制子系统 uppaal 时间自动机 自动验证
在线阅读 下载PDF
基于UPPAAL的实时系统模型验证 被引量:23
6
作者 周清雷 姬莉霞 王艳梅 《计算机应用》 CSCD 北大核心 2004年第9期129-131,共3页
UPPAAL是一种使用时间自动机模型的实时系统验证工具 ,它可以避免时间自动机求积时状态空间的爆炸。介绍了时间自动机理论和工具UPPAAL ,着重说明如何用UPPAAL进行模型检查 。
关键词 实时系统 模型检查 时间自动机 uppaal
在线阅读 下载PDF
基于UPPAAL的AADL模型可调度性验证 被引量:16
7
作者 刘倩 桂盛霖 +1 位作者 李允 罗蕾 《计算机应用》 CSCD 北大核心 2009年第7期1820-1824,共5页
针对体系结构分析设计语言(AADL)模型的可调度性验证问题,提出了利用模型检测工具UPPAAL对其线程组件在非抢占型调度策略下的可调度性进行形式化分析和验证的方法,并实现了从AADL模型到UPPAAL中模型的模型转换工具。实验结果证明了通过U... 针对体系结构分析设计语言(AADL)模型的可调度性验证问题,提出了利用模型检测工具UPPAAL对其线程组件在非抢占型调度策略下的可调度性进行形式化分析和验证的方法,并实现了从AADL模型到UPPAAL中模型的模型转换工具。实验结果证明了通过UPPAAL来分析和验证AADL模型的可调度性问题的可行性。相比其他方法而言,基于形式化理论的本方法的验证结果更加精确。 展开更多
关键词 体系结构分析设计语言 uppaal 可调度性 非抢占
在线阅读 下载PDF
基于UPPAAL的高铁列控系统等级转换过程建模与验证 被引量:10
8
作者 康仁伟 王俊峰 吕继东 《北京交通大学学报》 CAS CSCD 北大核心 2012年第6期63-67,73,共6页
为了满足铁路线路互联互通以及设备故障之后列车降级运行的需求,列车在运行过程中需要进行等级转换.等级转换过程中,车载设备未正常接收转换预告点、转换执行点应答器的信息,或者列车速度未降至线路允许速度以下等因素,可能导致等级转... 为了满足铁路线路互联互通以及设备故障之后列车降级运行的需求,列车在运行过程中需要进行等级转换.等级转换过程中,车载设备未正常接收转换预告点、转换执行点应答器的信息,或者列车速度未降至线路允许速度以下等因素,可能导致等级转换不成功,因此有必要通过形式化建模对转换过程分析和验证.本文提出了一种基于UPPAAL的等级转换过程建模与验证方法.采用时间自动机理论建立了CTCS-2/CTCS-3等级转换过程的时间自动机网络模型,应用UPPAAL验证工具对等级转换过程进行仿真分析,验证了等级转换过程的安全性,并对现有技术规范提出了改进意见. 展开更多
关键词 CTCS-2 CTCS-3等级转换 时间自动机 uppaal 安全性
在线阅读 下载PDF
基于UPPAAL的AADL行为模型验证方法研究 被引量:12
9
作者 李振松 顾斌 《计算机科学》 CSCD 北大核心 2012年第2期159-161,169,共4页
为了实现AADL(体系结构分析与设计语言)行为模型的分析验证,基于行为附件的文法结构以及行为描述方式,提出了AADL行为模型与UPPAAL下时间自动机模型之间的模型转换规则。在转换规则的基础上,设计和实现了自动转换的原型工具。最后以航... 为了实现AADL(体系结构分析与设计语言)行为模型的分析验证,基于行为附件的文法结构以及行为描述方式,提出了AADL行为模型与UPPAAL下时间自动机模型之间的模型转换规则。在转换规则的基础上,设计和实现了自动转换的原型工具。最后以航天器控制系统中制导、导航与控制计算机从陀螺取数的AADL模型为例,经自动转换得到时间自动机模型,并在UPPAAL下仿真、验证其行为正确性,同时证明了模型转换的有效性。 展开更多
关键词 AADL 行为模型 模型转换 uppaal 验证
在线阅读 下载PDF
基于UPPAAL的手机功耗流量建模方法研究 被引量:3
10
作者 张贵玲 朱正伟 +2 位作者 蒋威 诸燕平 朱晨阳 《电子测量与仪器学报》 CSCD 北大核心 2020年第12期144-150,共7页
由于智能手机电池容量有限,应用程序的功耗是其主要消耗之一,因为应用程序可能会产生意外功耗或能源错误,其中大多数是设计错误。为分析应用程序功耗和通信流量特性,提出使用基于模型检测的功耗流量分析方法。把手机各硬件组件作为研究... 由于智能手机电池容量有限,应用程序的功耗是其主要消耗之一,因为应用程序可能会产生意外功耗或能源错误,其中大多数是设计错误。为分析应用程序功耗和通信流量特性,提出使用基于模型检测的功耗流量分析方法。把手机各硬件组件作为研究对象,对时间自动机模型进行扩展,使用模型检测工具UPPAAL构建模型。该方法可以在开发的早期阶段使用,为应用程序的设计和分析提供了异步功耗的形式化模型。设计WiFi省电模式实例进行研究分析,验证分析该模型的主要属性,然后用手机应用QQ进行了实验对比。分析结果表明,该模型符合一般模型验证需求,与PowerTutor的测量结果相比,其相对误差均低于7%,能为复杂手机系统提供可参考的建模分析思路。 展开更多
关键词 智能手机 模型检测 时间自动机 uppaal WIFI
原文传递
基于UPPAAL-TRON的高速铁路列控系统非确定性时延一致性测试研究 被引量:6
11
作者 吕继东 朱晓琳 +2 位作者 王海峰 李开成 唐涛 《铁道学报》 EI CAS CSCD 北大核心 2016年第1期54-64,共11页
高速铁路列车运行控制系统是一个典型的实时系统,如何保证列控系统在时延约束条件下功能实现的正确性至关重要。传统的离线测试方法已广泛用于列控系统功能一致性测试中,然而,随着系统复杂度的提高,物理环境中时延的非确定性制约传统离... 高速铁路列车运行控制系统是一个典型的实时系统,如何保证列控系统在时延约束条件下功能实现的正确性至关重要。传统的离线测试方法已广泛用于列控系统功能一致性测试中,然而,随着系统复杂度的提高,物理环境中时延的非确定性制约传统离线测试方法的应用。本文引入"在线测试"的概念,利用时间自动机理论对典型场景车载设备的RBC切换过程建模,并定义可观测消息通道将该模型划分为环境和设备两部分,从而借助工具UPPAAL-TRON"边生成边执行"测试用例,找出了在非确定性时延下,仿真RBC测试模型与测试需求中不一致的地方。并通过改进测试模型中RBC处理占用参数的设置,实现对RBC切换过程中跨界传递联锁消息时延非确定性的一致性测试。 展开更多
关键词 列控系统 非确定性时延 一致性测试 uppaal-TRON RBC切换
在线阅读 下载PDF
一种基于UPPAAL的Web服务组合模型检测方法 被引量:4
12
作者 何亚丽 戎玫 张广泉 《计算机科学》 CSCD 北大核心 2010年第11期122-125,共4页
Web服务组合的正确性验证对提高软件开发效率、实现服务增值具有重要意义。为从高层抽象层次研究Web服务组合的正确性及其形式化验证方法,考虑到Web服务组合中的实时特征,在采用软件体系结构描述语言XYZ/ADL对Web服务组合进行描述的基础... Web服务组合的正确性验证对提高软件开发效率、实现服务增值具有重要意义。为从高层抽象层次研究Web服务组合的正确性及其形式化验证方法,考虑到Web服务组合中的实时特征,在采用软件体系结构描述语言XYZ/ADL对Web服务组合进行描述的基础上,将其实时描述部分XYZ/RE转换至时间自动机模型,组合后系统应满足的性质用分支时序逻辑CTL公式表示,最后应用模型检测工具UPPAAL实现了Web服务组合正确性的自动化验证。 展开更多
关键词 WEB服务组合 模型检测 XYZ/ADL XYZ/RE uppaal
在线阅读 下载PDF
基于MSC与UPPAAL的列控系统等级转换场景形式化验证 被引量:11
13
作者 胡雪莲 陶彩霞 《铁道标准设计》 北大核心 2015年第2期122-127,共6页
等级转换是C3级列控系统的重要场景,是列控系统兼容性的集中体现,转换的成功与否直接关系到列车的运行安全和行车效率。因此,有必要对设计规范中所描述的转换过程进行形式化建模和验证,以保障系统的安全性和实时性。为保证设计规范与所... 等级转换是C3级列控系统的重要场景,是列控系统兼容性的集中体现,转换的成功与否直接关系到列车的运行安全和行车效率。因此,有必要对设计规范中所描述的转换过程进行形式化建模和验证,以保障系统的安全性和实时性。为保证设计规范与所建模型的一致性,采取消息顺序图(MSC)与时间自动机相结合的方式,建立等级转换场景中C2级向C3级转换过程的MSC模型,并将其转换为时间自动机模型。应用UPPAAL对模型的安全性和受限活性进行仿真验证,结果表明设计规范中所描述的转换过程是安全可靠的,可以满足C3级列控系统的兼容性和安全性要求。 展开更多
关键词 CTCS 等级转换 MSC 时间自动机 uppaal 建模
在线阅读 下载PDF
UPPAAL——一种适合自动验证实时系统的工具 被引量:12
14
作者 郭华 庄雷 张习勇 《微计算机信息》 北大核心 2006年第05X期52-54,190,共4页
UPPAAL是一个基于时间自动机的自动验证工具,已成功地用于实时控制器和通信协议等实时系统的验证。本文介绍了UPPAAL的语法,语义和语用,列举了它的几种扩展形式,并归纳了其应用及研究现状.
关键词 uppaal 时间自动机 实时系统 模型检测 协议验证
在线阅读 下载PDF
UPPAAL环境下通讯协议的自动验证 被引量:2
15
作者 周清雷 王静 赵东明 《河南师范大学学报(自然科学版)》 CAS CSCD 北大核心 2006年第4期40-42,共3页
对UPPAAL环境下通讯协议的规范验证方法进行研究,在此基础上,利用一组时间自动机模型模拟一个具有严格时间限制的网络通讯协议,并对其正确性进行自动验证.
关键词 实时系统 时间自动机 uppaal 协议验证
在线阅读 下载PDF
基于UPPAAL的虚拟生产系统仿真 被引量:1
16
作者 李琳 江志斌 《上海交通大学学报》 EI CAS CSCD 北大核心 2006年第7期1140-1147,共8页
虚拟生产系统(VPSs)是一种为应对易变的和不确定的制造环境而提出的新型生产资源结构形式.针对VPSs的特点,提出了基于自治与协调机制的控制结构.应用赋时自动机理论以及在UPPAAL的辅助下,对VPSs进行了DEDS的建模.为获得期望的性能(生产... 虚拟生产系统(VPSs)是一种为应对易变的和不确定的制造环境而提出的新型生产资源结构形式.针对VPSs的特点,提出了基于自治与协调机制的控制结构.应用赋时自动机理论以及在UPPAAL的辅助下,对VPSs进行了DEDS的建模.为获得期望的性能(生产流程和时间)和行为特性(避免冲突和死锁),设计了基于启发式调度规则的自治与协调监控器,并进行了系统分析和时间最优调度的计算与仿真,从而构建起兼顾控制和调度问题的VPSs闭环监控系统. 展开更多
关键词 虚拟生产系统 赋时自动机理论 自治与协调 监控调度 uppaal
在线阅读 下载PDF
基于UPPAAL的简单网络支付协议形式化验证 被引量:1
17
作者 余兴超 马争先 +1 位作者 王玉斌 董荣胜 《广西科学院学报》 2010年第4期465-468,共4页
分析简单支付协议中不同银行间的交易行为和各主体的超时约束,建立消费者、商家、银行和超时计时器的时间自动机模型,并用UPPAAL工具验证其是否满足商品原子性。新模型在原模型的基础上,增加了超时计时器进程来负责接收来自其它进程的... 分析简单支付协议中不同银行间的交易行为和各主体的超时约束,建立消费者、商家、银行和超时计时器的时间自动机模型,并用UPPAAL工具验证其是否满足商品原子性。新模型在原模型的基础上,增加了超时计时器进程来负责接收来自其它进程的超时信息,在各主体的计时器触发超时之后,计时器将发送超时信息,再通过外部的仲裁程序来解决纠纷。新模型能够满足货币原子性和商品原子性,并且比原模型更加符合协议运行的实际环境。 展开更多
关键词 时间自动机 电子商务协议 uppaal 原子性
在线阅读 下载PDF
基于UPPAAL的RFID定位系统准确性验证 被引量:3
18
作者 金仙力 陈楚娇 《计算机技术与发展》 2016年第9期104-108,113,共6页
随着移动通信和移动定位技术的快速发展,极大地推动了移动目标定位系统的发展。对于移动目标实时定位需求的与日俱增,人们更加注重移动目标实时定位的准确性和可靠性。介绍了时间自动机理论,并分析了基于RFID技术的移动定位处理流程。... 随着移动通信和移动定位技术的快速发展,极大地推动了移动目标定位系统的发展。对于移动目标实时定位需求的与日俱增,人们更加注重移动目标实时定位的准确性和可靠性。介绍了时间自动机理论,并分析了基于RFID技术的移动定位处理流程。采用时间自动机模型对移动定位系统进行形式化分析,分别对定位系统的四个核心模块—标签、阅读器、数据库和处理器进行建模。为了验证定位系统的可靠性,通过构建各个模块中的动作行为状态,判定不同行为状态之间的转换是否满足时间约束条件。采用模型检测工具UPPAAL对建模后的定位系统进行活性验证和安全性验证分析。实验结果表明:所设计的定位模型不存在死锁问题,满足系统的安全性并能确保移动目标的精确定位。 展开更多
关键词 RFID定位系统 时间自动机 uppaal 模型验证
在线阅读 下载PDF
基于Uppaal的时延Petri网到时间自动机等价模型验证 被引量:1
19
作者 周清雷 王静 《计算机应用研究》 CSCD 北大核心 2005年第6期64-66,共3页
时延Petri网和时间自动机都可以有效地对实时系统的行为进行模拟和性能分析。利用时延Petri网到时间自动机等价转换算法(简记作TPNtoTA转换),将一个描述实时系统的时延Petri网模型转换成与其语义等价的一组时间自动机模型。使用时间自... 时延Petri网和时间自动机都可以有效地对实时系统的行为进行模拟和性能分析。利用时延Petri网到时间自动机等价转换算法(简记作TPNtoTA转换),将一个描述实时系统的时延Petri网模型转换成与其语义等价的一组时间自动机模型。使用时间自动机中成熟的模型验证工具Uppaal对此时延Petri网的模型进行验证。 展开更多
关键词 时延PETRI网 时间自动机 TPN-to-TA转换 uppaal
在线阅读 下载PDF
基于UPPAAL的燃气报警器的建模与验证 被引量:2
20
作者 刘珊艳 《荆楚理工学院学报》 2015年第4期16-21,共6页
燃气报警器是非常重要的燃气安全设备,它是安全使用城市燃气的最后一道保障。采用时间自动机对报警器系统进行精确的描述和验证是保证其正确性和实时性的重要途径。文章设计了能够根据环境燃气浓度进行实时控制的燃气报警器系统自动机模... 燃气报警器是非常重要的燃气安全设备,它是安全使用城市燃气的最后一道保障。采用时间自动机对报警器系统进行精确的描述和验证是保证其正确性和实时性的重要途径。文章设计了能够根据环境燃气浓度进行实时控制的燃气报警器系统自动机模型,并应用UPPAAL工具仿真系统的运行过程,进一步验证系统的安全性、活性、可达性和时间约束。实验结果表明,系统的执行不仅在逻辑结果上是正确的,在实时处理上也满足规定的时间约束。 展开更多
关键词 燃气报警器 时间自动机 uppaal 实时性
在线阅读 下载PDF
上一页 1 2 7 下一页 到第
使用帮助 返回顶部