基于CCS的软件规范描述及实例

1、基于CCS的软件规范描述及Java实例高春鸣高春鸣软件规范描述方法 软件规范描述方法主要是软件工程化的UML方法与形式化方法二类方法。形式化方法采用数学方法来描述、建模、分析和自动化软件。目前形式化方法主要流行的是Z、B、VDM和包括RAISE6在内的一批以谓词逻辑和集合论为基础的形式化规格说明语言。这些规格说明语言给出系统（程序）状态和状态变换操作的显式抽象定义，覆盖了从规范说明到编码过程的开发方法5。他们所用的符号和方法支持大部分的软件过程：需求分析、规格说明、软件设计、实现和维护。目前形式化方法主要存在的问题有：（1）类似Z、B的形式化规格说明语言，其实际规范和实际代码间的差异很大。（2

2、）由于Z、B形式化方法本身的特点，形式化方法和软件开发过程较难平滑地结合起来。基于进程代数的形式化描述方法 相对于逻辑方法,基于进程代数的模型和形式化描述方法能够刻画更为细致的系统行为关系。 CCS是进程代数方法的代表,它具有很好的代数性质,不仅有刻画系统行为的模型还具有进行推理的形式演算系统1，所以说CCS方法既有模型又有演算。此外,CCS还用互模拟关系刻画进程间的等价关系,实际上保证了系统规范和实现的语义一致性.本文首先用CCS演算描述系统需求规格，随后提出了带约束条件的CCS的概念。利用这个新的定义抽取了系统规范，最后用Java语言实现了系统原型代码。 CCS的定义的定义 语法语法 进程

3、可用下面BNF刻画其语法: E:=Nil|A|.E|E+E|E|E|EL|Ef 在进程E的表示中：Nil是终止的进程或死锁的进程,不再执行任何动作,常用0表示；A表示常量；.E是前缀操作项,描述动作先后执行序列；+是求和操作项,多个项求和时，记做,描述进程的不确定选择,至少有一个进程执行；|是组合操作项,描述两个进程的并行执行;是限定操作项,描述具有标记的动作,在进程中不能执行;是换名映射操作项。 操作语义操作语义 派生树和进程迁移图派生树和进程迁移图 为了演示如何使用上述操作规则,我们利用派生树推导。来展示一个实时系统的各种行为.假设有一进程表达式为: 图1表示了它对应的派生树。 在进程迁移

4、图中,进程以及进程间的交互行为,既可以用图表示方法，其中一个图可以对应一个进程,图之间的归约对应进程之间的交互行为。一般是通过合并一个派生树中代表相同的表达式的节点而得到的进程迁移图。 0 .) 0 .0 .( . rrP设派生树和进程迁移图派生树和进程迁移图 我们采用CCS建模方法是基于进程迁移图向进程表达式转换的思路。我们根据系统需求，画出进程派生树，通过合并一个派生树中代表相同的表达式的节点而得到进程迁移图，然后根据结构操作语义和系统约束条件得到进程表达式。并且实现了进程表达式和图之间的手工转换形式。 实例研究实例研究 我们用CCS演算描述系统需求规格，并抽取了系统规范，用Java语言实

5、现了系统原型代码。系统的原型是一个自动售货机1，如下是一个销售巧克力的自动售货机的图。我们设定大的巧克力要花费2角钱，小的巧克力要花费1角钱，为简化起见，自动售货机的投币孔只能投2角或1角钱硬币（假设有2角钱硬币）。该自动售货机工作流程是：买巧克力，从投币孔投一个1角或2角钱的硬币开始，客户可以继续投币，但是不能超过4角钱，也可以按大巧克力或小巧克力按扭，接着若收集盘中有巧克力则从取货盘处取走巧克力。自动售货机的动作按下列严格的规定：售货机既不会占客户的便宜又不会自己吃亏；在投币达到4角钱后，两个投币孔不能再投入任何硬币；取货盘只能装一只巧克力，在取货盘处已有一只巧克力时，售货机锁住两个按扭和

6、投币孔，客户不能再次投币；在按了按扭之后，必须从取货盘处取走巧克力，才能再次投币。 系统约束条件 归纳以上自然语言描述的系统需求，系统约束条件为：货物价格：大的巧克力要花费2角钱，小的巧克力要花费1角钱；投币孔限制：2角投币孔投2角钱硬币，1角投币孔投1角钱硬币；售货机工作流程限制：买巧克力，从投币孔投一个1角或2角钱的硬币，然后按大巧克力或小巧克力按扭，接着必须从取货盘处取走巧克力。取货盘只能装一只巧克力，在取货盘处已有一只巧克力时，售货机锁住按扭和两个投币孔，客户不能再次投币；在按了选择巧克力按扭之后，必须从取货盘处取走巧克力，才能再次投币。没有按选择巧克力按扭之前，巧克力不能落入取货盘处

7、。售货机原则：不容许投币之后，出现不能售出相应价值的巧克力；也不能售出多于投币价值的巧克力；不容许投币之后，出现机器不能处理的情况，而需要退还客户的硬币。售货机内金额限制：在投币达到4角钱后，两个投币孔不能再投入任何硬币。 采用采用CCS演算描述系统需求演算描述系统需求 采用采用CCS演算描述系统需求演算描述系统需求 1角孔 2角孔 大按扭 小按扭 取货盘1p2pbiglittlecollect系统规范 根据系统约束条件和操作语义，参照系统进程迁移图，系统进程表达式的定义如下，也即系统规范的一个具体实现： 系统进程迁移图 系统的行为分析 整个系统的行为分析，从进程迁移图可以看到，系统存在无限的

8、状态循环路径，如连续2次投入2角硬币，可到达系统w(4p,0)状态，接着做big, 动作，客户可取出一支小的巧克力，到达w(2p,0)状态，客户这时既可继续做选择和取巧克力的工作，消耗已投硬币金额，也可又投入2角硬币，重新达到w(4p,0)状态，所以系统状态迁移存在无限的状态循环路径。以下是该无限的状态循环路径的进程表达式表示： collect无限的状态循环路径的进程表达式系统规范 系统规范 系统规范抽象了系统的行为，但由于在规范中还存在着系统模型常量，故当模型改系统规范抽象了系统的行为，但由于在规范中还存在着系统模型常量，故当模型改变时，这些常量也变化，上述方程式描述的系统规范将作废。这是因

9、为采用纯变时，这些常量也变化，上述方程式描述的系统规范将作废。这是因为采用纯CCS描述的系统规范的抽象程度有限，系统的约束条件无法加入到规范之中，所以此规描述的系统规范的抽象程度有限，系统的约束条件无法加入到规范之中，所以此规范不能作为软件形式化规格描述。因此，我们提出了带约束条件的范不能作为软件形式化规格描述。因此，我们提出了带约束条件的CCS的概念，这的概念，这样就可以把系统的约束条件显式的表现在进程表达式中。比如表达式中样就可以把系统的约束条件显式的表现在进程表达式中。比如表达式中“(money+xi )=4p xi”代表遍历代表遍历Xi的定义域中满足的定义域中满足“(money+xi

10、)=4p”这个约这个约束条件的值的集合，这个是非确定选择。我们对自动售货机的规范重新描述如下：束条件的值的集合，这个是非确定选择。我们对自动售货机的规范重新描述如下： 软件行为等价判定 i）规范与规范：对描述多进程且状态复杂的大型系统屏蔽系统的内部动作，采取抽取系统外部行为描述作为系统规约，并在系统规约与系统的软件实现间形成互模拟关系。这样可在系统软件规约与系统软件实现多个层次的不同粒度的软件行为互模拟验证； ii）规范与实现：抽象规范与具体实现之间的互模拟验证； iii）实现与实现：对同一个规范的不同实现的互模拟验证。 系统实现系统实现 我们对系统进行了软件模拟，将系统进程表达式向我们对系统

11、进行了软件模拟，将系统进程表达式向Java程序转换，程序转换，CCS的语的语法符号对应着程序构件法符号对应着程序构件, 一个进程的进程迁移图对应一个进程，一个进程对一个进程的进程迁移图对应一个进程，一个进程对应一个类，一个进程对应一组进程表达式；一个动作对应一个方法，方法的应一个类，一个进程对应一组进程表达式；一个动作对应一个方法，方法的参数就是类的状态变量；动作前置、后置条件（约束条件，设置下一步的动参数就是类的状态变量；动作前置、后置条件（约束条件，设置下一步的动作端口、通道开闭）通过手工向类中的方法做映射。作端口、通道开闭）通过手工向类中的方法做映射。整个自动售货机用一个类整个自动售货机

12、用一个类VendingMachine模拟模拟, 转换规则如下，整个转换用转换规则如下，整个转换用手工实现：手工实现： class VendingMachine int state;/数组元素对应的各端口的状态，置数组元素对应的各端口的状态，置0表示关闭端口，置表示关闭端口，置1表示开表示开放端口：放端口： /state0-1p,state1-2p,state2-little,state3-big,state4-collect int money;/钱的数量钱的数量 int number;/收集盘中巧克力的个数收集盘中巧克力的个数 VendingMachine();/构造方法构造方法 void

13、pressLittle(int money, int number)；/处理处理little按扭方法按扭方法 void pressBig(int money,int number)；/处理处理big按扭方法按扭方法 void put1P(int money,int number)；/处理投处理投1硬币方法硬币方法 void put2P(int money,int number),；/处理投处理投2个硬币方法个硬币方法 void collectChocolate(int money,int number)；/处理收集巧克力方法处理收集巧克力方法 void createComponents ();

14、/创建创建GUI组件，添加用户界面事件映射关系组件，添加用户界面事件映射关系 main();/主函数主函数 系统实现系统实现 系统进程表达式的无限循环等待 系统实现系统实现 系统动作对应类VendingMachine中的方法系统实现系统实现 系统进程表达式中不同动作之间用“+”表示的非确定性选择对应着机器端口与客户的相互作用非确定性选择对应着机器端口与客户的相互作用，采用用户界面事件触发机制实现。 系统实现系统实现 以进程表达式的定义反映的系统约束条件对应着VendingMachine对象中的方法调用序列 系统实现系统实现系统进程表达式与动作方法的实现过程没有直接的映射关系，我们可以通过系统进

15、程表达式与动作方法的实现过程没有直接的映射关系，我们可以通过动作方法中的代码间接实现系统的约束条件动作方法中的代码间接实现系统的约束条件 public void put1p(int money, int number)/判断判断1p端口是否开放端口是否开放if(state0!=1) System.out.println(“非法操作！非法操作！”)； Return; /执行执行1p动作改变系统状态动作改变系统状态this.money=money+1; /投入投入1角钱，角钱，money加加1this.number=number; /投币动作不影响巧克力个数，巧克力个数不变投币动作不影响巧克力个数，巧克力个数不变 /根据系统状态以及系统约束条件设置下一步五个端口的状态根据系统状态以及系统约束条件设置下一步五个端口的状态if(this.money+1)=4) this.state0=1; /开放数组开放