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

基于CCS的软件规范描述及Java实例 高春鸣 软件规范描述方法 软件规范描述方法主要是软件工程化的UML方法与形式化方法二类方法。形式化方法采用数学方法来描述、建模、分析和自动化软件。目前形式化方法主要流行的是Z、B、VDM和包括RAISE[6]在内的一批以谓词逻辑和集合论为基础的形式化规格说明语言。这些规格说明语言给出系统（程序）状态和状态变换操作的显式抽象定义，覆盖了从规范说明到编码过程的开发方法[5]。他们所用的符号和方法支持大部分的软件过程：需求分析、规格说明、软件设计、实现和维护。目前形式化方法主要存在的问题有：（1）类似Z、B的形式化规格说明语言，其实际规范和实际代码间的差异很大。（2）由于Z、B形式化方法本身的特点，形式化方法和软件开发过程较难平滑地结合起来。 基于进程代数的形式化描述方法 相对于逻辑方法,基于进程代数的模型和形式化描述方法能够刻画更为细致的系统行为关系。 CCS是进程代数方法的代表,它具有很好的代数性质,不仅有刻画系统行为的模型还具有进行推理的形式演算系统[1]，所以说CCS方法既有模型又有演算。此外,CCS还用互模拟关系刻画进程间的等价关系,实际上保证了系统规范和实现的语义一致性.本文首先用CCS演算描述系统需求规格，随后提出了带约束条件的CCS的概念。利用这个新的定义抽取了系统规范，最后用Java语言实现了系统原型代码。 CCS的定义 语法 进程Ｅ可用下面BNF刻画其语法: E::=Nil|A|?.E|E+E|E|E|E\L|E[f] 在进程E的表示中：Nil是终止的进程或死锁的进程,不再执行任何动作,常用0表示；A表示常量；?.E是前缀操作项,描述动作先后执行序列；Ｅ+Ｅ是求和操作项,多个项求和时，记做,描述进程的不确定选择,至少有一个进程执行；Ｅ|Ｅ是组合操作项,描述两个进程的并行执行;Ｅ\Ｌ是限定操作项,描述具有标记Ｌ的动作,在进程Ｅ中不能执行;Ｅ[ｆ]是换名映射操作项。 操作语义 派生树和进程迁移图 为了演示如何使用上述操作规则,我们利用派生树推导。来展示一个实时系统的各种行为.假设有一进程表达式为: 图1表示了它对应的派生树。 在进程迁移图中,进程以及进程间的交互行为,既可以用图表示方法，其中一个图可以对应一个进程,图之间的归约对应进程之间的交互行为。一般是通过合并一个派生树中代表相同的表达式的节点而得到的进程迁移图。 派生树和进程迁移图 我们采用CCS建模方法是基于进程迁移图向进程表达式转换的思路。我们根据系统需求，画出进程派生树，通过合并一个派生树中代表相同的表达式的节点而得到进程迁移图，然后根据结构操作语义和系统约束条件得到进程表达式。并且实现了进程表达式和图之间的手工转换形式。 实例研究 我们用CCS演算描述系统需求规格，并抽取了系统规范，用Java语言实现了系统原型代码。系统的原型是一个自动售货机[1]，如下是一个销售巧克力的自动售货机的图。我们设定大的巧克力要花费2角钱，小的巧克力要花费1角钱，为简化起见，自动售货机的投币孔只能投2角或1角钱硬币（假设有2角钱硬币）。该自动售货机工作流程是：买巧克力，从投币孔投一个1角或2角钱的硬币开始，客户可以继续投币，但是不能超过4角钱，也可以按大巧克力或小巧克力按扭，接着若收集盘中有巧克力则从取货盘处取走巧克力。自动售货机的动作按下列严格的规定：售货机既不会占客户的便宜又不会自己吃亏；在投币达到4角钱后，两个投币孔不能再投入任何硬币；取货盘只能装一只巧克力，在取货盘处已有一只巧克力时，售货机锁住两个按扭和投币孔，客户不能再次投币；在按了按扭之后，必须从取货盘处取走巧克力，才能再次投币。 系统约束条件 归纳以上自然语言描述的系统需求，系统约束条件为： 货物价格：大的巧克力要花费2角钱，小的巧克力要花费1角钱； 投币孔限制：2角投币孔投2角钱硬币，1角投币孔投1角钱硬币； 售货机工作流程限制：买巧克力，从投币孔投一个1角或2角钱的硬币，然后按大巧克力或小巧克力按扭，接着必须从取货盘处取走巧克力。取货盘只能装一只巧克力，在取货盘处已有一只巧克力时，售货机锁住按扭和两个投币孔，客户不能再次投币；在按了选择巧克力按扭之后，必须从取货盘处取走巧克力，才能再次投币。没有按选择巧克力按扭之前，巧克力不能落入取货盘处。 售货机原则：不容许投币之后，出现不能售出相应价值的巧克力；也不能售出多于投币价值的巧克力；不容许投币之后，出现机器不能处理的情况，而需要退还客户的硬币。 售货机内金额限制：在投币达到4角钱后，两个投币孔不能再投入任何硬币。 采用CCS演算描述系统需求 采用CCS演算描述系统需求 系统规范 根据系统约束条件和操作语义，参照系统