计算机科学与技术方法论课件

《计算机科学与技术方法论课件》由会员分享，可在线阅读，更多相关《计算机科学与技术方法论课件（93页珍藏版）》请在金锄头文库上搜索。

1、计算机科学与技术方法论 专题讲座计算机科学与技术方法论课件计算机科学与技术方法论课件软件开发中的形式化方法 n n1 形式化技术的产生和发展n n2 软件开发中为什么使用形式化方法n n3 形式化规格技术n n4 形式化验证技术n n5 小结计算机科学与技术方法论课件计算机科学与技术方法论课件1 形式化技术的产生和发展 自20世纪60年代末以来，许多学者开展了形式化技术的相关研究。形式化技术最早是从戴克斯特拉和霍尔（C.Hoare）在程序验证方面的工作和斯科特（D.S.Scott）以及其他学者在程序语义方面的工作发展起来的。现在，形式化技术已经成为计算机科学的一个重要分支和研究领域，其作用相当

2、于传统工程设计（如计算流体动力学，CFD）在航空设计中的作用。计算机科学与技术方法论课件计算机科学与技术方法论课件1 形式化技术的产生和发展n n近些年来，形式化技术的学术研究及其工业应用得到了长足的发展。研究人员建立了系统设计人员易于理解的规格概念和术语，以及有效应用这些术语和概念的形式化规格技术及语言，建立了功能更加强大和完善的模型验证和定理证明技术，并开发出了与之相应的从研究原型到商品化产品的支撑工具和环境。计算机科学与技术方法论课件计算机科学与技术方法论课件1 形式化技术的产生和发展n n尽管当前对大型复杂的系统进行完整的形式化验证还不现实，但把形式化技术应用于大型复杂系统的关键部分确

3、实是一个有效的实用策略。目前，有效的模型检验和定理证明技术已成为硬件验证中传统仿真技术的补充，而软件开发工程师们开始使用更为严格的形式化规格及验证技术，成功地完成了过程控制领域工业规模系统的设计，通信系统中大量的安全可靠通信协议得到了测试和检验。计算机科学与技术方法论课件计算机科学与技术方法论课件1 形式化技术的产生和发展n n形式化技术成功的工业应用引起了人们的普遍关注，可以预计，在未来的工业应用系统开发中，形式化技术将会发挥越来越重要的作用。计算机科学与技术方法论课件计算机科学与技术方法论课件软件开发中的形式化方法 n n1 形式化技术的产生和发展n n2 软件开发中为什么使用形式化方法n

4、 n3 形式化规格技术n n4 形式化验证技术n n5 总结计算机科学与技术方法论课件计算机科学与技术方法论课件2 软件开发中为什么使用形式化方法n n（1）保证质量的需要n n（2）节约成本的需要n n（3）形式方法和复用n n（4）英国国防部的标准n n（5）经典案例计算机科学与技术方法论课件计算机科学与技术方法论课件（1）保证质量的需要n n 为了得到高质量的软件，我们强烈地希望使用软件工程中最好的实践。软件中存在的缺陷至少会引起客户的愤怒，而在更坏的情况下可能会给客户的业务造成较大的破坏或者造成生命损失。因此，企业要采用最好的实践，使他们的软件过程变得成熟起来。形式方法是一种前沿技术，

5、研究表明，这种技术非常有助于那些希望把软件产品的缺陷出现率减到最小的公司。计算机科学与技术方法论课件计算机科学与技术方法论课件（2）节约成本的需要n n有证据显示，形式方法的使用减少了项目成本。例如，IBM的大型CICS事务处理项目的独立审核表明，9的成本节约要归功于形式方法的使用。对T800型变换计算机的Inmos浮点单元的独立审核也证明，形式方法的使用估计可以减少12个月的测试时间。 计算机科学与技术方法论课件计算机科学与技术方法论课件（3）形式方法和复用n n有效的软件复用有助于提高软件开发的生产率，这在应用软件的快速开发中具有特殊的意义。n n软件复用的思想是开发出可在未来项目中使用的

6、基本部件，这就要求部件具有高质量和高可用性，而且部件的实际行为和使用环境也要具备一个文档化的描述。计算机科学与技术方法论课件计算机科学与技术方法论课件（3）形式方法和复用n n 形式方法在软件复用中也占有一席之地，因为它形式方法在软件复用中也占有一席之地，因为它可提高部件正确性的置信度，并对某个部件的行可提高部件正确性的置信度，并对某个部件的行为进行明确的形式描述。可以对部件进行广泛的为进行明确的形式描述。可以对部件进行广泛的测试，以便为部件的正确性提供更高的置信度。测试，以便为部件的正确性提供更高的置信度。一个部件一般会在不同的环境中使用，而部件在一个部件一般会在不同的环境中使用，而部件在某

7、种条件下能正常运转并不能保证它在未来也能某种条件下能正常运转并不能保证它在未来也能够成功运转，因为这个部件和其他部件或其他软够成功运转，因为这个部件和其他部件或其他软件之间可能存在着潜在的不良相互作用。因此，件之间可能存在着潜在的不良相互作用。因此，我们希望部件的行为能够得到明确的规定和充分我们希望部件的行为能够得到明确的规定和充分的了解，并对部件的构成进行形式分析，以确保的了解，并对部件的构成进行形式分析，以确保风险最小化，并在最后得到高质量的软件。风险最小化，并在最后得到高质量的软件。计算机科学与技术方法论课件计算机科学与技术方法论课件（3）形式方法和复用n n学术界和工业界都对部件的形式

8、化进行了研究；作为欧洲RACE计划的一部分，EC SCORE研究项目考虑了复用中亟待解决的问题。它包括部件的形式规范以及实际的部件模型的开发。该项目还考虑了电信环境中存在的特征交互问题。这验证了形式方法可以成功地用于特征交互的确定和消除。显然形式方法也对确定和消除部件间的不良交互起了一定的作用。计算机科学与技术方法论课件计算机科学与技术方法论课件（4）英国国防部的标准 n n在某些环境下，形式方法的使用是强制性的。英国国防部在20世纪90年代初期发行了两种与软件开发生命周期中使用形式方法有关的安全至上标准。 计算机科学与技术方法论课件计算机科学与技术方法论课件（4）英国国防部的标准n n第一个

9、标准是防卫标准(Defense Standard)0055，即Def Stan00-55 n n另一个防卫标准是Def Stan 00-56计算机科学与技术方法论课件计算机科学与技术方法论课件（4）英国国防部的标准n nDef Stan00-55标准要求英国在安全至上的软件开发中强制采用形式方法：尤其要提到的是，它要求强制使用形式数学来证明最为关键的程序正确地实现了他们的规范。 n nDef Stan 00-56标准的目标是提供指南，以便确定哪一个系统或系统的哪一个部分是安全至上的，然后要求在这些系统中使用形式方法。计算机科学与技术方法论课件计算机科学与技术方法论课件（4）英国国防部的标准n

10、n这两个标准表明了英国国防部采用的安全措施有多么严格，Brown在文献中提出：n n在导弹系统表明其安全之前，我们必须假设它处于危险状况中，没有危险错误存在的证据并不等于没有危险。计算机科学与技术方法论课件计算机科学与技术方法论课件（5）经典案例及应用n n典型应用系统包括：IBM商用信息控制系统、英国伦敦空中交通管理系统、空中交通防碰撞系统TCAS等。计算机科学与技术方法论课件计算机科学与技术方法论课件（5）经典案例及应用n n牛津大学和Hursley实验室于20世纪80年代合作将Z规格语言用于IBM商用信息控制系统。IBM对整个开发进行的测试表明，Z规格语言的应用明显地改善了产品质量、大量

11、减少了错误和早期诊断错误。IBM估计使总体开发成本降低9。这一成果获皇家技术成就奖。计算机科学与技术方法论课件计算机科学与技术方法论课件（5）经典案例及应用n nPraxisPraxis公司于公司于19921992年交付给英国民航局的信息显年交付给英国民航局的信息显示系统是伦敦机场新空中交通管理系统的一部分。示系统是伦敦机场新空中交通管理系统的一部分。在该系统的需求分析阶段，形式化描述和非形式在该系统的需求分析阶段，形式化描述和非形式结构化的需求概念相结合；在系统规格阶段，采结构化的需求概念相结合；在系统规格阶段，采用了抽象的用了抽象的VDMVDM模型；在设计阶段，抽象模型；在设计阶段，抽象V

12、DMVDM细细化为更为具体的规格。项目开发的生产效率和采化为更为具体的规格。项目开发的生产效率和采用非形式化技术相当，甚至更好。同时，软件质用非形式化技术相当，甚至更好。同时，软件质量得到了很大的提高，软件的故障率仅为量得到了很大的提高，软件的故障率仅为0.750.75每每千行代码，大大低于采用非形式化技术所提供的千行代码，大大低于采用非形式化技术所提供的软件的故障率（约为软件的故障率（约为220220每千行代码）。每千行代码）。计算机科学与技术方法论课件计算机科学与技术方法论课件（5）经典案例及应用n n加州大学的安全关键系统研究组所开发的空中交通防碰撞系统的形式化需求规格TCASII，采用

13、了基于Statecharts的需求状态机语言RSML，解决了开发过程中遇到的许多问题。TCASII项目表明了复杂过程控制系统列写形式化需求规格的可能性以及应用工程师们不经任何专门培训建立易读且易评判的形式化规格的可行性。计算机科学与技术方法论课件计算机科学与技术方法论课件（5）经典案例及应用n n除此之外还有：除此之外还有： （1）数据库：用于存储病人监护信息的HP 医用仪器实时数据库系统。 （2）核反应堆系统：核反应器安全系统、 核发电系统的切换装置。 （3）电信系统：AT&T的5ESS电话交换系 统、德国电信的电话业务系统。计算机科学与技术方法论课件计算机科学与技术方法论课件（5）经典案例

14、及应用（4）保密系统：NATO控制指挥和控制系统 中的保密策略模型、Multinet网关系统 的数据安全传输、美国国家标准和技术 院的令牌访问控制系统。（5）通信协议：协议规格、测试集的生成、 协议转换。计算机科学与技术方法论课件计算机科学与技术方法论课件（5）经典案例及应用（6）运输系统：巴黎地铁的自动火车保护 系统、英国铁路信号控制、以色列机 载航空电子软件。计算机科学与技术方法论课件计算机科学与技术方法论课件软件开发中的形式化方法 n n1 形式化技术的产生和发展n n2 软件开发中为什么使用形式化方法n n3 形式化规格技术n n4 形式化验证技术n n5 总结计算机科学与技术方法论课

15、件计算机科学与技术方法论课件3 形式化规格技术n n3.1 形式化规格的定义n n3.2 形式化规格的分类n n3.3 操作类规格技术 n n3.4 描述类规格技术 n n3.5 双重类规格技术计算机科学与技术方法论课件计算机科学与技术方法论课件3.1 形式化规格的定义n n规格就是对系统或者对象及其期望的特性或者行为进行的描述。规格所要描述的内容包括：功能特性、行为特性、结构特性、时间特性。功能特性侧重于系统的功能方面，即做什么；行为特性侧重于系统的具体行为演化，即如何做；结构特性侧重于系统的组成，各个组成部分或者子系统间的联系和复合；时间特性则是时间相关的系统特性。计算机科学与技术方法论课

16、件计算机科学与技术方法论课件3.1 形式化规格的定义n n形式化规格就是通过具有明确数学定义的文法和语义的语言实现以上描述。计算机科学与技术方法论课件计算机科学与技术方法论课件3 形式化规格技术n n3.1 形式化规格的定义n n3.2 形式化规格的分类n n3.3 操作类规格技术 n n3.4 描述类规格技术 n n3.5 双重类规格技术计算机科学与技术方法论课件计算机科学与技术方法论课件3.2 形式化规格的分类n n形式化规格技术可分为：操作类、描述类和双重形式化规格技术可分为：操作类、描述类和双重类。类。n n操作类技术基于状态和迁移，因其本质上可执行，操作类技术基于状态和迁移，因其本质

17、上可执行，故具有直观和可视的特点；描述类技术基于数学故具有直观和可视的特点；描述类技术基于数学公理和概念，通过逻辑和代数给出系统的状态空公理和概念，通过逻辑和代数给出系统的状态空间，具有高度抽象、便于通过自动工具进行验证间，具有高度抽象、便于通过自动工具进行验证的特点；双重类技术则兼有二者的特点，既能够的特点；双重类技术则兼有二者的特点，既能够通过数学公理和概念高度抽象描述系统，又具有通过数学公理和概念高度抽象描述系统，又具有状态和迁移的可执行特征。状态和迁移的可执行特征。计算机科学与技术方法论课件计算机科学与技术方法论课件3 形式化规格技术n n3.1 形式化规格的定义n n3.2 形式化规

18、格的分类n n3.3 操作类规格技术 n n3.4 描述类规格技术 n n3.5 双重类规格技术计算机科学与技术方法论课件计算机科学与技术方法论课件3.3 操作类规格技术 n n操作类技术通过可执行模型描述系统，即模型本身能够采用静态分析和执行模型得到验证。n n操作类技术侧重于系统行为的特性描述，主要包括：有限状态机及其扩展技术和Petri网技术等。2Petri网1有限状态机计算机科学与技术方法论课件计算机科学与技术方法论课件3.3.1有限状态机（1）产生背景（2）形式化定义（3）有限状态图的表示（4）“生产者与消费者”实例计算机科学与技术方法论课件计算机科学与技术方法论课件（1）产生背景n

19、 n有限状态机或者自动机的概念于20世纪50年代提出，包括Moore机和Mealy机。由于状态机本质上的可操作性，因而它成为多种操作模型的基础。经典的有限状态机（Moore机和Mealy机），可用来规格系统的行为特性，并具有状态迁移图和状态迁移矩阵两种表述方式。计算机科学与技术方法论课件计算机科学与技术方法论课件（2）形式化定义n n有限状态机FSM（Finite State Machine）是一种基本的、简单的、重要的形式化技术，它具有广泛的应用，可用于系统生命期中从系统规格到系统设计的所有阶段。直观地理解，有限状态机就是一个具有有限状态的机器。n n有限状态机是一个5元组M = (Q，q0

20、，F)，其中：计算机科学与技术方法论课件计算机科学与技术方法论课件（2）形式化定义n n QQ = = q q0 0，q q1 1，qnqn 是有限状态集合。在任一确是有限状态集合。在任一确定的时刻，有限状态机只能处于一个确定的状态定的时刻，有限状态机只能处于一个确定的状态qiqi；n n = = 1 1， 2 2， mm 是有限输入字符集合。在任一是有限输入字符集合。在任一确定的时刻，有限状态机只能接收一个确定的输入确定的时刻，有限状态机只能接收一个确定的输入 j j；n n ： QQ QQ是状态转移函数。在某一状态下，给定是状态转移函数。在某一状态下，给定输入后有限状态机将转入由状态迁移函

21、数决定的一个新的输入后有限状态机将转入由状态迁移函数决定的一个新的状态；状态；n n q q0 0QQ是初始状态，有限状态机由此状态开始接收输是初始状态，有限状态机由此状态开始接收输入；入；n n F F QQ是终结状态集合，有限状态机在达到终态后不再是终结状态集合，有限状态机在达到终态后不再接收输入。接收输入。计算机科学与技术方法论课件计算机科学与技术方法论课件（3）有限状态图的表示n n有限状态机通常用图来表示，图中节点代表状态，有向弧表示迁移关系，输入标注在相应的关系弧旁边。图1显示了一个简单的有限状态机，该状态机有4个状态q0、q1、q2和q3，输入集合有3个元素a、b和c。各个状态之

22、间的转移关系可从图中清楚地看出。计算机科学与技术方法论课件计算机科学与技术方法论课件（3）有限状态图的表示图7.1 有限状态机计算机科学与技术方法论课件计算机科学与技术方法论课件（4）“生产者与消费者”实例n n“生产者消费者”系统中，包含一个生产者和一个消费者。生产者进程产生消息，并把产生的消息写入一个能容纳两个消息的缓存区中。生产者在进行“生产”动作后，状态由P1转变为P2；而在“写”动作后，状态由P2恢复为P1。消费者进程能读取消息，并把消息从缓存器中取走。 计算机科学与技术方法论课件计算机科学与技术方法论课件（4）“生产者与消费者”实例n n消费者在进行消费者在进行“ “消费消费” ”

23、动作后，状态由动作后，状态由C1C1转变为转变为C2C2；而在；而在“ “读读” ”动作后，状态由动作后，状态由C2C2恢复为恢复为C1C1。如果缓存器是满的，那么生产者进程必须等待，如果缓存器是满的，那么生产者进程必须等待，直到消费者进程从缓存器中取出一个消息，使缓直到消费者进程从缓存器中取出一个消息，使缓存器产生一个消息空位。同样，如果缓存器是空存器产生一个消息空位。同样，如果缓存器是空的，那么消费者进程就必须等待，直到生产者进的，那么消费者进程就必须等待，直到生产者进程产生一个消息并把所产生的消息写入缓存器中。程产生一个消息并把所产生的消息写入缓存器中。缓存器在进行缓存器在进行“ “读读

24、” ”动作后，缓存器大小减动作后，缓存器大小减“1”“1”，而在，而在“ “写写” ”动作后，缓存器大小加动作后，缓存器大小加“1”“1”。计算机科学与技术方法论课件计算机科学与技术方法论课件（4）“生产者与消费者”实例n n利用有限状态机，分别对生产者、消费者和缓存器进行规格，如图2（a）、图2（b）和图2（c）所示。图中清楚地给出了两个进程和一个缓存器的描述，但是作为一个整体系统，我们还需要对系统的整体行为进行规格。在这里可以利用有限状态机的复合运算或者笛卡儿积运算，得到整个系统完整行为的有限状态机规格，如图2（d）所示。计算机科学与技术方法论课件计算机科学与技术方法论课件（4）“生产者与

25、消费者”实例计算机科学与技术方法论课件计算机科学与技术方法论课件（4）“生产者与消费者”实例计算机科学与技术方法论课件计算机科学与技术方法论课件（4）“生产者与消费者”实例计算机科学与技术方法论课件计算机科学与技术方法论课件（4）“生产者与消费者”实例图2 生产者消费者系统规格计算机科学与技术方法论课件计算机科学与技术方法论课件3.3 操作类规格技术 n n操作类技术通过可执行模型描述系统，即模型本身能够采用静态分析和执行模型得到验证。n n操作类技术侧重于系统行为的特性描述，主要包括：有限状态机及其扩展技术和Petri网技术等。2Petri网1有限状态机计算机科学与技术方法论课件计算机科学与

26、技术方法论课件2Petri网n n1962年，德国学者Petri（C.A.Petri）在他的博士论文用自动机通信（Communication with Automata）中首次使用了网状结构模拟通信系统。这种模型后来就被称为Petri网。后来研究人员不断拓展和丰富了Petri网理论。（1）形式化定义（2）图形表示（3）“生产者与消费者”实例计算机科学与技术方法论课件计算机科学与技术方法论课件（1）形式化定义n nPetri网是一个适合于研究具有并发、竞争、同步等特征行为的形式化技术。类似于有限状态机，Petri网也是一种使用图形方式对系统进行规格的技术。Petri网的描述能力强于有限状态机。n

27、 nPetri网可以定义为一个6元组N = ( P，T；F，K，W，M0 )，其中：计算机科学与技术方法论课件计算机科学与技术方法论课件（1）形式化定义n n P=P1，P2，Pm是一个有限库所集，用于表示系统中资源或者条件的状态；n n T=t1，t2，tn是一个有限变迁集，用于表示系统中的事件；n n F(PT)(TP)是一个有限的连接库所到变迁或者变迁到库所的有向弧或者关系的集合，表示事件发生的前提或者结果；计算机科学与技术方法论课件计算机科学与技术方法论课件（1）形式化定义n n K: P Z+为库所的容量函数（Z+位正整数集）；n n W：FZ+为权函数；n n M0为初始标识，用于

28、表示系统的初始状态（资源的初始分布）。n n上述Petri网的定义，在K 1和W 1时可简写为元组N = ( P，T；F，M0 )。计算机科学与技术方法论课件计算机科学与技术方法论课件（1）形式化定义n n托肯位于库所中，所有库所中托肯的分布称为标托肯位于库所中，所有库所中托肯的分布称为标识，标识用于表示系统的状态，它会随着变迁的识，标识用于表示系统的状态，它会随着变迁的发生而重新分布，从而表征系统的动态行为。发生而重新分布，从而表征系统的动态行为。n n 与状态机相比，与状态机相比，PetriPetri网具有更强的描述能力，它网具有更强的描述能力，它克服了状态机不能描述并发的缺陷。事实上，状

29、克服了状态机不能描述并发的缺陷。事实上，状态机可看作态机可看作PetriPetri网的一类特殊的有向图，其中含网的一类特殊的有向图，其中含有两种节点：库所和变迁。库所节点和变迁节点有两种节点：库所和变迁。库所节点和变迁节点间用有向弧联系，这种联系可以用变迁矩阵表示。间用有向弧联系，这种联系可以用变迁矩阵表示。计算机科学与技术方法论课件计算机科学与技术方法论课件（1）形式化定义n n库所节点可以包含有托肯，变迁节点遵循使能规则可以引发，而引发的变迁将按照引发规则改变库所节点中托肯的分布，由此描述系统的动态行为演化。Petri网可以描述系统中的并发、同步、冲突等特性。 计算机科学与技术方法论课件计

30、算机科学与技术方法论课件（2）图形表示n n在图形表示中，用圆圈表示库所，用短线表示变迁，用有向弧表示关系，用圆点表示托肯。图3（a）为一简单的Petri网的示意图。该Petri网中，包含库所集合p1，p2，p3，p4，p5，p6，p7、变迁集合t1，t2，t3，t4，t5，t6，库所p1、p2和p3中均包含有1个托肯，库所和变迁之间的联系可从图中清楚地看出。计算机科学与技术方法论课件计算机科学与技术方法论课件（2）图形表示n n在图在图3 3（a a）中，变迁）中，变迁t1t1和和t2t2是使能的。在这种情是使能的。在这种情况下，该况下，该PetriPetri网的演化，即托肯的变化就可能存网

31、的演化，即托肯的变化就可能存在如下在如下3 3种不同方式：引发种不同方式：引发t1t1，引发，引发t2t2，或者引，或者引发发t1t1和和t2t2。也就是说，在给定。也就是说，在给定PetriPetri网的初始托肯网的初始托肯后，其演化过程可能是不同的，具有不确定性。后，其演化过程可能是不同的，具有不确定性。在图在图3 3（a a）的情况下，引发）的情况下，引发t1t1所得到的下一个状所得到的下一个状态如图态如图3 3（b b）所示；引发）所示；引发t2t2所得到的下一个状态所得到的下一个状态如图如图3 3（c c）所示；引发）所示；引发t1t1和和t2t2所得到的下一个状所得到的下一个状态如

32、图态如图3 3（d d）所示。在图）所示。在图7.37.3（b b）的情况下，变）的情况下，变迁迁t2t2和和t3t3使能。在引发变迁使能。在引发变迁t2t2后，将同样得到图后，将同样得到图3 3（d d）所示状态。在图）所示状态。在图3 3（c c）的情况下，变迁）的情况下，变迁t1t1和和t4t4使能。在引发变迁使能。在引发变迁t1t1后，将同样得到图后，将同样得到图3 3（d d）所示状态。）所示状态。 计算机科学与技术方法论课件计算机科学与技术方法论课件（2）图形表示图3 一个简单Petri网计算机科学与技术方法论课件计算机科学与技术方法论课件（2）图形表示图3 一个简单Petri网计

33、算机科学与技术方法论课件计算机科学与技术方法论课件（3）“生产者与消费者”实例n n我们也可以将Petri网应用于生产者消费者系统的规格。图4（a）、图4（b）、图4（c）、图4（d）依次为生产者、消费者、缓存器以及整个系统的Petri网规格。计算机科学与技术方法论课件计算机科学与技术方法论课件（3）“生产者与消费者”实例计算机科学与技术方法论课件计算机科学与技术方法论课件（3）“生产者与消费者”实例计算机科学与技术方法论课件计算机科学与技术方法论课件（3）“生产者与消费者”实例图4 生产者消费者系统计算机科学与技术方法论课件计算机科学与技术方法论课件n n对描述类规格技术和双重类规格技术仅简

34、单介绍 计算机科学与技术方法论课件计算机科学与技术方法论课件3 形式化规格技术n n3.1 形式化规格的定义n n3.2 形式化规格的分类n n3.3 操作类规格技术 n n3.4 描述类规格技术 n n3.5 双重类规格技术计算机科学与技术方法论课件计算机科学与技术方法论课件3.4 描述类规格技术n n描述类规格技术的数学基础是代数或者逻辑。此类技术具有数学上的严密性和高度抽象性，并通过做什么的方式进行系统性能规格。基于不同的数学基础，描述类规格技术进一步分为：基于代数的描述技术和基于逻辑的描述技术。1基于代数的描述技术2基于逻辑的描述技术计算机科学与技术方法论课件计算机科学与技术方法论课件

35、3.4.1 基于代数的描述技术n n基于代数的描述技术以抽象数据类型基于代数的描述技术以抽象数据类型ADTADT概念为概念为基础，可以对系统进行由粗到细的多层次抽象。基础，可以对系统进行由粗到细的多层次抽象。此类方法中，系统本身视为一个此类方法中，系统本身视为一个ADTADT，规格则在，规格则在于描述其文法和语义。文法定义给出于描述其文法和语义。文法定义给出ADTADT中算子中算子域的描述。语义则通过数学表达式给出这些算子域的描述。语义则通过数学表达式给出这些算子的执行，这些数学表达式的形式为用编程语言书的执行，这些数学表达式的形式为用编程语言书写的一组公理。复杂写的一组公理。复杂ADTADT

36、由简单由简单ADTADT定义，重复定义，重复进行则完成整个系统的规格，这样也就给后期的进行则完成整个系统的规格，这样也就给后期的验证带来方便。验证可以在各个层次的规格上进验证带来方便。验证可以在各个层次的规格上进行，复杂行，复杂ADTADT的特性可通过简单的特性可通过简单ADTADT特性的验证特性的验证而得到验证。而得到验证。计算机科学与技术方法论课件计算机科学与技术方法论课件3.4.1 基于代数的描述技术n n基于代数的描述技术主要有Z、LOTOS、VDM和Larch等。（1）Z语言（2）LOTOS（3）VDM（4）Larch计算机科学与技术方法论课件计算机科学与技术方法论课件（1）Z语言n

37、 n自20世纪70年代晚期，牛津大学的计算实验室和其他地方的程序设计研究组开发出Z语言，它基于集合和一阶谓词逻辑。Z语言中Z是指著名的数学家Zermolo，他的主要成就是集合论。Z语言中有称作为框架演算的系统分解机制，系统的规格分解为许多小的框架，这些框架则描述系统的静态和动态行为。Z规格为非形式化文本、定义、公理描述、约束、类型定义和框架的混合，其中的ADT操作采用谓词逻辑表述。 计算机科学与技术方法论课件计算机科学与技术方法论课件（1）Z语言n nZ语言本身并不支持时间约束定义，Z语言和实时区间逻辑RTIL结合则是在此方面的扩展。同时，Z语言也在面向对象方面进行了扩展，如：OOZE、Moo

38、Z、Z+和Object-Z等，这些扩展Z语言都将信息封装、继承、实例等引入了Z框架演算，这样系统的状态空间定义为单个系统对象状态空间的复合。Object-Z中还集成了时态逻辑，可以进行实时规格。 计算机科学与技术方法论课件计算机科学与技术方法论课件（2）LOTOSn n 从1981年到1988年，ISO的FDT（Formal Description Technique）小组的专家们开发了LOTOS（Language of Temporal Ordering Specifications），主要用于开放分布式系统形式化规格。现在的国际标准是IS8807。LOTOS可通过ADT概念定义系统所有结构

39、方面的特性。LOTOS中的进程概念非常突出，结构解耦基于进程，分布式系统视为含有子进程的进程。计算机科学与技术方法论课件计算机科学与技术方法论课件（2）LOTOSn n进程之间的关系通过代数算子定义，如：顺序和并行执行。进程之间通过消息和门通信，消息可携带有数据和控制。LOTOS下，系统规格在于定义进程行为，描述进程的通信、执行和同步，进程之间的时态顺序通过门定义。计算机科学与技术方法论课件计算机科学与技术方法论课件（3）VDMn n 自20世纪70年代早期，IBM实验室的研究小组提出了VDM（The Vienna Development Method），其初始目的在于建立一种定义编程语言PL

40、/I的形式化方法。目前VDM不仅是一种规格语言，而且成为了英国标准。VDM的数学基础是集合理论和谓词逻辑理论。 计算机科学与技术方法论课件计算机科学与技术方法论课件（3）VDMn n VDM VDM下的系统规格在于定义类型、函数和操作。下的系统规格在于定义类型、函数和操作。数据类型由异构的数据类型由异构的VDMVDM基本类型复合来定义，基本类型复合来定义，VDMVDM基本类型包括自然数、整数、布尔量等。对基本类型包括自然数、整数、布尔量等。对于新的类型，其操作可自动获得。函数定义为具于新的类型，其操作可自动获得。函数定义为具有变元的过程，返回结果。函数也可由其前、后有变元的过程，返回结果。函数

41、也可由其前、后条件来规格。操作作用于状态，这些状态基于操条件来规格。操作作用于状态，这些状态基于操作自身的前条件来择取。操作可以读、写外部事作自身的前条件来择取。操作可以读、写外部事件。件。VDMVDM模型没有定义系统结构的机制，数据类模型没有定义系统结构的机制，数据类型根据其他数据类型定义，不能够将系统分解为型根据其他数据类型定义，不能够将系统分解为相互通信的子系统。目前，相互通信的子系统。目前，VDMVDM也在时间特性处也在时间特性处理和面向对象方面得到了扩展。理和面向对象方面得到了扩展。计算机科学与技术方法论课件计算机科学与技术方法论课件（4）Larchn n arch arch族语言是

42、基于族语言是基于ADTADT的较早建立的规格语言之的较早建立的规格语言之一，它是一，它是LARCHLARCH项目的主要成果之一。它支持通项目的主要成果之一。它支持通过代数语言过代数语言LarchLarch共享语言描述公共共享语言描述公共LarchLarch模模型，使用该语言可以定义新的型，使用该语言可以定义新的ADTADT。LarchLarch共享共享语言的接口支持由一谓词语言定义，该接口起着语言的接口支持由一谓词语言定义，该接口起着支持主语言的作用。例如：支持主语言的作用。例如：Larch/PascalLarch/Pascal通过通通过通常的常的PascalPascal提供提供LarchLa

43、rch型编程。目前已有多种其型编程。目前已有多种其他他LarchLarch语言，如：语言，如：Larch/CLULarch/CLU、Larch/ADALarch/ADA、Larch/CLarch/C、Larch/SmalltalkLarch/Smalltalk、Larch/Modula-3Larch/Modula-3和和Larch/C+Larch/C+等。等。计算机科学与技术方法论课件计算机科学与技术方法论课件3.4 描述类规格技术n n描述类规格技术的数学基础是代数或者逻辑。此类技术具有数学上的严密性和高度抽象性，并通过做什么的方式进行系统性能规格。基于不同的数学基础，描述类规格技术进一步分

44、为：基于代数的描述技术和基于逻辑的描述技术。1基于代数的描述技术2基于逻辑的描述技术计算机科学与技术方法论课件计算机科学与技术方法论课件3.4.2 基于逻辑的描述技术n n基于逻辑的描述技术通过逻辑规则来规格系统的演化，与操作类技术不同的是规格所描述的系统状态空间是抽象和无限的。这些规则一般是一阶Horn子句或者高阶逻辑公式。这类技术不能够对系统的结构特性进行描述。时态逻辑是从命题逻辑基础上演变而来的，并通过引入时态算子实现对断言随时间变化进行的描述和解释。典型的时态算子包括always、sometimes、henceforth和eventually等。计算机科学与技术方法论课件计算机科学与技

45、术方法论课件3.4.2 基于逻辑的描述技术n n基于时态逻辑的描述规格技术主要有计算树逻辑CTL、实时区间逻辑RTIL、赋时计算树逻辑TCTL和赋时命题时态逻辑TPTL等。（1）实时逻辑RTL（2）TRIO计算机科学与技术方法论课件计算机科学与技术方法论课件（1）实时逻辑RTLn n实时逻辑RTL是一种描述事件和动作间时态关系的形式语言。RTL中有3种类型的常数：动作、事件和整数。动作可以是简单的或者复合的，复合动作可以是顺序的或者并发的。事件和动作类似于激励和响应，周期事件通过递归谓词规格。整数可以是时间常数或者时间数目。系统的RTL规格在于从事件动作模型推演出一组公理。RTL中，时间是绝对

46、的，执行语义和调度机制无关。计算机科学与技术方法论课件计算机科学与技术方法论课件（2）TRIOn nTRIO是在一阶逻辑基础上引入时态函数Dist(F,t)、Futr(F,t)和Past(F,t)的一种语言，事件之间的时态关系则可由这些函数的一阶逻辑公式表述。时间在这里是蕴涵表示的，所以难以规格绝对时间约束。计算机科学与技术方法论课件计算机科学与技术方法论课件3 形式化规格技术n n3.1 形式化规格的定义n n3.2 形式化规格的分类n n3.3 操作类规格技术 n n3.4 描述类规格技术 n n3.5 双重类规格技术计算机科学与技术方法论课件计算机科学与技术方法论课件3.5 双重类规格技

47、术n n理想的形式化规格技术，应该是既具有操作类技术的可执行性和可视性，又具有描述类技术的形式可验证性。双重类规格技术则是在此方面的努力，现有的此类规格技术包括：ESM/RTTL、TRIO+和TROL等。（1）ESM/RTTL（2）TRIO+（3）TROL计算机科学与技术方法论课件计算机科学与技术方法论课件（1）ESM/RTTLn nESM/RTTLESM/RTTL是一种集成扩展状态机是一种集成扩展状态机ESMESM语言和实语言和实时时态逻辑时时态逻辑RTTLRTTL的双重规格技术。的双重规格技术。ESMESM是一种扩是一种扩展展MealyMealy机模型，其中引入了变量，以及赋值、机模型，其

48、中引入了变量，以及赋值、发送和接受等操作。发送和接受等操作。ESMESM中状态的转移条件为状中状态的转移条件为状态变量的一阶表达式，输出为状态变量的赋值。态变量的一阶表达式，输出为状态变量的赋值。时间机制通过整体时间变量描述，时间是离散的，时间机制通过整体时间变量描述，时间是离散的，状态迁移是即时的。状态迁移是即时的。RTTLRTTL是一种在时态逻辑算子是一种在时态逻辑算子untiluntil和和nextnext基础上，增加了基础上，增加了EventuallyEventually和和HenceforthHenceforth算子而形成的规格技术。通过算子而形成的规格技术。通过RTTLRTTL的一

49、阶逻辑公式可对系统的功能特性进行描述。的一阶逻辑公式可对系统的功能特性进行描述。计算机科学与技术方法论课件计算机科学与技术方法论课件（2）TRIO+n n TRIO+是TRIO的面向对象扩展，将可视和递阶解耦结合到描述性逻辑语言。通过定义类构件及其关系，TRIO+能够描述系统的结构特性。同时，TRIO+是一个可执行模型。计算机科学与技术方法论课件计算机科学与技术方法论课件（3）TROLn n TROL是一种面向对象的双重规格语言，其中采用了修正面向对象模型，能够对系统行为、功能和结构特性进行描述。在TROL中，系统递阶解耦为对象和子对象，而不能进一步分解的对象定义为扩展状态机。状态机模型支持时

50、间约束描述。TROL语言的描述特征可用于系统的分析阶段，支持面向对象，包括继承和实例等。计算机科学与技术方法论课件计算机科学与技术方法论课件软件开发中的形式化方法 n n1 形式化技术的产生和发展n n2 软件开发中为什么使用形式化方法n n3 形式化规格技术n n4 形式化验证技术n n5 总结计算机科学与技术方法论课件计算机科学与技术方法论课件4 形式化验证技术n n形式化验证就是基于已建立的形式化规格，对所规格系统的相关特性进行分析和验证，以评判系统是否满足期望的特性。形式化验证并不能完全确保系统的性能正确无误，但是可以最大限度地理解和分析系统，并尽可能地发现其中的不一致性、模糊性、不完

51、备性等错误。形式化验证的主要技术包括模型验证和定理证明。计算机科学与技术方法论课件计算机科学与技术方法论课件4 形式化验证技术n n（1）模型检验n n（2）定理证明 计算机科学与技术方法论课件计算机科学与技术方法论课件（1）模型检验n n模型检验是基于有限模型并检验该模型的期望特性的一种技术。粗略地讲，检验就是状态空间的蛮力搜索，模型的有限性确保了搜索可以终止。n n模型检验有两种主要方法。其一是时态模型检验，该方法中规格以时态逻辑形式表述，系统模拟为有限状态迁移系统。有效的搜索过程用来检验给定的有限状态迁移系统是否是规格的一个模型。 计算机科学与技术方法论课件计算机科学与技术方法论课件（1

52、）模型检验n n另一种方法中，规格以自动机方式给出，系统也模拟为一个自动机。系统的自动机模型和规格比较，以确定其行为是否与规格的自动机模型一致。一致性概念已进行了广泛的研究，包括：语言包含、细化有序、观测等价等。n n不同于定理证明，模型检验是完全自动且高效的。模型检验可用于系统部分规格，因此可用于未完全规格的系统。计算机科学与技术方法论课件计算机科学与技术方法论课件（1）模型检验n n模型检验的主要局限性在于状态组合爆炸问题。模型检验的主要局限性在于状态组合爆炸问题。有序布尔决策图有序布尔决策图OBDDOBDD是表述状态迁移系统的高是表述状态迁移系统的高效率方法，使得较大规模系统的验证成为可

53、能。效率方法，使得较大规模系统的验证成为可能。其他可能改善状态组合复杂性的途径有利用偏序其他可能改善状态组合复杂性的途径有利用偏序信息、局部简化、语义最小、消除不必要状态等信息、局部简化、语义最小、消除不必要状态等几种。几种。n n目前，模型检验预计可以处理目前，模型检验预计可以处理100200100200个状态变个状态变量的系统。模型检验已用来检验状态数目可达量的系统。模型检验已用来检验状态数目可达1012010120的系统，并且通过采用适当的抽象技术就的系统，并且通过采用适当的抽象技术就可以处理本质上无限状态的系统。模型检验的技可以处理本质上无限状态的系统。模型检验的技术挑战在于设计可以处

54、理大型搜索空间的算法和术挑战在于设计可以处理大型搜索空间的算法和数据结构。数据结构。计算机科学与技术方法论课件计算机科学与技术方法论课件（1）模型检验n n模型检验的工业应用离不开模型检验器的支持。工业应用部门可以选取现有的模型检验器，也可以根据自身应用特点自行开发模型检验器。目前，学术和工业界已开发出了大量的模型检验器，根据所检验规格的特点可分为时态逻辑模型检验器、行为一致检验器和复合检验器。计算机科学与技术方法论课件计算机科学与技术方法论课件（2）定理证明n n定理证明是系统及其特性均以某种数学逻辑公式表示的技术。逻辑由一具有公理和推理规则的形式化系统给出。定理证明实质上是从系统公理中寻找

55、特性证明的过程。证明采用公理或者规则，且可能推演出定义和引理。不同于模型检验，定理证明可以处理无限状态空间问题。 计算机科学与技术方法论课件计算机科学与技术方法论课件（2）定理证明n n定理证明系统可粗略地分为自动的和交互的两种类型。自动定理证明系统是通用搜索过程，在解决各种组合问题中比较成功；交互式定理证明系统则更适合于系统的形式化开发和机械形式化。同样地，定理证明的实施也是需要定理证明器的支持。现有的定理证明器包括：用户导引自动推演工具、证明检验器和复合证明器。计算机科学与技术方法论课件计算机科学与技术方法论课件软件开发中的形式化方法 n n1 形式化技术的产生和发展n n2 软件开发中为什么使用形式化方法n n3 形式化规格技术n n4 形式化验证技术n n5 总结计算机科学与技术方法论课件计算机科学与技术方法论课件小结n n介绍了形式化技术的产生和分类n n简单说明了软件开发中使用形式化方法的原因，并通过经典的案例说明形式化方法在软件开发中的重要性n n分别对形式化规格技术和验证技术进行了介绍，通过经典的“生产者消费者”实例对有限状态机和Petri网进行了讲解计算机科学与技术方法论课件计算机科学与技术方法论课件