论文部分内容阅读
[摘要]：形式化是一种基于数学的严谨的描述方式和方法。形式化不仅能够清晰地描述软件体系结构风格，并且为软件体系结构的设计提供了一种易于交流和理解的途径，因此形式化是现在软件体系结构研究的主要课题之一。形式化语言有很多种，本文要介绍的是Z语言，首先进行了Z语言的概括，以及Z语言的数学基础，最后列举了一个简单的例子说明Z语言的用法。
[关键词]形式化软件体系结构Z语言
中图分类号：S883.7 文献标识码：S 文章编号：1009―914X（2013）28―0551―02
0、引言
随着软件系统复杂度的不断增长，开发可靠，性能高的软件，已成为当前前言燃眉之急。形式化方法建立在数学模型基础之上是解决该问题的一个有价值、有希望的技术，其目标是使系统达到较高的可信度和正确性阶段，并能使系统满足优良的结构性和易维护性，最终使软件能更好的服务于用户满足需求。
采用传统方法进行软件需求分析常常不能精确的描述软件和验证，致使设计软件阶段和编码出现错误。但如果在此过程的需求分析阶段中引入形式化方法，则可以缜密的描述所开发的软件功能，一方面在减少二义性基础上提高精确性，为验证做好铺垫，另一方面对需求分析进行推理验证自动性，实现软件分析的自动化提高工作效率。
1、形式化与软件工程
1.1 形式化方法理论描述
形式化方法是建立在严格数学基础上，具有缜密的数学语义的一种开发方法。它采用数学符号的一种逻辑性的、一致性的和精密性的方式来描述软件各个精密系统的性质。对系统建立一个数学模型是它的本质思想，描述系统性质的基于数学的技术，这样的形式化方法为其提供了一个框架，在框架中以系统的而不是特别的方式刻画、开发和验证系统。形式化方法有两方面的内容分别是：形式化规格说明、形式化验证。
形式化方法的规格采用形式规格说明语言来具体的描述，比如 Z、LOTOS 等语言。Z语言作为一种采用半图形化的模式语言，拥有语言精确、无二义性、能进行证明和一致性检查等特征，它被广泛应用于各个领域。采用形式化方法有如下优势：
（1）规格说明为自动化生产软件奠定良好的基础，（2）减少了软件开发者和用户对用户需求理解上的偏差，（3）能有效的证明等价性上的目标系统和规格说明。
1.2 形式化方法的评价
形式化方法是目前兴起的一种软件开发方法，软件工作者和用户对形式化方法的评价褒贬不一，但是，绝大多的软件工作者和用户还是对形式化方法和规格说明语言充满信心和研究使用兴趣认为是研究热点。目前软件开发形式化的优势如下：（1）规格说明为自动化生产软件奠定基础；（2）减少了软件开发者和用户对用户需求理解上的偏差；（3）能对等价性上的目标系统和规格说明进行有效证明。
软件形式化未能推广的主要原因以及暂存的缺点是：
（1）形式化目前仅能在需求分析及描述阶段发挥优良作用；（2）形式化方法过于抽象不便于理解；（3）形式化有时对客观世界的动态变化过程的描述不能胜任；
1.3 形式化软件开发过程模型
形式化软件开发又称为自动化程序设计方法，一般情况下有三个阶段：用户需求规格化说明、自动化程序设计和测试维护回馈阶段。形式化软件开发的流程与其它软件开发方法基本一致，但是它在这三个阶段的实现方法上和手段运用上独有特点。
2、Z语言
如上所述，形式化方法是一种包括了各种语言、工具和技术等等的用于规范、设计和验证计算机系统的基于数学模型的方法。Z语言是目前非常流行的一种形式规格说明语言并且具有“状态—操作”特性的形式化规格说明语言。在软件产业的一些大型项目中已获得成功的应用，Z以带等词的一阶谓词逻辑ZF（Zermelo-Fraenkel）公理集合论为主要数学基础。Z中有两种语言：数学和模式语言。。Z语言在工业、学术界得到了廣泛的应用，因此被称为“软件工程”语言。
2.1Z语言起源
Z语言是由牛津大学程序设计研究小组开发的一种形式语言。随后该程序设计小组与IBM的Hursley实验室合作，将Z语言用于开发IBM客户信息控制系统，全面提高了最终产品的质量和效率，大大减少了监测出的错误数量，并且降低了整体开发费用的9%，在ISO指导下的国际标准化Z语言工作于2002年完成。
2.2Z语言简介
Z语言是一种具有“状态-操作”风格的形式化规格说明语言，并在很多大型软件项目中获得成功应用，一般用于需求分析描述。Z语言以一阶谓词逻辑和集合论作为形式语言基础，将函数、映像、关系等方法用于规格说明。用 Z 语言描述的、最简单的形式化规格说明含有下述 4 个部分：
（1）数据类型、给定的集合以及常数。（2）状态定义（3）初始状态（4）操作。
下面就电梯问题，依次介绍这四个部分。
1）给定的集合
一个 Z 规格表示是开始于一系列给定的初始化集合。所谓初始化集合就是不需要详细定义的带方括号的形式表示的集合。对于电梯问题，所有按钮的集合定义为给定的初始化集合并且称为 Button，所以，Z 规格说明开始于：〔 Button 〕
2）状态定义
一个 Z 规格说明由若干个 “ 格（schema）”组成，每个格含一系列限定变量取值范围的谓词和有一组变量说明。
在电梯问题中，Button包含有四个子集，分别是floor_buttons（楼层按钮的集合）、elevator_buttons（电梯按钮的集合）、buttons（电梯问题中所有按钮的集合）以及 pushed（所有被按的按钮的集合，即所有处于打开状态的按钮的集合）。描述了格Button_State，其中，符号P表示幂集（即给定集的所有子集）。约束条件声明，floor_buttons 集与 elevator_buttons 集不相交，而且它们共同组成buttons 集（在下面的讨论中并不需要 floor_buttons 集和 elevator_buttons 集，是用来说明 Z 格包含的内容）。
3）初始状态
抽象的初始状态是指系统第一次开启时的状态。对于 电梯问题来说，抽象的初始状态为：Button_Init 〔 Button_State ｜ pushed= Φ〕上式表示，当系统首次开启时 pushed 集为空，即所有按钮都处于关闭状态。
4）操作
如果一个原来处于关闭状态的按钮被按下，则该按钮 开启，这个按钮就被添加到 pushed 集中。操作中谓词部分，包含了一组前置条件和后置条件，分别被用于调用操作和操作完全结束之后。如果前置条件可以成立，则操作执行完成后可得到后置条件。但是，如果在调用操作的前置条件不成立的条件下调用该操作，那么久不能得到相应指定的结果（因此结果无法预测）。在前述的电梯问题中，假设电梯到达了某楼层，如果该楼层按钮已经打开，则此时它会关闭；相似的，如果相应的该电梯按钮已经打开，则此时它也会关闭。也就是说，如果 “ button? ”属于 pushed 集，则将它移出该集合。
2.3Z语言的数学基础
（1）集合
定义集合有两种方式：1）列举出集合中的所有元素2）通过构造来创建，包括符号定义、谓词（约束条件）、项（集合中的一般形式）例如：{month：N|month<13.month}集合的运算：∪，∩，∈
（2）叉集运算
A={a，b}，B={x，y} AXB={（a，x），（a，y），（b，x），（b，y）}
（3）幂集运算
PA：包含空集在内的关于A的所有子集构成的集合
A={x，y} PA=P{x，y}={ 空，{x}，{y}，{x，y} }
（4）序列：元素组成的有序集，可出现重复元素，且关心元素顺序，用“[]”表示。[a，b，c，d]与[b，c，a，d]不同[a，b，b，d]合法。seq A表示由A的元素组成的、包括空序列在内的所有序列的集合。若A={x，y}，则seq A={[]，[x，y]，[y，x]}
（5）逻辑代数
→，∨，∧，逻辑蕴含=>等
2.4类型、关系和函数
（1）类型
类型是一个受限制的种类的表达式，或者是给定的集合名，或者由多个简单类型所构成的复合类型。在Z规格说明中，每一个表达式总和一个类型相关，一个变量总是需要声明为一个类型，并且该变量的值是它的类型中的一个成员。
（2）关系和函数
类型与类型之间的关系和函数是叉积类型的特别子集，在Z语言中常用到的关系和函数有：
*X<->Y 定义域类型X和值域类型Y之间所有关系的集合。
*X->Y 从类型X到类型Y的所有全入射函数的集合。
*X+->Y 从类型X到类型Y的所有片函数的集合，部分函数不必在定义域类型的所有元素上定义函数。
* decl | pred1.pred2 表示对在decl中满足pred1的所有变量，都使pred2为真。
*∈decl | pred1.pred2 表示在decl中满足pred1的变量，都使pred2为真。
2.5Z语言应用例子
电话号码簿：假设每个人只允许有一个电话号码
所包含的两个集合：所有人名集合，所有电话号码的集合：[NAME；TELE]
*电话号码簿的状态空间，用模式来描述：状态空间的表述包含变量的声明和两个变量的关系。known是已记录了电话号码的人的名字的集合，tele是一个函数，返回对应名字的号码，分割线下表示known集合和tele集合的定义域一样。
*添加号码操作的模式描述：
图1添加号码操作
∆TelephoneBook表示TelephoneBook状态发生了变化。有四个变数known、tele、known'、tele'。前两个表示未发生变化的状态，后两个表示发生变化的状态。name？表示输入名字，telephone？表示输入电话号码。
分割线下表示输入的名字不属于已经存在于电话薄中人的名字，改变后的tele‘是原来的tele加上输入名字与号码对应后的并集。
* 查找某人的电话号码的操作：
图2查找某人电话号码的操作
TelephoneBook表示此操作使得电话薄没有发生任何变化，输入的名字必须是在NAME集合中，tele！是输出的电话号码。分割线下表示输入的名字属于已经记录的名字当中，输出的号码等于函数中输入的名字后对应的号码。
3、Z语言的评价
已经在许多软件开发项目中成功地运用了Z语言，目前，Z可能是在软件开发中应用最广泛的形式化语言，尤其是在大型项目中Z语言呈现出更为明显的优势。Z语言的成功之处在于以下几个原因：
（1）较为容易发现用Z语言编写的规格说明中的错误，特别是在软件工作者自我审查规格说明过程中，以及参照形式化的规格说明来审查设计和代码时。（2）用Z语言写规格说明时，要求軟件工作者十分精确地使用Z说明符。（3）Z语言是一种形式化语言，开发者在需要时严格地验证规格说明的正确性。
使用形式化规格说明是全球的总趋势，过去，主要是欧洲习惯于使用形式化规格说明技术，现在越来越多的美国公司也开始使用形式化规格说明技术。这是一种具有特色的有效的形式化方法，但是Z语言还存在如下不足：
（1）计算机难以直接处理Z语言（2）在大型系统的模块化能力方面Z语言略显不足。（3）较难识别影响某一状态模式的所有操作模式（4）Z中不包含重用机制所以不能操作规格说明的重用。
4、结束语
本文主要是Z语言以及模型检测工具SMV的理论研究，软件形式化研究仍然是现代软件工程的前沿技术。通过规格说明使得软件需求精确化并且为自动化生产软件奠定了坚实的基础。形式化方法在软件工程周期的各个阶段的应用有待进一步的提高。可以明确的是随着形式化方法的推进和在软件工程的全周期的应用的加大，软件工程自动划时代将提前到来，并且软件自动化能在根本上提高软件质量和生产效率。
参考文献
[1] 缪淮扣，李刚，朱关铭.软件工程语言-Z[M].上海：上海科技文献出版社，1999.
[2] 张玮玮，陈珊.软件开发中的形式化方法介绍[J].张家口职业技术学院学报，2005，18（1）：54-57.
[3] 郭广义，李代平，梅小虎.Z语言与软件体系结构风格的形式化[J].计算机技术与发展，2009，19（5）：140-143.
作者简介
程娜（1987—），女，河南孟州人，中南财经政法大学管理科学与工程专业2012级硕士研究生。
[关键词]形式化软件体系结构Z语言
中图分类号：S883.7 文献标识码：S 文章编号：1009―914X（2013）28―0551―02
0、引言
随着软件系统复杂度的不断增长，开发可靠，性能高的软件，已成为当前前言燃眉之急。形式化方法建立在数学模型基础之上是解决该问题的一个有价值、有希望的技术，其目标是使系统达到较高的可信度和正确性阶段，并能使系统满足优良的结构性和易维护性，最终使软件能更好的服务于用户满足需求。
采用传统方法进行软件需求分析常常不能精确的描述软件和验证，致使设计软件阶段和编码出现错误。但如果在此过程的需求分析阶段中引入形式化方法，则可以缜密的描述所开发的软件功能，一方面在减少二义性基础上提高精确性，为验证做好铺垫，另一方面对需求分析进行推理验证自动性，实现软件分析的自动化提高工作效率。
1、形式化与软件工程
1.1 形式化方法理论描述
形式化方法是建立在严格数学基础上，具有缜密的数学语义的一种开发方法。它采用数学符号的一种逻辑性的、一致性的和精密性的方式来描述软件各个精密系统的性质。对系统建立一个数学模型是它的本质思想，描述系统性质的基于数学的技术，这样的形式化方法为其提供了一个框架，在框架中以系统的而不是特别的方式刻画、开发和验证系统。形式化方法有两方面的内容分别是：形式化规格说明、形式化验证。
形式化方法的规格采用形式规格说明语言来具体的描述，比如 Z、LOTOS 等语言。Z语言作为一种采用半图形化的模式语言，拥有语言精确、无二义性、能进行证明和一致性检查等特征，它被广泛应用于各个领域。采用形式化方法有如下优势：
（1）规格说明为自动化生产软件奠定良好的基础，（2）减少了软件开发者和用户对用户需求理解上的偏差，（3）能有效的证明等价性上的目标系统和规格说明。
1.2 形式化方法的评价
形式化方法是目前兴起的一种软件开发方法，软件工作者和用户对形式化方法的评价褒贬不一，但是，绝大多的软件工作者和用户还是对形式化方法和规格说明语言充满信心和研究使用兴趣认为是研究热点。目前软件开发形式化的优势如下：（1）规格说明为自动化生产软件奠定基础；（2）减少了软件开发者和用户对用户需求理解上的偏差；（3）能对等价性上的目标系统和规格说明进行有效证明。
软件形式化未能推广的主要原因以及暂存的缺点是：
（1）形式化目前仅能在需求分析及描述阶段发挥优良作用；（2）形式化方法过于抽象不便于理解；（3）形式化有时对客观世界的动态变化过程的描述不能胜任；
1.3 形式化软件开发过程模型
形式化软件开发又称为自动化程序设计方法，一般情况下有三个阶段：用户需求规格化说明、自动化程序设计和测试维护回馈阶段。形式化软件开发的流程与其它软件开发方法基本一致，但是它在这三个阶段的实现方法上和手段运用上独有特点。
2、Z语言
如上所述，形式化方法是一种包括了各种语言、工具和技术等等的用于规范、设计和验证计算机系统的基于数学模型的方法。Z语言是目前非常流行的一种形式规格说明语言并且具有“状态—操作”特性的形式化规格说明语言。在软件产业的一些大型项目中已获得成功的应用，Z以带等词的一阶谓词逻辑ZF（Zermelo-Fraenkel）公理集合论为主要数学基础。Z中有两种语言：数学和模式语言。。Z语言在工业、学术界得到了廣泛的应用，因此被称为“软件工程”语言。
2.1Z语言起源
Z语言是由牛津大学程序设计研究小组开发的一种形式语言。随后该程序设计小组与IBM的Hursley实验室合作，将Z语言用于开发IBM客户信息控制系统，全面提高了最终产品的质量和效率，大大减少了监测出的错误数量，并且降低了整体开发费用的9%，在ISO指导下的国际标准化Z语言工作于2002年完成。
2.2Z语言简介
Z语言是一种具有“状态-操作”风格的形式化规格说明语言，并在很多大型软件项目中获得成功应用，一般用于需求分析描述。Z语言以一阶谓词逻辑和集合论作为形式语言基础，将函数、映像、关系等方法用于规格说明。用 Z 语言描述的、最简单的形式化规格说明含有下述 4 个部分：
（1）数据类型、给定的集合以及常数。（2）状态定义（3）初始状态（4）操作。
下面就电梯问题，依次介绍这四个部分。
1）给定的集合
一个 Z 规格表示是开始于一系列给定的初始化集合。所谓初始化集合就是不需要详细定义的带方括号的形式表示的集合。对于电梯问题，所有按钮的集合定义为给定的初始化集合并且称为 Button，所以，Z 规格说明开始于：〔 Button 〕
2）状态定义
一个 Z 规格说明由若干个 “ 格（schema）”组成，每个格含一系列限定变量取值范围的谓词和有一组变量说明。
在电梯问题中，Button包含有四个子集，分别是floor_buttons（楼层按钮的集合）、elevator_buttons（电梯按钮的集合）、buttons（电梯问题中所有按钮的集合）以及 pushed（所有被按的按钮的集合，即所有处于打开状态的按钮的集合）。描述了格Button_State，其中，符号P表示幂集（即给定集的所有子集）。约束条件声明，floor_buttons 集与 elevator_buttons 集不相交，而且它们共同组成buttons 集（在下面的讨论中并不需要 floor_buttons 集和 elevator_buttons 集，是用来说明 Z 格包含的内容）。
3）初始状态
抽象的初始状态是指系统第一次开启时的状态。对于 电梯问题来说，抽象的初始状态为：Button_Init 〔 Button_State ｜ pushed= Φ〕上式表示，当系统首次开启时 pushed 集为空，即所有按钮都处于关闭状态。
4）操作
如果一个原来处于关闭状态的按钮被按下，则该按钮 开启，这个按钮就被添加到 pushed 集中。操作中谓词部分，包含了一组前置条件和后置条件，分别被用于调用操作和操作完全结束之后。如果前置条件可以成立，则操作执行完成后可得到后置条件。但是，如果在调用操作的前置条件不成立的条件下调用该操作，那么久不能得到相应指定的结果（因此结果无法预测）。在前述的电梯问题中，假设电梯到达了某楼层，如果该楼层按钮已经打开，则此时它会关闭；相似的，如果相应的该电梯按钮已经打开，则此时它也会关闭。也就是说，如果 “ button? ”属于 pushed 集，则将它移出该集合。
2.3Z语言的数学基础
（1）集合
定义集合有两种方式：1）列举出集合中的所有元素2）通过构造来创建，包括符号定义、谓词（约束条件）、项（集合中的一般形式）例如：{month：N|month<13.month}集合的运算：∪，∩，∈
（2）叉集运算
A={a，b}，B={x，y} AXB={（a，x），（a，y），（b，x），（b，y）}
（3）幂集运算
PA：包含空集在内的关于A的所有子集构成的集合
A={x，y} PA=P{x，y}={ 空，{x}，{y}，{x，y} }
（4）序列：元素组成的有序集，可出现重复元素，且关心元素顺序，用“[]”表示。[a，b，c，d]与[b，c，a，d]不同[a，b，b，d]合法。seq A表示由A的元素组成的、包括空序列在内的所有序列的集合。若A={x，y}，则seq A={[]，[x，y]，[y，x]}
（5）逻辑代数
→，∨，∧，逻辑蕴含=>等
2.4类型、关系和函数
（1）类型
类型是一个受限制的种类的表达式，或者是给定的集合名，或者由多个简单类型所构成的复合类型。在Z规格说明中，每一个表达式总和一个类型相关，一个变量总是需要声明为一个类型，并且该变量的值是它的类型中的一个成员。
（2）关系和函数
类型与类型之间的关系和函数是叉积类型的特别子集，在Z语言中常用到的关系和函数有：
*X<->Y 定义域类型X和值域类型Y之间所有关系的集合。
*X->Y 从类型X到类型Y的所有全入射函数的集合。
*X+->Y 从类型X到类型Y的所有片函数的集合，部分函数不必在定义域类型的所有元素上定义函数。
* decl | pred1.pred2 表示对在decl中满足pred1的所有变量，都使pred2为真。
*∈decl | pred1.pred2 表示在decl中满足pred1的变量，都使pred2为真。
2.5Z语言应用例子
电话号码簿：假设每个人只允许有一个电话号码
所包含的两个集合：所有人名集合，所有电话号码的集合：[NAME；TELE]
*电话号码簿的状态空间，用模式来描述：状态空间的表述包含变量的声明和两个变量的关系。known是已记录了电话号码的人的名字的集合，tele是一个函数，返回对应名字的号码，分割线下表示known集合和tele集合的定义域一样。
*添加号码操作的模式描述：
图1添加号码操作
∆TelephoneBook表示TelephoneBook状态发生了变化。有四个变数known、tele、known'、tele'。前两个表示未发生变化的状态，后两个表示发生变化的状态。name？表示输入名字，telephone？表示输入电话号码。
分割线下表示输入的名字不属于已经存在于电话薄中人的名字，改变后的tele‘是原来的tele加上输入名字与号码对应后的并集。
* 查找某人的电话号码的操作：
图2查找某人电话号码的操作
TelephoneBook表示此操作使得电话薄没有发生任何变化，输入的名字必须是在NAME集合中，tele！是输出的电话号码。分割线下表示输入的名字属于已经记录的名字当中，输出的号码等于函数中输入的名字后对应的号码。
3、Z语言的评价
已经在许多软件开发项目中成功地运用了Z语言，目前，Z可能是在软件开发中应用最广泛的形式化语言，尤其是在大型项目中Z语言呈现出更为明显的优势。Z语言的成功之处在于以下几个原因：
（1）较为容易发现用Z语言编写的规格说明中的错误，特别是在软件工作者自我审查规格说明过程中，以及参照形式化的规格说明来审查设计和代码时。（2）用Z语言写规格说明时，要求軟件工作者十分精确地使用Z说明符。（3）Z语言是一种形式化语言，开发者在需要时严格地验证规格说明的正确性。
使用形式化规格说明是全球的总趋势，过去，主要是欧洲习惯于使用形式化规格说明技术，现在越来越多的美国公司也开始使用形式化规格说明技术。这是一种具有特色的有效的形式化方法，但是Z语言还存在如下不足：
（1）计算机难以直接处理Z语言（2）在大型系统的模块化能力方面Z语言略显不足。（3）较难识别影响某一状态模式的所有操作模式（4）Z中不包含重用机制所以不能操作规格说明的重用。
4、结束语
本文主要是Z语言以及模型检测工具SMV的理论研究，软件形式化研究仍然是现代软件工程的前沿技术。通过规格说明使得软件需求精确化并且为自动化生产软件奠定了坚实的基础。形式化方法在软件工程周期的各个阶段的应用有待进一步的提高。可以明确的是随着形式化方法的推进和在软件工程的全周期的应用的加大，软件工程自动划时代将提前到来，并且软件自动化能在根本上提高软件质量和生产效率。
参考文献
[1] 缪淮扣，李刚，朱关铭.软件工程语言-Z[M].上海：上海科技文献出版社，1999.
[2] 张玮玮，陈珊.软件开发中的形式化方法介绍[J].张家口职业技术学院学报，2005，18（1）：54-57.
[3] 郭广义，李代平，梅小虎.Z语言与软件体系结构风格的形式化[J].计算机技术与发展，2009，19（5）：140-143.
作者简介
程娜（1987—），女，河南孟州人，中南财经政法大学管理科学与工程专业2012级硕士研究生。