检索结果-内蒙古大学图书馆

电子与信息学报 2011年第3期33卷 580-586页

作者：刘铭张国印姚爱红门朝光哈尔滨工程大学计算机科学与技术学院哈尔滨150001

Petri网是一种基于图形进行模拟和分析的数学工具,能够描述系统的异步和并发行为,但是现有高级Petri网不能对嵌入式实时系统进行完整的模拟与实时性分析。该文首先通过扩展有色Petri网提出了层次实时有色Petri网模型,然后描述了嵌入式... 详细信息

Petri网是一种基于图形进行模拟和分析的数学工具,能够描述系统的异步和并发行为,但是现有高级Petri网不能对嵌入式实时系统进行完整的模拟与实时性分析。该文首先通过扩展有色Petri网提出了层次实时有色Petri网模型,然后描述了嵌入式实时系统的建模和实时性分析方法。最后,将该文提出的方法应用于硬实时系统——列车通信网络MVB总线控制器的建模和实时性分析过程,仿真和分析结果表明,该方法能够满足列车通信网络系统设计对MVB总线控制器的功能验证和实时性分析需求。

关键词： Petri网列车通信网络嵌入式实时系统形式化建模

来源：评论

学校读者我要写书评

暂无评论

一种基于场景的CTCS-3列车控制系统建模方法研究

引用

铁道学报 2011年第9期33卷 55-61页

作者：王帅吉吟东杨士元清华大学计算机科学与技术系北京100084 清华信息科学与技术国家实验室北京100084 清华大学自动化系北京100084

对CTCS-3列车控制系统进行有效的测试、分析和验证是保证列车运行安全和旅客生命财产安全的重要手段,而形式化模型是系统测试、分析和验证的基础。本文以CTCS-3列车运行控制系统的UML非形式化模型为基础,以自动机模型作为系统形式化模... 详细信息

对CTCS-3列车控制系统进行有效的测试、分析和验证是保证列车运行安全和旅客生命财产安全的重要手段,而形式化模型是系统测试、分析和验证的基础。本文以CTCS-3列车运行控制系统的UML非形式化模型为基础,以自动机模型作为系统形式化模型描述的数学工具,研究UML顺序图(场景)自动转化为自动机网模型的方法。首先将场景的UML顺序图自动转化为子系统的子自动机模型,然后通过合并不同场景的子自动机模型,得到子系统的组元自动机模型,最后通过对通信通道的建模得到系统的自动机网模型。使用本方法,基于系统的UML顺序图模型可以自动生成系统的自动机网模型。

关键词： CTCS-3列车运行控制系统自动机顺序图形式化建模运营场景

来源：评论

学校读者我要写书评

暂无评论

高速列车追踪运行的控制机理研究

引用

铁道学报 2013年第3期35卷 53-61页

作者：潘登郑应平同济大学电子与信息工程学院上海201804

针对铁路移动闭塞系统列车间隔呈现出"移动"和"长度变化"的特征,研究高速列车追踪运行的控制机理。对高速列车追踪运行过程中的行为调整问题进行分析,确定了行为调整动态评价的综合性优化指标,然后运用Petri网对列... 详细信息

针对铁路移动闭塞系统列车间隔呈现出"移动"和"长度变化"的特征,研究高速列车追踪运行的控制机理。对高速列车追踪运行过程中的行为调整问题进行分析,确定了行为调整动态评价的综合性优化指标,然后运用Petri网对列车运行状态及其行为调整的起因、过程作了形式化描述;建立高速列车追踪运行过程中行为调整的控制模型,给出列车行为综合评价方法、控制策略算法及具体的实现步骤。仿真表明,研究方法有助于列车间隔动态控制,可有效实现列车安全、高效和平稳运行。

关键词：高速列车跟驰理论列车自动驾驶机理形式化建模仿真

来源：评论

学校读者我要写书评

暂无评论

基于Coq的操作系统任务管理需求层建模及验证

引用

软件学报 2020年第8期31卷 2375-2387页

作者：姜菁菁乔磊杨孟飞杨桦刘波北京控制工程研究所北京100190 中国空间技术研究院北京100094 计算机科学国家重点实验室(中国科学院软件研究所) 北京100190

为确保星上操作系统中任务管理设计的可靠性,利用定理证明工具Coq对操作系统任务管理模块进行需求层建模及形式化验证.从用户角度,基于星上操作系统任务管理的基本机制,提出一种基于任务状态列表集合的验证框架.在需求层将基本机制进行... 详细信息

为确保星上操作系统中任务管理设计的可靠性,利用定理证明工具Coq对操作系统任务管理模块进行需求层建模及形式化验证.从用户角度,基于星上操作系统任务管理的基本机制,提出一种基于任务状态列表集合的验证框架.在需求层将基本机制进行形式化建模,并在Coq中实现.针对建立的需求层模型,提出6条与实际星上操作系统任务管理一致的性质并进行验证.给出其中一条性质在Coq中的验证过程,结果表明,模型满足该条性质.

关键词：任务管理需求层形式化建模 Coq 形式化验证

来源：评论

学校读者我要写书评

暂无评论

扩展π演算对时间相关移动并发系统的建模与推演

引用

西安交通大学学报 2014年第9期48卷 30-36页

作者：罗玲段振华西安电子科技大学计算理论与技术研究所西安710071 西安电子科技大学ISN国家重点实验室西安710071

针对π演算难于对时间相关移动并发系统进行建模和推演,提出了一种采用扩展π演算p-π对时间相关移动并发系统进行形式化建模与推演的方法。该方法首先采用区间动作前缀和瞬时动作前缀分别描述系统的时间相关行为和交互行为,并通过操作... 详细信息

针对π演算难于对时间相关移动并发系统进行建模和推演,提出了一种采用扩展π演算p-π对时间相关移动并发系统进行形式化建模与推演的方法。该方法首先采用区间动作前缀和瞬时动作前缀分别描述系统的时间相关行为和交互行为,并通过操作算子将子进程进行复合,然后利用操作规则构造出系统的时间相关标记迁移系统和可接受的执行路径,最后基于上述迁移系统和执行路径完成对系统性质的推演。对移动车辆控制系统的分析表明,所提方法可对时间相关移动并发系统进行有效建模和推演,保证时间相关移动并发系统的可靠性。

关键词： π演算时间相关移动并发系统形式化建模推演

来源：评论

学校读者我要写书评

暂无评论

基于高阶多型π演算的可生存系统认知模型研究

引用

系统仿真学报 2016年第2期28卷 275-282页

作者：赵国生张楠王健哈尔滨师范大学计算机科学与信息工程学院黑龙江哈尔滨150025 哈尔滨理工大学计算机科学与技术学院黑龙江哈尔滨150001

提出一个具有多层感知能力的可生存系统认知模型。基于高阶多型π演算把认知模型的形式化建模与认知能力的量化分析同步结合,通过对系统运行状态和系统业务及内部结构形式化建模后进行认知能力的量化评估。提出一个具有多层感知能力的... 详细信息

提出一个具有多层感知能力的可生存系统认知模型。基于高阶多型π演算把认知模型的形式化建模与认知能力的量化分析同步结合,通过对系统运行状态和系统业务及内部结构形式化建模后进行认知能力的量化评估。提出一个具有多层感知能力的可生存系统认知模型;基于高阶多型π演算对可生存系统认知模型从两个角度进行形式化建模;利用MWB工具实现对不同攻击场景下的系统可用性、瞬时可用性、稳态可用性和高优先级任务吞吐量的试验。

关键词：可生存系统认知模型高阶多型π演算形式化建模

来源：评论

学校读者我要写书评

暂无评论

一种基于Isabelle/HOL的安全通信协议验证方法

引用

计算机工程 2021年第1期47卷 146-153页

作者：夏锐钱振江刘苇苏州大学计算机科学与技术学院江苏苏州215000 常熟理工学院计算机科学与工程学院江苏常熟215500 国网电力科学研究院南京211000

传统对称密钥加密协议的加密和解密速度较快,但用户无法进行身份认证,容易造成通信代理持有密钥过多导致管理困难的问题,而非对称密钥加密协议可实现用户的合法身份认证,但密钥复杂度高,使其在处理大容量消息时运行速度较慢。为解决上... 详细信息

传统对称密钥加密协议的加密和解密速度较快,但用户无法进行身份认证,容易造成通信代理持有密钥过多导致管理困难的问题,而非对称密钥加密协议可实现用户的合法身份认证,但密钥复杂度高,使其在处理大容量消息时运行速度较慢。为解决上述问题,结合对称和非对称密钥加密方式,构建D_protocol混合密钥加密协议。使用Isabelle/HOL定理证明辅助工具对D_protocol协议建立通信代理和消息序列的形式化模型,采用形式化操作语义描述用户行为,通过归纳分析方式对通信协议消息交互过程涉及的相关定理展开验证,结果表明D_protocol协议在提高通信效率的同时具有较高的安全性,并且可在一定程度上抵抗外部攻击和中间人攻击。

关键词：通信协议混合密钥形式化建模形式化验证 Isabelle/HOL定理证明辅助工具

来源：评论

学校读者我要写书评

暂无评论

支持业务事务验证的服务协调模型

引用

小型微型计算机系统 2011年第9期32卷 1734-1739页

作者：袁敏黄志球李祥南京航空航天大学信息科学与技术学院南京210016 湘南学院计算机科学系湖南郴州423043

在Web服务业务流程中如何保证参与者之间的协调一致性是亟待解决的重要问题.Web服务事务规范中描述的参与者之间的交互消息缺乏严格的语义,无法精确地描述复杂的协调活动,本文用Pi-演算形式化描述WS-TX规范中定义业务活动事务的WS-BA协... 详细信息

在Web服务业务流程中如何保证参与者之间的协调一致性是亟待解决的重要问题.Web服务事务规范中描述的参与者之间的交互消息缺乏严格的语义,无法精确地描述复杂的协调活动,本文用Pi-演算形式化描述WS-TX规范中定义业务活动事务的WS-BA协议,在此基础上建立了适用于多方参与的业务事务的服务协调模型;并利用基于等价自动机转换的HAL模型检测工具,验证分析了WS-BA协议的安全性和活性,给出一个多方参与的业务事务实例的验证过程,介绍如何利用模型检测技术来分析业务流程设计正确性的方法,有效地确保了业务事务执行的可靠性和一致性.

关键词：服务协调业务流程事务形式化建模

来源：评论

学校读者我要写书评

暂无评论

模糊时间Petri网及扩展的模糊时间Petri网

引用

计算机科学 2005年第11期32卷 241-246页

作者：董玉梅张立臣广东工业大学计算机学院广州510090

网络实时系统对时间和QoS有严格要求,因此对设计、实现和测试的技术和工具都有很高的要求。模糊时间Petri网是将模糊集合理论用于不确定的或主观的时间信息的表示,在每个变迁上添加时问间隔约束对模糊时间Petri网进行扩展得到扩展的模... 详细信息

网络实时系统对时间和QoS有严格要求,因此对设计、实现和测试的技术和工具都有很高的要求。模糊时间Petri网是将模糊集合理论用于不确定的或主观的时间信息的表示,在每个变迁上添加时问间隔约束对模糊时间Petri网进行扩展得到扩展的模糊时间 Petri网,它是一种对网络实时系统进行建模和分析的形式化模型,Petri网数学理论基础能保证并发系统的可靠性和正确性。本文详细地介绍了模糊时间 Petri网及可扩展的时间 Petri网,可扩展的时间 Petri网的网精简方法,使用 design/CPN仿真,及使用EFTN对多媒体同步建模,并探讨了进一步研究的方向。

关键词：形式化建模网精简实时系统模糊时间Petri网扩展的模糊时间Petri网时间Petri网可扩展模糊集合理论 design 形式化模型

来源：评论

学校读者我要写书评

暂无评论

安全协议的串空间图表示

引用

计算机研究与发展 2006年第12期43卷 2062-2068页

作者：王焕宝张佑生李援合肥工业大学计算机与信息学院合肥230009

串空间是安全协议的一种形式化描述,串空间图是它的图示化表示·定义开丛为串空间图的构造单元,并在开丛集上定义前缀算子和组合算子·通过开丛之间的前缀和组合运算,给出了无穷并发运行安全协议串空间图的生成方法·定义... 详细信息

串空间是安全协议的一种形式化描述,串空间图是它的图示化表示·定义开丛为串空间图的构造单元,并在开丛集上定义前缀算子和组合算子·通过开丛之间的前缀和组合运算,给出了无穷并发运行安全协议串空间图的生成方法·定义了开丛互模拟以及串空间图之间的互模拟等价关系,并给出用于消除串空间图冗余结构的化简规则·案例分析和与相关工作的比较表明,无冗余的串空间图为无穷并发运行安全协议的安全属性验证提供了一个有效的分析模型·

关键词：安全协议串空间图形式化建模

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：