通信系统演算CCS与自动验证工具MWB

移动工作台MWB(Mobility Workbench)是为π-演算开发的一个自动验证工具,可对用π-演算、通信系统演算(CCS)等描述的移动并发系统进行分析与验证;首先扼要叙述CCS的基本概念,然后介绍MWB在Windows下的应用情况,最后以著名的交换比特协议(ABP)为例说明用MWB分析CCS进程的方法。

并发系统模型检测中的状态约减算法

组合可达性分析是对并发系统模型分析验证的基础和关键,但是难于解决验证中的所谓的状态爆炸问题。对此提出了基于假定状态约减验证算法(ABSR),通过自动构造子系统接口定义来约束其状态规模,在验证过程中约减冗余状态,能更大程度降低状态爆炸几率和提高验证效率。借助假定-保证(Assume-Guarantee)算法有效性定理和组合可达性分析(CRA)算法安全性验证定理,证明该验证算法的有效性。通过采用通信系统演算(CCS)描述的任务模型为例证,证明上述算法比传统CRA算法更有效。

一种面向同步交互的软件演化过程建模方法

全球化软件开发导致以交互方式协作开发的频率和复杂性越来越高。为了控制和规范软件演化的开发行为进而提高软件质量,文献[10]设计了软件演化过程元模型EPMM,由EPMM定义的软件演化过程模型未能形式描述其交互的特点。基于EPMM^([10])定义的软件演化过程包括全局层、过程层、活动层和任务层4个抽象层的思想,设计了软件演化过程元模型CEPMM。CEPMM定义的软件演化过程模型可形式描述同步交互的特点是在其活动层,由此提出一种基于通信系统演算(CCS)的软件演化过程活动层的建模方法,然后在Visual Studio平台下实现软件演化过程活动层可视化的建模工具CAmodel。CEPMM构建的软件演化过程活动层模型不仅可以描述并发、迭代等特点,还可以形式描述同步交互的特性,为模型进行严格的数学方法分析、推理奠定了基础。

基于CCS的信号量形式化建模与验证

利用通信系统演算CCS(Calculus of Communicating Systems),对用来解决进程间通信问题的信号量给出了形式化建模和验证的方法,并利用该方法对以信号量机制解决生产者—消费者问题和哲学家进餐问题进行建模、逻辑说明和验证。该方法具有一定通用性,并可将其推广到其他通过信号量机制解决进程通信的问题当中。

面向同步交互的软件演化过程全局层和过程层的建模

在全球化软件开发的背景下,针对分布在不同地域的开发团队频繁同步交互式所引起的软件演化过程的可信问题,和软件演化过程元模型EPMM构建的软件演化过程模型描述的同步交互是非形式化的问题,提出了使用通信系统演算CCS为形式工具的分布式软件演化过程元模型CEPMM.基于CEPMM构建分布式软件演化过程多层模型,包括全局层、过程层、活动层及任务层:任务是原子的,不可分割;为建立分布式软件演化过程全局层和过程层模型提出一种建模方法;最后为实现基于EPMM建模到基于CEPMM建模全局层和过程层转化,在Visual Studio平台下使用C#语言研发出工具CLPmodel.结果表明:全局层和过程层模型的建立,为在该粒度上对分布式软件演化过程的可信分析与研究奠定基础.

一种基于BCCS的多视图一致性检测的元模型

模型驱动架构(MDA)是一种采用建模描述语言如UML或BON等对需求建立平台无关模型,作为对需求规约以补充的开发方法。在复杂系统中,一个需求模型往往涵盖了多种类型的模型,用于描述系统的不同方面,如描述系统实体的静态模型,以及描述系统运行过程以及状态的动态模型,在这些模型中,往往会出现内部以及相互之间的不一致性。尝试通过B方法以及通信演算系统(CCS)来描述BON的元模型,并以此来检测BON模型中所出现的不一致性。