《软件工程第十章形式化方法课件.ppt》由会员分享，可在线阅读，更多相关《软件工程第十章形式化方法课件.ppt（105页珍藏版）》请在taowenge.com淘文阁网|工程机械CAD图纸|机械工程制图|CAD装配图下载|SolidWorks_CaTia_CAD_UG_PROE_设计图分享下载上搜索。
1、软件工程第十章形式化方法第1页，此课件共105页哦第十章第十章形式化方法形式化方法l形式化方法提供了规约环境的基础，它使得所生成的分析模型比用传统的或面向对象的方法生成的模型更完整、一致和无二义性。集合论和逻辑符号的描述设施使得我们可以创建清晰的关于事实的陈述。第2页，此课件共105页哦l支配形式化方法的基本概念是：数据不变式、状态、离散数学、序列相关联的符号体系、形式化规约语言。第3页，此课件共105页哦10.1形式化方法形式化方法l形式化方法的定义定义定义101：用于开发计算机系统的形式化方法是描述系统性质的基于数学的技术。这样的形式化方法提供了一个框架，人们可以在框架中以系统的方式刻划、
2、开发和验证系统。第4页，此课件共105页哦l形式化方法主要思想l利用形式化规格说明语言定义用户需求，并采用数学推演的方法证明需求定义的性质，例如一致性、实时系统的活性和公平性等。对于复杂的应用问题，尽管无法验证整个需求定义的完全性，但仍有可能为避免某些要点的疏漏而建立数学断言，然后予以形式证明或反驳。第5页，此课件共105页哦形式化方法是克服需求分析阶段不精确性、不一致性和不完全性的有效途径。第6页，此课件共105页哦l10.1.1形式化方法概念形式化方法概念例10-1：符号表(如右图)：它由一组没有重复的项构成。程序被用于维护一个符号表，在许多不同类型的应用中使用此符号表。第7页，此课件共1
3、05页哦l如果对于上表有一个陈述：包括不多于Max2D的用户名，那么就为表设定了一个限制，这就称为数据不变式的条件的一个构成成分。数据不变式是一个条件，它在包含一组数据的系统的执行过程中总保持为真。第8页，此课件共105页哦l上面讨论的符号表的数据不变式有两个构成成分：(1)表中包含的名字数不超过MaxIds。(2)在表中没有重复的名字。第9页，此课件共105页哦p状态的概念在形式化方法的语言环境中，状态是系统访问和修改的存储数据。在上述符号表程序的例子中，状态是符号表。p操作的概念这是在系统中发生的读或写状态数据的动作。第10页，此课件共105页哦l10.1.2数学知识数学知识1.集合和构造
4、性规约所谓集合，乃是有某些可以相互区分的如何对象，如数、变量、函数、字母、数字、图、语言、程序、事件等，或者没有任何对象，汇集在一起所组成的整体。第11页，此课件共105页哦例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页哦在集合中，元素出现的顺序是不重要的。我们将集合中元素的数量称为集合的基数(cardinality)，并用操作符#返回集合的基数。l例10-5：表达式说
5、明用于已知集合的基数操作符，其结果指出集合中项的数量：A，B，C，D4第13页，此课件共105页哦如果要定义一个集合，可以通过枚举出集合的元素来定。也可以是创建一个构造性集合规约，这种方式是用布尔表达式来刻划集合成员的一般形式。l例10-6：下面是一个构造性规约的例子：n：Nn5n第14页，此课件共105页哦这个规约中有三个部分：基调n：N；：谓词n5；：项n。基调刻划在形成集合时考虑的值的范围，谓词定义集合如何被构造，项则给出集合中项的一般形式。第15页，此课件共105页哦2.集合运算符用命题法定义两个集合的运算。定义定义10-2设A，B为任意两个集合。令AB=xxA或xBAB=xxA和xB
6、AB=xxA且xBAB=（AB）（AB）第16页，此课件共105页哦l集合的运算可以用文氏图如图直观地表示。图中的阴影部分表示运算的结果。第17页，此课件共105页哦第18页，此课件共105页哦l3笛卡尔乘积笛卡尔乘积l4.逻辑运算符逻辑运算符l4.序列序列第19页，此课件共105页哦l10.1.3应用数学符号描述形式规约例10-18：块处理器在操作系统中一个更重要的部分是维护由用户创建的文件的子系统，块处理器是文件子系统中的一部分。文件存储中的文件由存储设备上的存储块构成，在计算机的操作中，文件被创建和删除，需要存储块的获取和释放。为了处理这些，文件子系统维持一个未用块池，并将保持对当前使用
7、块的跟踪。当块从被删除文件释放时，它们通常被加入到等待进入未用块池的块队列中。如图所示.第20页，此课件共105页哦第21页，此课件共105页哦l对这个子系统而言，状态是自由块的集合、已用块的集合、以及返回块的队列，数据不变式用自然语言表达如下：第22页，此课件共105页哦1.没有块同时被标记为未用和已用。2.所有在队列中的块集合将是当前已用块集合的子集。3.没有队列元素包含相同的块号。第23页，此课件共105页哦4.已用块和未用块的集合将是组成文件的块的总集。5.在未用块集合中没有重复的块号。6.在已用块集合中没有重复的块号。第24页，此课件共105页哦l和子系统关联的某些操作如下：1.将一
8、个块集合加到队列尾。2.从队列前面移走一个已用块集合并将其放到未用块集合中。3.检查是否块队列为空。第25页，此课件共105页哦l描述块处理器的不变式有如下一组条件：1.没有块同时被标记为未用和已用。2.所有在队列中的块集合将是当前已用块集合的子集。3.在未用块集合中没有重复的块号。第26页，此课件共105页哦4.没有队列元素包含相同的块号。5.已用块和未用块的集合将是组成文件的块的总集。6.在已用块集合中没有重复的块号。第27页，此课件共105页哦l10.1.4形式化规约语言l形式化规约语言通常由三个主要的成分构成：(1)语法，定义用于表示规约的特定符号；(2)语义，帮助定义用于描述系统的“
9、对象的全域(universeofobjects)”；(3)一组关系，定义确定出哪个对象真正满足规约的规则。第28页，此课件共105页哦l形式化规约语言的语法域通常基于从标准集合论符号和谓词演算导出的语法。第29页，此课件共105页哦10.2有限状态机（有限状态机（FSM）l很多实时系统，特别是实时控制系统，其整个分析机制与系统的状态有相当大的关系。有限状态机由有限的状态和相互之间的转移构成，在任何时候只能处于给定数目的状态中的一个。第30页，此课件共105页哦l当接收到一个输入事件时，状态机产生一个输出，同时也可能伴随着状态的转移。主要有两种方法来建立有限状态机，一种是状态转移图，另一种是状态
10、转移表，分别用图形方式和表格方式建立有限状态机。第31页，此课件共105页哦l有限状态机的组成如下：（1）一个有限的状态集合Q（2）一个有限的输入集合I（3）一个变迁函数：QIQ变迁函数也是一个状态函数，在某一状态下，给定输入后，FSM转入该函数产生的新状态。的定义域内的某些数值可以是未定义的。第32页，此课件共105页哦l下图示意了一个简单的有限状态机。左图表明该FSM有q0、q1、q2、q3四个状态，输入集中有a、b、c三个元素；右图中各个状态之间的转换关系则更清晰。第33页，此课件共105页哦第34页，此课件共105页哦l有限状态机的优点在于简单易用，状态间的关系能够直观看到。第35页，
11、此课件共105页哦l有限状态机应用在实时系统中时，其最大的缺点是：任何时刻系统只能有一个状态，无法表示并发性，不能描述异步并发的系统。另外，在系统部件较多时，状态数随之增加，导致复杂性显著增长。第36页，此课件共105页哦10.3Petri网概念网概念lPetri网是在软件分析中，用一种系统的数学和图形的描述与分析的方法。对于具有并发、异步、分布、并行、不确定性或随机性的信息处理系统，都可以利用Petri网方法构造出要开发的Petri网模型。第37页，此课件共105页哦l由于Petri网的表示手法是用图形工具。因此其表示形式与传统方法的结构图、流程图具有同样的直观、形象效果。第38页，此课件共
12、105页哦lPetri网可以建立状态方程、代数方程以及系统行为的其他数学模型。因此，系统开发人员和理论研究工作者都可以根据需要利用Petri网。第39页，此课件共105页哦l10.3.1静态结构lPetri网理论认为，任何系统是由两类基本元素组成：一类是表示状态的元素，另一是表示状态变化的元素。第40页，此课件共105页哦l在Petri网中，表示状态的元素用位置（place）表示，表示状态变化的元素用转移（transition）表示。转移的作用是改变状态，位置的作用是决定转移能否发生。将状态的元素和状态变化的元素两者间的这种依赖关系用弧（箭头）表示出来就是一个Petri网。第41页，此课件共1
13、05页哦lPetri网的基本成份可以表示为一个三元组：N=（P，T；F）并满足以下条件：（1）PT（2）PT=（3）F（PT）（TP）（4）DOM（F）COD（F）=PT第42页，此课件共105页哦l例：N的Petri网N=（P，T；F）P=p1，p2，p3，p4，p5，p6T=t1，t2，t3，t4，t5，t6F=（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
14、页哦第44页，此课件共105页哦l10.3.2动态特征l在用Petri网作为系统分析和建模工具时，除了具有描述的静态结构的能力外，还包括位置容量以及转移启动对位置容量的影响信息。第45页，此课件共105页哦l如果对于位置容量的有限容量用大于零的整数表示。转移启动对位置中标记数的影响用弧上的整数表示。那么，于是具有动态特征的Petri网就可以表示为六元组：=（P，T；F，K，W，M0）第46页，此课件共105页哦l例：具有M0和W的Petri网可以表示为下图所示。第47页，此课件共105页哦第48页，此课件共105页哦l对于上图所示的Petri网，M0=（1，0，0，0，0，0）W（t2，p1）
15、=W（t5，p6）=W（t6，p1）=4W（t3，p3）=6W（t4，p5）=5第49页，此课件共105页哦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页哦l10.3.3转移启动规则l前面介绍的Petri网的动态特征是Petri网的动态行为的特性描述。这种动态行为是通过转移启动引起标识改变的变化来体现的。而转移启动则要有可以启动转移（转移有效）的条件和启动规则。第51页，此课件共105页哦（1）转移t有效的条件（2）转移t启动的结果第52页，此课件共10
16、5页哦l我们以下图为例说明转移启动规则。第53页，此课件共105页哦第54页，此课件共105页哦l为了说明“并发”和“冲突”这两个概念，我们用图10-9所示的Petri网来表示“混惑”。第55页，此课件共105页哦第56页，此课件共105页哦l有了这些基本概念后，就可以对于“并发”和“冲突”两个概念的完整描述。第57页，此课件共105页哦l1.并发l设M为Petri网的一个标识，若存在t1和t2使得Mt1和Mt2，并满足Mt1M1M1t2，且Mt2M2Mt1，则称t1和t2在M下并发。第58页，此课件共105页哦l2.冲突l设M为Petri网的一个标识，若存在t1和t2使得Mt1和Mt2，并满
17、足Mt1M1M1t2，且Mt2M2M2t1，则称t1和t2在M下冲突，说是说在M标识下，t1和t2都有效，但t1和t2中只有一个能启动，而且其中任一个转移启动都会使另一个转移无效。第59页，此课件共105页哦l10.3.4行为特性l行为特性包括：1、可达性2、有界性3、活性4、可逆性第60页，此课件共105页哦5、可覆盖性6、持久性7、同步距离8、公平性第61页，此课件共105页哦l10.3.5行为特性分析方法l行为特性分析方法分为三类：l（1）可覆盖性（可达性）树。l（2）矩阵方程求解。l（3）分层或化简。第62页，此课件共105页哦l用不变性、关联矩阵和状态方程的分析方法，就是完全用代数计
18、算对网系统进行分析的方法。第63页，此课件共105页哦l不变量l所谓不变量是指网系统中有S-不变量和T-不变量。下面几个图显示的是不变量的Petri网。第64页，此课件共105页哦第65页，此课件共105页哦第66页，此课件共105页哦第67页，此课件共105页哦l2.状态方程如果N=（P，T；F）是纯网，则C与N存在一一对应的关系。第68页，此课件共105页哦l3.关联矩阵正如网系统的标识可以表示为一个向量一样，网结构也可以用一个矩阵来表示。第69页，此课件共105页哦l10.3.6结构特性分析方法lPetri网有它的的拓扑结构。结构特性依赖于Petri网的拓扑结构。这些特性适合于网的任何初
19、始标识，也就是说这些特性是独立于网的初始标识M0的。因此，这些特性通常可以用关联矩阵C及其相关的齐次方程或不等式来刻划。第70页，此课件共105页哦l对于Petri网N，我们引入如下几种结构特性：l1.结构活性若N存在一个活的初始标识，则称N为结构活的。l2.完全可控性若N的任何标识都可从N的任一其他标识到达，则称N为完全可控的。l3.结构有界性若N对任何有限的初始标识M0都是有界的，则称N为结构有界性。第71页，此课件共105页哦l定理一定理一：Petri网N是结构有界的，当且仅当存在一个m维正整数向量Y，使得CY0。第72页，此课件共105页哦l推论：推论：N中位置pi是结构无界的，当且仅
20、当存在一个非负整数n维向量X，使得CTX=M0，其中的M第i项大于0（即M（pi）0）。第73页，此课件共105页哦l4.守恒性若N的每一（某些）位置p存在一个正整数Y（p），使得对任何给定的初始标识M0和每个MR（M0），都有标识的加权和MTY=M0TY为一个常量，则称N为（部分）守恒的。第74页，此课件共105页哦l定理二：定理二：Petri网是（部分）守恒的，当且仅当存在一个正的（非负）整数m维向量Y，满足CY=0，Y0。第75页，此课件共105页哦l5.重复性若N存在一个标识M0和一个从M0开始的启动序列，使得每个（某些）转移在中可以无限次发生，则称N为（部分）重复的。第76页，此课件
21、共105页哦l定理三：定理三：Petri网N是（部分）重复的，当且仅当存在一个正的（非负）整数n维向量x，使得CTX0，X0。第77页，此课件共105页哦l6.一致性若N存在一个标识M0和一个从M0返回到M0的启动序列，使得每个（某些）转移在中至少出现一次，则称N为（部分）一致的。第78页，此课件共105页哦l定理四：定理四：Petri网N是（部分）一致的，当且仅当存在一个正的（非负）整数n维向量X，便得CTX=0，X0第79页，此课件共105页哦l10.3.7Petri网到程序结构的转换网到程序结构的转换l1.流程图的方法传统方法的流程图方法主要用于顺序软件开发的详细设计阶段的建模与分析。如
22、果把并行处理退化为只有一个单进程的软件系统，用Petri网表示，那么传统方法的流程图方法也可以用于并行软件的开发。第80页，此课件共105页哦l2.编程语言的方法除了流程图与Petri网互相转换的方法外，也可以用编程语言转换。但是编程语言（如Ada、C+等）必须选用具有并发机制。用具有并发机制编程语言与Petri网两者之间建立起恰当的联系，这样就可以实现从Petri网到编程语言的转换。第81页，此课件共105页哦l3.面向对象的程序设计方法面向对象最适合用于Petri网的描述与分析，因为对象把数据和施加于这些数据上的私有操作封装在一起。操作名列在封装对象的界面上，当其他对象要“启动”该对象某个
23、操作时，则以操作名发一条消息，该对象接受了消息，操作即动作起来，完成对私有数据的加工。第82页，此课件共105页哦10.4净室方法学净室方法学l净室软件工程(Cleanroomsoftwareengineering)是一种在软件开发过程中强调在软件中建立正确性的需要的方法。代替传统的分析、设计、编码、测试和调试周期，净室方法建议一种不同的观点：通过在第一次正确地书写代码增量并在测试前验证它们的正确性来避免对成本很高的错误消除过程的依赖。它的过程模型是在代码增量积聚到系统的过程的同时进行代码增量的统计质量验证。第83页，此课件共105页哦l10.4.1净室方法l对软件工程的净室哲学首先由Mill
24、和其同事于1980年代提出，虽然对这个严格的软件开发方法的早期经验显示了很大的希望，但它并没有得到广泛的使用，主要是由于下面的原因：第84页，此课件共105页哦1.净室方法学太理论、太数学，以至难于在真实的软件开发中使用。2.不需要进行单元测试，而是进行正确性验证和统计质量控制，与当前大多数软件开发方式背离。3.软件开发产业的成熟度。第85页，此课件共105页哦l10.4.2净室过程模型l净室方法使用增量软件模型的一个专门版本。一个“软件增量的流水线”被若干小的、独立的软件工程小组开发，一旦每个增量被认证通过，它将被集成为一个整体。因此，系统的功能随时间增加。对每个增量的净室任务序列如图所示。
25、第86页，此课件共105页哦第87页，此课件共105页哦l10.4.3功能规约l净室软件工程通过使用称为盒结构规约的方法来遵从操作分析原则。从在顶层的本质表示转移向在底层的实现特定的细节。有三种盒类型：第88页，此课件共105页哦l黑盒。这种盒刻划系统或系统的某部分的行为。通过运用由激发得到反应的一组变迁规则，系统(或部分)对特定的激发(事件)作出反应。第89页，此课件共105页哦l状态盒。这种盒以类似于对象的方式封装状态数据和服务(操作)。在这个规约视图中，表示出状态盒的输入(激发)和输出(反应)。状态盒也表示黑盒的“激发历史”，即，封装在状态盒中的、必须在蕴含的变迁间保留的数据。第90页，
26、此课件共105页哦l清晰盒。在清晰盒中定义状态盒所蕴含的变迁功能，简单地说，清晰盒包含了对状态盒的过程设计。第91页，此课件共105页哦l下图给出了使用盒结构规约的求精方法。第92页，此课件共105页哦第93页，此课件共105页哦l10.4.4黑盒规约l黑盒规约是一个抽象，用图所示的符号描述了系统如何对激发作出反应。第94页，此课件共105页哦第95页，此课件共105页哦l10.4.5状态盒规约l状态盒是“状态机制的一个简单通用化”。一个状态是系统行为的某些可观测的模式。当进行处理时，一个系统对事件(激发)作出反应从当前状态转变到某新状态。当转变进行时，可能发生某个动作。如图所示，状态盒同黑盒
27、协作。第96页，此课件共105页哦第97页，此课件共105页哦10.5客户客户/服务器模式服务器模式l分布式计算机体系结构的进展，使得我们能够为在组织中如何组织工作及如何处理信息开发新的途径。新的组织结构和新的信息处理方法有决策支持系统、组件和成像等技术，这种技术的思想与基于主机型和基于微机的技术根本不同。第98页，此课件共105页哦l10.5.1系统的结构l下图给出了一个分布的和协作的计算机体系结构。第99页，此课件共105页哦第100页，此课件共105页哦l在C/S结构中，位于另一个计算机上层的计算机称为服务器，而在下层的计算机称为客户机。客户请求服务，而服务器提供服务。然而，在下图所示的体系结构范围内，可以完成一系列不同的实现。第101页，此课件共105页哦第102页，此课件共105页哦l10.5.2中间件和对象请求代理体系结构l一种广泛使用的对象请求代理标准称为CORBA，由对象管理组织OMG开发。CORBA的基本体系结构如图所示。第103页，此课件共105页哦第104页，此课件共105页哦l10.5.3分析建模问题l对C/S系统的需求活动和针对更传统的计算机体系结构的分析建模方法几乎没有不同，因此，在前面讨论的基本分析原则以及讨论的分析建模方法同样适用于C/S系统。第105页，此课件共105页哦