摘要：为解决直接建立系统NuSMV(符号模型检测器)模型的困难,提出一种从UML(统一建模语言)模型转换到NuSMV模型的方法,实现了UML与NuSMV结合的形式化验证.首先,使用UML中的视图对系统进行描述,建立系统的UML模型;然后,设计转换规则并给出转换算法,实现从UML模型到NuSMV模型的自动转换;最后,使用计算树逻辑对系统的属性进行描述,并通过NuSMV完成对系统的形式化验证.以一个双按键并发电梯系统为例,说明了基于UML-NuSMV的并发系统建模与验证过程.

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

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

摘要：面向对象的并发系统与传统的并发系统的不同之片在于其进程结构的动态性，系统中地进程以及进程之间的通信链路随着对象的变化而动态地建议或撤消。文法模型比其他形式化化工具更适合描述这种并发和动态的特性。这里我们介绍一个新的用于描述向对象并发系统的图文法模型，在该模型中为系统的设计开发者提供了一个用来描述诉静态和动态结构的语言工具－ＣＤＳＬ语言。

摘要：1引言Java作为一种面向分布式计算环境的语言,提供了完全意义上的多线程支持,能有效利用资源,提高系统效率,但是多线程并发也带来了很多严重问题,如死锁.为了详尽分析Java并发系统,首先必须对并发系统进行建模.

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

摘要：模型检验是一种重要的自动验证技术 ,通过显式状态搜索或隐式不动点计算来验证并发或实时系统的模态 /命题性质 ,以保证通信协议、数字电路等设计的正确性 .详细阐述了模型检验技术的发展与研究现状 .首先描述了并发系统分别基于自动机理论和符号化的两种主要模型检验策略 ,并给出解决状态爆炸问题的主要方法 ;然后介绍了针对实时系统以及面向对象设计的模型检验方法 ;对每种方法都介绍了相应的典型工具 .

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

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

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