软件工程第十章形式化方法

软件工程第十章形式化方法

第十章形式化方法形式化方法提供了规约环境的基础，它使得所生成的分析模型比用传统的或面向对象的方法生成的模型更完整、一致和无二义性。集合论和逻辑符号的描述设施使得我们可以创建清晰的关于事实的陈述。第2页,共105页，2024年2月25日，星期天支配形式化方法的基本概念是：数据不变式、状态、离散数学、序列相关联的符号体系、形式化规约语言。第3页,共105页，2024年2月25日，星期天10.1形式化方法形式化方法的定义定义10—1：用于开发计算机系统的形式化方法是描述系统性质的基于数学的技术。这样的形式化方法提供了一个框架，人们可以在框架中以系统的方式刻划、开发和验证系统。第4页,共105页，2024年2月25日，星期天形式化方法主要思想利用形式化规格说明语言定义用户需求，并采用数学推演的方法证明需求定义的性质，例如一致性、实时系统的活性和公平性等。对于复杂的应用问题，尽管无法验证整个需求定义的完全性，但仍有可能为避免某些要点的疏漏而建立数学断言，然后予以形式证明或反驳。第5页,共105页，2024年2月25日，星期天形式化方法是克服需求分析阶段不精确性、不一致性和不完全性的有效途径。第6页,共105页，2024年2月25日，星期天10.1.1形式化方法概念

例10--1：符号表(如右图)：它由一组没有重复的项构成。程序被用于维护一个符号表，在许多不同类型的应用中使用此符号表。第7页,共105页，2024年2月25日，星期天如果对于上表有一个陈述：包括不多于Max2D的用户名，那么就为表设定了一个限制，这就称为数据不变式的条件的一个构成成分。数据不变式是一个条件，它在包含一组数据的系统的执行过程中总保持为真。第8页,共105页，2024年2月25日，星期天上面讨论的符号表的数据不变式有两个构成成分：(1)表中包含的名字数不超过MaxIds。(2)在表中没有重复的名字。第9页,共105页，2024年2月25日，星期天状态的概念 在形式化方法的语言环境中，状态是系统访问和修改的存储数据。在上述符号表程序的例子中，状态是符号表。操作的概念 这是在系统中发生的读或写状态数据的动作。第10页,共105页，2024年2月25日，星期天10.1.2数学知识1.集合和构造性规约 所谓集合，乃是有某些可以相互区分的如何对象，如数、变量、函数、字母、数字、图、语言、程序、事件等，或者没有任何对象，汇集在一起所组成的整体。第11页,共105页，2024年2月25日，星期天例10--2：一个包含4个元素的自然数集合： ｛1，3，5，7｝例10--3：包含五种程序设计语言的名字的集合： ｛C，C＋＋，Pascal，Basic，FORTRAN｝例10--4：下面的数的聚集不是集合，因为它包含了重复的元素2： ｛33，2，99，11，22，88，2｝第12页,共105页，2024年2月25日，星期天

在集合中，元素出现的顺序是不重要的。我们将集合中元素的数量称为集合的基数(cardinality)，并用操作符#返回集合的基数。

例10--5：表达式说明用于已知集合的基数操作符，其结果指出集合中项的数量： ＃｛A，B，C，D｝＝4第13页,共105页，2024年2月25日，星期天

如果要定义一个集合，可以通过枚举出集合的元素来定。也可以是创建一个构造性集合规约，这种方式是用布尔表达式来刻划集合成员的一般形式。例10--6：下面是一个构造性规约的例子： ｛n：N｜n＜5·n｝第14页,共105页，2024年2月25日，星期天

这个规约中有三个部分： ①：基调n：N； ②：谓词n＜5； ③：项n。 基调刻划在形成集合时考虑的值的范围，谓词定义集合如何被构造，项则给出集合中项的一般形式。

第15页,共105页，2024年2月25日，星期天2.集合运算符 用命题法定义两个集合的运算。 定义10--2设A，B为任意两个集合。令

A∪B={x│x∈A或x∈B}A∩B={x│x∈A和x∈B}A－B={x│x∈A且xB}AB=（A∪B）－（A∩B）第16页,共105页，2024年2月25日，星期天集合的运算可以用文氏图如图直观地表示。图中的阴影部分表示运算的结果。第17页,共105页，2024年2月25日，星期天第18页,共105页，2024年2月25日，星期天3．笛卡尔乘积

4.逻辑运算符

4.序列

第19页,共105页，2024年2月25日，星期天10.1.3应用数学符号描述形式规约例10--18：块处理器在操作系统中一个更重要的部分是维护由用户创建的文件的子系统，块处理器是文件子系统中的一部分。文件存储中的文件由存储设备上的存储块构成，在计算机的操作中，文件被创建和删除，需要存储块的获取和释放。为了处理这些，文件子系统维持一个未用块池，并将保持对当前使用块的跟踪。当块从被删除文件释放时，它们通常被加入到等待进入未用块池的块队列中。如图所示.第20页,共105页，2024年2月25日，星期天第21页,共105页，2024年2月25日，星期天

对这个子系统而言，状态是自由块的集合、已用块的集合、以及返回块的队列，数据不变式用自然语言表达如下：第22页,共105页，2024年2月25日，星期天

1.没有块同时被标记为未用和已用。

2.所有在队列中的块集合将是当前已用块集合的子集。

3.没有队列元素包含相同的块号。第23页,共105页，2024年2月25日，星期天4.已用块和未用块的集合将是组成文件的块的总集。

5.在未用块集合中没有重复的块号。

6.在已用块集合中没有重复的块号。第24页,共105页，2024年2月25日，星期天和子系统关联的某些操作如下：

1.将一个块集合加到队列尾。

2.从队列前面移走一个已用块集合并将其放到未用块集合中。

3.检查是否块队列为空。第25页,共105页，2024年2月25日，星期天描述块处理器的不变式有如下一组条件：

1.没有块同时被标记为未用和已用。

2.所有在队列中的块集合将是当前已用块集合的子集。

3.在未用块集合中没有重复的块号。第26页,共105页，2024年2月25日，星期天4.没有队列元素包含相同的块号。

5.已用块和未用块的集合将是组成文件的块的总集。

6.在已用块集合中没有重复的块号。第27页,共105页，2024年2月25日，星期天10.1.4形式化规约语言形式化规约语言通常由三个主要的成分构成：

(1)语法，定义用于表示规约的特定符号；

(2)语义，帮助定义用于描述系统的“对象的全域(universeofobjects)”；

(3)一组关系，定义确定出哪个对象真正满足规约的规则。第28页,共105页，2024年2月25日，星期天形式化规约语言的语法域通常基于从标准集合论符号和谓词演算导出的语法。第29页,共105页，2024年2月25日，星期天10.2有限状态机（FSM）很多实时系统，特别是实时控制系统，其整个分析机制与系统的状态有相当大的关系。有限状态机由有限的状态和相互之间的转移构成，在任何时候只能处于给定数目的状态中的一个。第30页,共105页，2024年2月25日，星期天当接收到一个输入事件时，状态机产生一个输出，同时也可能伴随着状态的转移。主要有两种方法来建立有限状态机，一种是"状态转移图"，另一种是"状态转移表"，分别用图形方式和表格方式建立有限状态机。第31页,共105页，2024年2月25日，星期天有限状态机的组成如下：（1）一个有限的状态集合Q

（2）一个有限的输入集合I

（3）一个变迁函数δ：Q×I→Q变迁函数也是一个状态函数，在某一状态下，给定输入后，FSM转入该函数产生的新状态。δ的定义域内的某些数值可以是未定义的。第32页,共105页，2024年2月25日，星期天下图示意了一个简单的有限状态机。左图表明该FSM有q0、q1、q2、q3四个状态，输入集中有a、b、c三个元素；右图中各个状态之间的转换关系则更清晰。第33页,共105页，2024年2月25日，星期天第34页,共105页，2024年2月25日，星期天有限状态机的优点在于简单易用，状态间的关系能够直观看到。第35页,共105页，2024年2月25日，星期天有限状态机应用在实时系统中时，其最大的缺点是：任何时刻系统只能有一个状态，无法表示并发性，不能描述异步并发的系统。另外，在系统部件较多时，状态数随之增加，导致复杂性显著增长。第36页,共105页，2024年2月25日，星期天10.3Petri网概念Petri网是在软件分析中，用一种系统的数学和图形的描述与分析的方法。对于具有并发、异步、分布、并行、不确定性或随机性的信息处理系统，都可以利用Petri网方法构造出要开发的Petri网模型。第37页,共105页，2024年2月25日，星期天由于Petri网的表示手法是用图形工具。因此其表示形式与传统方法的结构图、流程图具有同样的直观、形象效果。第38页,共105页，2024年2月25日，星期天Petri网可以建立状态方程、代数方程以及系统行为的其他数学模型。因此，系统开发人员和理论研究工作者都可以根据需要利用Petri网。第39页,共105页，2024年2月25日，星期天10.3.1静态结构Petri网理论认为，任何系统是由两类基本元素组成：一类是表示状态的元素，另一是表示状态变化的元素。第40页,共105页，2024年2月25日，星期天在Petri网中，表示状态的元素用位置（place）表示，表示状态变化的元素用转移（transition）表示。转移的作用是改变状态，位置的作用是决定转移能否发生。将状态的元素和状态变化的元素两者间的这种依赖关系用弧（箭头）表示出来就是一个Petri网。第41页,共105页，2024年2月25日，星期天Petri网的基本成份可以表示为一个三元组：

N=（P，T；F）并满足以下条件：（1）P∪T≠ф

（2）P∩T=ф

（3）F（P×T）∪（T×P）（4）DOM（F）∪COD（F）=P∪T第42页,共105页，2024年2月25日，星期天例：N的Petri网

N=（P，T；F）

P={p1，p2，p3，p4，p5，p6}T={t1，t2，t3，t4，t5，t6}F={（p1，t1），（t1，p2），（p2，t2），（t2，p1），（p1，t3），（t3，p3），（t3，p4），（p3，t4），（p4，t5），（t4，p5），（t5，p6），（p5，t6），（p6，t6），（t6，p6）}N的Petri网图形表示如下图所示。第43页,共105页，2024年2月25日，星期天第44页,共105页，2024年2月25日，星期天10.3.2动态特征在用Petri网作为系统分析和建模工具时，除了具有描述的静态结构的能力外，还包括位置容量以及转移启动对位置容量的影响信息。第45页,共105页，2024年2月25日，星期天如果对于位置容量的有限容量用大于零的整数表示。转移启动对位置中标记数的影响用弧上的整数表示。那么，于是具有动态特征的Petri网就可以表示为六元组：∑=（P，T；F，K，W，M0）第46页,共105页，2024年2月25日，星期天例：具有M0和W的Petri网可以表示为下图所示。第47页,共105页，2024年2月25日，星期天第48页,共105页，2024年2月25日，星期天对于上图所示的Petri网，

M0=（1，0，0，0，0，0）

W（t2，p1）=W（t5，p6）

=W（t6，p1）

=4W（t3，p3）=6W（t4，p5）=5

第49页,共105页，2024年2月25日，星期天W（p1，t3）=W（p3，t4）

=W（p5，t6）

=（p6，t6）

=W（t3，p4）

=W（p4，t5）

=W（p1，t1）

=W（t1，p2）

=W（p2，t2）=1第50页,共105页，2024年2月25日，星期天10.3.3转移启动规则前面介绍的Petri网的动态特征是Petri网的动态行为的特性描述。这种动态行为是通过转移启动引起标识改变的变化来体现的。而转移启动则要有可以启动转移（转移有效）的条件和启动规则。第51页,共105页，2024年2月25日，星期天

（1）转移t有效的条件（2）转移t启动的结果第52页,共105页，2024年2月25日，星期天我们以下图为例说明转移启动规则。第53页,共105页，2024年2月25日，星期天第54页,共105页，2024年2月25日，星期天为了说明“并发”和“冲突”这两个概念，我们用图10--9所示的Petri网来表示“混惑”。第55页,共105页，2024年2月25日，星期天第56页,共105页，2024年2月25日，星期天有了这些基本概念后，就可以对于“并发”和“冲突”两个概念的完整描述。第57页,共105页，2024年2月25日，星期天1.并发设M为Petri网∑的一个标识，若存在t1和t2使得M[t1＞和M[t2＞，并满足M[t1＞M1M1[t2＞，且M[t2＞M2M[t1＞，则称t1和t2在M下并发。第58页,共105页，2024年2月25日，星期天2.冲突设M为Petri网∑的一个标识，若存在t1和t2使得M[t1＞和M[t2＞，并满足M[t1＞M1

]M1[t2＞，且M[t2＞M2]M2[t1＞，则称t1和t2在M下冲突，说是说在M标识下，t1和t2都有效，但t1和t2中只有一个能启动，而且其中任一个转移启动都会使另一个转移无效。第59页,共105页，2024年2月25日，星期天10.3.4行为特性行为特性包括：

1、可达性

2、有界性

3、活性

4、可逆性第60页,共105页，2024年2月25日，星期天5、可覆盖性

6、持久性

7、同步距离

8、公平性第61页,共105页，2024年2月25日，星期天10.3.5行为特性分析方法行为特性分析方法分为三类：（1）可覆盖性（可达性）树。（2）矩阵方程求解。（3）分层或化简。第62页,共105页，2024年2月25日，星期天用不变性、关联矩阵和状态方程的分析方法，就是完全用代数计算对网系统进行分析的方法。第63页,共105页，2024年2月25日，星期天不变量所谓不变量是指网系统中有S-不变量和T-不变量。下面几个图显示的是不变量的Petri网。第64页,共105页，2024年2月25日，星期天第65页,共105页，2024年2月25日，星期天第66页,共105页，2024年2月25日，星期天第67页,共105页，2024年2月25日，星期天2.状态方程如果N=（P，T；F）是纯网，则C与N存在一一对应的关系。第68页,共105页，2024年2月25日，星期天3.关联矩阵正如网系统的标识可以表示为一个向量一样，网结构也可以用一个矩阵来表示。第69页,共105页，2024年2月25日，星期天10.3.6结构特性分析方法Petri网有它的的拓扑结构。结构特性依赖于Petri网的拓扑结构。这些特性适合于网的任何初始标识，也就是说这些特性是独立于网的初始标识M0的。因此，这些特性通常可以用关联矩阵C及其相关的齐次方程或不等式来刻划。第70页,共105页，2024年2月25日，星期天对于Petri网N，我们引入如下几种结构特性：1.结构活性若N存在一个活的初始标识，则称N为结构活的。2.完全可控性若N的任何标识都可从N的任一其他标识到达，则称N为完全可控的。3.结构有界性若N对任何有限的初始标识M0都是有界的，则称N为结构有界性。第71页,共105页，2024年2月25日，星期天定理一：Petri网N是结构有界的，当且仅当存在一个m维正整数向量Y，使得CY≤0。第72页,共105页，2024年2月25日，星期天推论：N中位置pi是结构无界的，当且仅当存在一个非负整数n维向量X，使得CTX=△M＞≠0，其中的△M第i项大于0（即△M（pi）＞0）。第73页,共105页，2024年2月25日，星期天4.守恒性若N的每一（某些）位置p存在一个正整数Y（p），使得对任何给定的初始标识M0和每个M∈R（M0），都有标识的加权和MTY=M0TY为一个常量，则称N为（部分）守恒的。第74页,共105页，2024年2月25日，星期天定理二：Petri网是（部分）守恒的，当且仅当存在一个正的（非负）整数m维向量Y，满足CY=0，Y≠0。第75页,共105页，2024年2月25日，星期天5.重复性若N存在一个标识M0和一个从M0开始的启动序列σ，使得每个（某些）转移在σ中可以无限次发生，则称N为（部分）重复的。第76页,共105页，2024年2月25日，星期天定理三：Petri网N是（部分）重复的，当且仅当存在一个正的（非负）整数n维向量x，使得CTX≥0，X≠0。第77页,共105页，2024年2月25日，星期天6.一致性若N存在一个标识M0和一个从M0返回到M0的启动序列σ，使得每个（某些）转移在σ中至少出现一次，则称N为（部分）一致的。第78页,共105页，2024年2月25日，星期天定理四：Petri网N是（部分）一致的，当且仅当存在一个正的（非负）整数n维向量X，便得CTX=0，X≠0第79页,共105页，2024年2月25日，星期天10.3.7Petri网到程序结构的转换1.流程图的方法传统方法的流程图方法主要用于顺序软件开发的详细设计阶段的建模与分析。如果把并行处理退化为只有一个单进程的软件系统，用Petri网表示，那么传统方法的流程图方法也可以用于并行软件的开发。第80页,共105页，2024年2月25日，星期天2.编程语言的方法除了流程图与Petri网互相转换的方法外，也可以用编程语言转换。但是编程语言（如Ada、C++等）必须选用具有并发机制。用具有并发机制编程语言与Petri网两者之间建立起恰当的联系，这样就可以实现从Petri网到编程语言的转换。第81页,共105页，2024年2月25日，星期天3.面向对象的程序设计方法面向对象最适合用于Petri网的描述与分析，因为对象把数据和施加于这些数据上的私有操作封装在一起。操作名列在封装对象的界面上，当其他对象要“启动”该对象某个操作时，则以操作名发一条消息，该对象接受了消息，操作即动作起来，完成对私有数据的加工。第82页,共105页，2024年2月25日，星期天10.4净室方法学净室软件工程(Cleanroomsoftwareengineering)是一种在软件开发过程中强调在软件中建立正确性的需要的方法。代替传统的分析、设计、编码、测试和调试周期，净室方法建议一种不同的观点：通过在第一次正确地书写代码增量并在测试前验证它们的正确性来避免对成本很高的错误消除过程的依赖。它的过程模型是在代码增量积聚到系统的过程的同时进行代码增量的统计质量验证。第83页,共105页，2024年2月25日，星期天

10.4.1净室方法对软件工程的净室哲学首先由Mill和其同事于1980年代提出，虽然对这个严格的软件开发方法的早期经验显示了很大的希望，但它并没有得到广泛的使用，主要是由于下面的原因：第84页,共105页，2024年2月25日，星期天1.净室方法学太理论、太数学，以至难于在真实的软件开发中使用。

2.不需要进行单元测试，而是进行正确性验证和统计质量控制，与当前大多数软件开发方式背离。

3.软件开发产业的成熟度。第85页,共105页，2024年2月25日，星期天

10.4.2净室过程模型净室方法使用增量软件模型的一个专门版本。一个“软件增量的流水线”被若干小的、独立的软件工程小组开发，一旦每个增量被认证通过，它将被集成为一个整体。因此，系统的功能随时间增加。对每个增量的净室任务序列如图所示。第86页,共105页，2024年2月25日，星期天第87页,共105页，2024年2月25日，星期天

10.4.3功能规约净室软件工程通过使用称为盒结构规约的方法来遵从操作分析原则。从在顶层的本质表示转移向在底层的实现特定的细节。有三种盒类型：第88页,共105页，2024年2月25日，星期天黑盒。这种盒刻划系统或系统的某部分的行为。通过运用由激发得到反应的一组变迁规则，系统(或部分)对特定的激发(事件)作出反应。第89页,共105页，2024年2月25日，星期天状态盒。这种盒以类似于对象的方式封装状态数据和服务(操作)。在这个规约视图中，表示出状态盒的输入(激发)和输出(反应)。状态盒也表示黑盒的“激发历史”，即，封装在状态盒中的、必须在蕴含的变迁间保留的数据。第90页,共105页，2