基于SPIN/Promela的并发系统验证

并发系统安全性分析是当前计算机科学中一个重要的研究领域。模型检测是最成功的自动验证技术之一,其成功应用归功于有效验证工具的支持。SPIN 是一种著名的分析验证并发系统逻辑一致性的工具。本文在阐述 SPIN工作机理的基础上,详细分析了基于 SPIN 的系统建模语言 Promela 中通道操作、基本数据结构及其功能,并设计了SPIN 形式化验证软件系统的基本算法,最后运用 SPIN 对一个并发系统实例进行验证,得出了相应验证输出图。

时态逻辑形式化描述并发系统性质

时态逻辑是一种描述反应式(并发)系统中状态迁移序列的形式化方法,用于刻画并发系统所需验证的性质,是模型检测的基础.阐述了时态逻辑CTL 及其子逻辑CTL、LTL的语法及语义,然后分析运用时态逻辑描述并发系统性质,最后给出一个应用实例.

基于Petri网的并发系统控制器设计

针对并发系统的死锁现象 ,通过原系统 Petri网模型的状态可达图和行为规范 ,产生目标系统的可达图 ,进一步生成控制器的 Petri网模型 .由此为这类问题的控制器 Petri网模型的生成提供一条有效途径 .

基于Petri网语言的并发系统性质研究(英文)

给出 Petri网弱活性 (无死锁 )与活性的两个语言刻画 ,讨论了同步合成 Petri网的语言性质 .基于 Petri网语言 ,给出了判定 Petri网活性的充分必要条件 .同时研究了 Petri网同步合成过程中活性保持问题 ,给出保持活性的充分必要条件 .

并发系统基本模型及其分析

本文概述了目前用于并发系统形式描述的几个重要的基本模型：ＦＳＭ、Ｐｅｔｒｉ网、ＦＴＳ以及ＣＳＰ、ＣＣＳ、Ｓｔａｔｅｃｈａｒｔ等，并分析了上述一些模型的特点和不足之处，指出ＦＴＳ模型为时态逻辑用于并发系统形式描述提供了良好的基础。

并发系统建模与分析研究

基于Ｐｅｔｒｉ网提出一套完整的并发系统需求说明、建模、形式验证的方法。建立概念模型，用于需求规格说明，包括功能图、资源图和约束集。给出概念模型的精练过程，以及由概念模型到Ｐｅｔｒｉ网模型的转换算法。

基于Petri网的异步并发系统建模方法及应用研究

从Petri网的角度,异步并发是指两个或多个事件没有因果关系及由因果关系产生的顺序,与是否同时或是否有统一的时间控制没有关系。异步并发系统具有对称性、自返性而不具备传递性。其建模过程涉及到变迁发生的条件、结果以及是否存在冲突、冲撞等问题。用异步并发系统的建模方法改进Linux系统的队列数据结构,用Visobjnet++软件进行模拟,并编程测试,得到了比原结构更高的效率。

功能确定的离散并发系统的Petri网规范设计方法

本文提出概念模型的概念，作为实际问题到Ｐｅｔｒｉ同模型的桥梁，也就是系统的规格说明．概念模型包括功能图、资源图和约束集三部分，由此将系统设计中的功能与环境严格区分开，给出实际问题到概念模型，以及概念模型到Ｐｅｔｒｉ网模型的转换算法，从而构成一个面向功能的系统的Ｐｅｔｒｉ网规范设计方法．通过一制造系统的建模，说明了该方法的规范性和有效性．

并发系统的模型和自动验证

时序逻辑可以很好地应用于描述和验证并发系统的动态特性。AMC(Model Checker for Asynchronous concurrent systems)代替传统的从公理出发的形式推导,将并发系统描述转换为系统状态模型,然后应用模型实现对系统时序特性的自动验证。AMC能处理一般形式的合理性问题,并能对大的并发系统进行层次结构模型验证。

非确定并发系统设计的Petri网形式化方法

本文首先建立逻辑偏序结构概念，用于刻划非确定系统的功能结构；建立环境结构，用于描述实现系统功能所需的资源及其服务关系；以约束集表示系统应遵守的行为规范，三者合一形成了系统的需求规格说明。基于需求规格说明，分别给出逻辑偏序结构到功能网，功能网及其环境结构到系统结构网的转换算法。按照约束集的规范，结合以往的结果，对系统结构配置适当的初态，施加必要的协调控制装置，最终得到一个功能符合，性能良好，资源分配合理的系统Ｐｅｔｒｉ同模型。

实时并发系统的PTSL模型检测

随着实时并发系统的软件规模越来越大、复杂性日趋增加,如何保证并发实时系统正确性和可靠性成为日益紧迫的问题。模型检测技术采用自动化的验证算法判断系统是否具有某一性质,它不仅包括对系统模型的遍历以及基于图形的分析方法,而且还需要大量的数值计算。本文把实时并发模型看成对并发博弈模型(CGS)的扩展,在此基础上添加了概率与时间性质,提出了概率时间并发博弈结构(PTCGS)。同时本文还提出了新的逻辑语言-概率时间策略逻辑(PTSL),它显式地把策略作为一阶逻辑中的对象,从而使我们能够以简单而自然的方式指定PTCGS系统中的非零和属性。PTSL模型检测方法能够让设计者准确知道模型是否满足用户的需求,从而提高系统的可靠性。最后,本文以ZeroConf协议为例来说明PTSL模型检测方法的正确性。

并发系统建模与运作集成环境中的AGENT机制

计算机网络和计算机群集技术的发展,使分布式计算技术可以充分利用分散的计算资源,改进系统的性能和可靠性。文章采用JAVARMI技术实现分布式对象,把计算性任务构造成可移动的Agent,通过Agent的自主迁移完成分布式计算,在原有的基于面向对象PETRI并发系统建模与运作工具的基础上,实现多AGENT的体系结构,完成分布式的系统建模与运作目标,最终解决企事业过程的复杂系统模拟与运作问题。

并发系统模型研究

1.引言一个模型的作用是对想要构造或分析的系统性质给出严格定义,同时也为验证这些性质提供一个基础。现有的用于软件开发的每一种形式化描述和分析方法其有效性范围均是相对于程序执行的某一数学模型而言,并不是实际的系统。

用Petri网进行并发系统的描述与分析

本文介绍了以Petri网为工具对并发系统进行描述和分析的方法,并以Ada并发程序为例给出了Ada并发程序的描述方法。文中给出了一种Petri网的化简算法,并对化简后的Petri网构造出可达树,根据可达树分析系统的安全性、有界性和死锁等性质。

血清补体及尿蛋白肌酐比与妊娠并发系统性红斑狼疮患者流产及早产的相关性分析

目的探究血清补体及尿蛋白肌酐比(ACR)水平与妊娠并发系统性红斑狼疮(SLE)患者流产及早产的相关性。方法选择2018年3月—2020年8月本院收治的妊娠并发SLE患者120例纳入并发组,选择同期于本院进行孕检的健康孕妇104名纳入对照组。观察并记录两组孕妇血清补体C3、C4含量及ACR水平变化;分析血清补体及ACR水平与妊娠并发SLE患者流产及早产的相关性;采用Logistic回归分析影响妊娠并发SLE患者发生流产及早产的相关因素。结果并发组血清补体C3、C4含量显著低于对照组,孕周显著短于对照组(P<0.05),ACR水平、流产及早产发生率均显著高于对照组(P<0.05);流产及早产组孕妇血清补体C3、C4含量显著低于非流产及早产组(P<0.05),ACR水平显著高于非流产及早产组(P<0.05);Logistic回归分析结果显示,血清补体C3、C4降低、ACR水平升高均为影响妊娠并发SLE患者发生流产及早产的独立危险因素(P<0.05)。结论妊娠并发SLE患者血清补体C3、C4含量显著降低,ACR水平显著升高,且与患者不良妊娠结局中流产及早产的发生有关。

基于图文法的并发系统状态测试方法及其实现

在并发系统的研究和开发中，迫切需要一种能正确有效地描述并发系统的动态进程互联结构、动态进程通信和进程演化行为的形式化方法以及基于这种形式化方法的并发系统动态状态的测试手段．本文介绍一种基于图文法模型的并发系统状态测试方法，该方法与描述并发系统结构和行为的图文法模型相结合，构成了一个并发系统开发支持环境．这一方法可根据对并发系统的状态测试要求，在并发系统的运行期自动跟踪和记录并发系统的运行状态和通信情况，使并发系统的开发者可以实时地得到并发系统的运行状态。

Web Service并发系统的设计与研究

由于Internet的发展和大规模应用需求的不断涌现,单个甚至多个Web Services也往往不能很好地满足一些复杂的应用。提出了Web Service并发系统的设想。在实现技术上,通过划分小粒度服务,对小粒度服务的调用和整合,最后通过Web Service并发总线控制实现Web Service的并发系统。从而提高服务的速度和效率,充分利用资源并保证负载平衡。该模型对于改造和开发企业级Web Service有一定的适应性。

多机并发系统动态信息的逆向抽取和过滤策略

针对多机并发系统的复杂性,为了辅助用户从多个层次全面地理解并发系统,就需要抽取出能反映系统整体行为特征的动态信息。从进程的视角研究信息的逆向获取,提出了一种抽取多机并发系统动态信息的方法。此方法基于反射和开放编译的植入机制和共享内存机制,来获取所需要的动态信息,在此基础上运用分类策略来组织、收集和过滤信息,最后进行了系统的实验研究。结果表明,逆向抽取的动态信息能够正确、有效地反映多机并发系统设计时进程级别的关系。

基于偏序简化的并发系统验证

构件交互风格和交互协议的描述与验证是基于构件的分布式系统开发的基础和关键,而构件交互协议是一种典型的分布式并发系统。传统的方法难以解决系统建模和验证中的所谓的状态爆炸问题。偏序简化是应用迹的概念,对模型进行化简并且对模型进行死锁验证。但这样的验证重点放在了Petri网模型上,而没有涉及进程代数模型,所验证的只是模型是否有死锁状态。而以通信系统演算CCS为代表的进程代数,因其概念简洁,可用的数学工具丰富,在分布式并发系统的规范、分析、设计和验证方面获得了广泛应用。对此,提出将偏序规约应用于进程代数模型,给出基于进程代数模型的偏序简化算法,并提出利用进程代数模型偏序简化算法来验证安全性的方法。

基于场景的并发系统需求验证方法研究

为验证并发系统需求设计的正确性,提出一种基于场景的并发系统需求验证方法.首先,用UML顺序图建模并发系统需求场景,通过定义顺序图的操作语义及转换规则,将顺序图的XML描述文件自动转换为Promela程序,而后将描述系统需求的Promela程序和描述系统规约的线性时序逻辑作为模型检测器SPIN的输入,用模型检测的方法自动验证并发系统需求设计的一致性和完备性,最后为证明上述方法的有效性给出一个基于场景的ATM系统需求设计验证实例.实验结果表明,该方法能够有效地发现并发系统需求设计中的错误与不一致,为改进设计提供帮助.