《软件工程SoftwareEngineeringppt课件》由会员分享，可在线阅读，更多相关《软件工程SoftwareEngineeringppt课件（70页珍藏版）》请在金锄头文库上搜索。
1、 软件工程软件工程 Software Engineering国防科技大学计算机学院国防科技大学计算机学院 2004.07齐治昌齐治昌齐治昌齐治昌 教授，教授，教授，教授， 谭庆平谭庆平谭庆平谭庆平 教授，教授，教授，教授， 宁洪宁洪宁洪宁洪 教授，教授，教授，教授， 董威董威董威董威 博士博士博士博士2024/8/261国防科技大学计算机学院第七章第七章 面向数据的分析方法与面向数据的分析方法与形式化方法形式化方法前面介绍的面向数据流和面向对象的分析是目前前面介绍的面向数据流和面向对象的分析是目前被广泛采用并具有较好发展潜力的需求分析被广泛采用并具有较好发展潜力的需求分析 方法。方法。然而，在
2、软件开发实践中仍有其它一些方法可供分析然而，在软件开发实践中仍有其它一些方法可供分析人员选择，它们在各自适用的领域也表现出了一定的人员选择，它们在各自适用的领域也表现出了一定的优越性和生命力。这些方法包括面向数据结构的系统优越性和生命力。这些方法包括面向数据结构的系统开发方法开发方法( (DSSD)， Jackson系统开发方法系统开发方法( (JSD)以及以及形式化软件规格说明技术。前两种统称为面向数据的形式化软件规格说明技术。前两种统称为面向数据的需求分析方法。需求分析方法。2024/8/262国防科技大学计算机学院面向数据的分析方法与形式化方法面向数据的分析方法与形式化方法特点特点o以信
3、息对象及其操作为核心进行需求分析，与面向以信息对象及其操作为核心进行需求分析，与面向对象分析相似。对象分析相似。o复合信息对象具有层次结构，并且可按顺序、选择、复合信息对象具有层次结构，并且可按顺序、选择、重复三种结构分解为成员信息对象。重复三种结构分解为成员信息对象。o提供将层次信息结构映射为程序结构的机制，从而提供将层次信息结构映射为程序结构的机制，从而为软件设计奠定较好的基础。为软件设计奠定较好的基础。第七章第七章 面向数据的分析方法与形式化方法面向数据的分析方法与形式化方法2024/8/263国防科技大学计算机学院7.1 7.1 面向数据结构的系统开发方法面向数据结构的系统开发方法oD
4、SSDDSSD起源于七十年代起源于七十年代WarnierWarnier在信息领域分析方面的杰出工作。在信息领域分析方面的杰出工作。o利用顺序、选择、利用顺序、选择、 重复重复 三种结构表示信息的层次分解，并三种结构表示信息的层次分解，并指出可以从信息层次结构推导出程序结构。指出可以从信息层次结构推导出程序结构。oKen Orr Ken Orr 对对WarnierWarnier的工作进行了扩充，引进了数据流和处理的工作进行了扩充，引进了数据流和处理功能，从而发展成为一种需求分析方法。功能，从而发展成为一种需求分析方法。o本节介绍本节介绍 Warnier Warnier图图 DSSD DSSD方法
5、方法 创建实体图、信息过程图、创建实体图、信息过程图、WarnierWarnier-Orr-Orr原型图。原型图。第七章第七章 面向数据的分析方法与形式化方法面向数据的分析方法与形式化方法2024/8/264国防科技大学计算机学院面向数据结构的系统开发方法面向数据结构的系统开发方法(1)(1)首版首版标题新闻标题新闻 国内新闻国内新闻 本地新闻本地新闻(2)(2)商业金融版商业金融版股市行情股市行情 商业新闻商业新闻 广告广告(3)(3)文化体育版文化体育版文化、体育新闻文化、体育新闻 散文散文 新书评论新书评论7.1面向数据结构的系统开发方法面向数据结构的系统开发方法2024/8/265国防
6、科技大学计算机学院7.1.1 7.1.1 WarnierWarnier图图oWarnierWarnier图是一种表示信息层次结图是一种表示信息层次结构的紧致机制。构的紧致机制。oWarnierWarnier图具有树形层次结构，可图具有树形层次结构，可以用另外一些以用另外一些WarnierWarnier图继续分解图继续分解图中的叶结点。图中的叶结点。例例报纸自动组版系统报纸自动组版系统图，花括符内的信息条目构成顺序图，花括符内的信息条目构成顺序关系，园括符内的数字表示重复次关系，园括符内的数字表示重复次数，如，广告数，如，广告 可以有可以有1 1至至5 5条，股条，股市行情出现市行情出现0 0到
7、到1 1次。次。符号符号“”表示不可兼具的选择关表示不可兼具的选择关系。系。7.1面向数据结构的系统开发方法面向数据结构的系统开发方法2024/8/266国防科技大学计算机学院7.1.2 DSSD7.1.2 DSSD方法方法基于基于DSSDDSSD需求分析方法的步骤需求分析方法的步骤(1)(1)标识与应用问题有关的实体。标识与应用问题有关的实体。(2)(2)创建一种类似于数据流图的信息创建一种类似于数据流图的信息过程图。过程图。(3)(3)创建创建WarnierWarnier-Err-Err原型图。原型图。在详细介绍在详细介绍DSSDDSSD的具体步骤之前，首先用数据流图描的具体步骤之前，首先
8、用数据流图描述一个基于计算机的软件专卖店管理系统，见图述一个基于计算机的软件专卖店管理系统，见图7.2. 7.2. 注意，数据流图并非注意，数据流图并非DSSDDSSD的组成部分。图的组成部分。图7.27.2仅用于说仅用于说明后面将要用到的应用问题实例。明后面将要用到的应用问题实例。7.1面向数据结构的系统开发方法面向数据结构的系统开发方法2024/8/267国防科技大学计算机学院软件专卖店管理系统的数据流图表示软件专卖店管理系统的数据流图表示7.1面向数据结构的系统开发方法面向数据结构的系统开发方法2024/8/268国防科技大学计算机学院1. 1. 标识实体图标识实体图在在DSSDDSSD
9、中，与应用问题有关的实体及它们之间的信息中，与应用问题有关的实体及它们之间的信息流用实体图表示。它与面向对象分析中流用实体图表示。它与面向对象分析中 的对象消息的对象消息传递图有相似之处，因此，识别实体和信息流的方法传递图有相似之处，因此，识别实体和信息流的方法也类似于面向对象分析也类似于面向对象分析 。7.1面向数据结构的系统开发方法面向数据结构的系统开发方法2024/8/269国防科技大学计算机学院标识实体图标识实体图在在DSSDDSSD中，分析人员可通过对下述问题的回答来生成中，分析人员可通过对下述问题的回答来生成实体图实体图(1)(1)软件系统必须处理哪些信息项软件系统必须处理哪些信息
10、项? ?(2)(2)信息项的生产者和消费者分别是哪些实体信息项的生产者和消费者分别是哪些实体? ?o上述问题的有关实体是：客户、订单处理员、邮寄上述问题的有关实体是：客户、订单处理员、邮寄员、银行、结算员、管理员和邮局，见图员、银行、结算员、管理员和邮局，见图7. 3(7. 3(a)a)。订单处理员的实体图如图订单处理员的实体图如图7. 3(7. 3(b)b)所示。所示。o当所有实体的实体图都构造完成后，将它们综合起当所有实体的实体图都构造完成后，将它们综合起来便形成整个目标软件系统的实体图，见图来便形成整个目标软件系统的实体图，见图7. 47. 4。 7.1面向数据结构的系统开发方法面向数据
11、结构的系统开发方法2024/8/2610国防科技大学计算机学院标识实体图标识实体图7.1面向数据结构的系统开发方法面向数据结构的系统开发方法2024/8/2611国防科技大学计算机学院标识实体图标识实体图7.1面向数据结构的系统开发方法面向数据结构的系统开发方法2024/8/2612国防科技大学计算机学院2. 2. 创建信息创建信息过程图过程图oDSSDDSSD中的信息中的信息过程图与数过程图与数据流图的作用类似，都是用据流图的作用类似，都是用来表示信息流及其处理功能来表示信息流及其处理功能的。的。o信信 息息过程图从每个实体过程图从每个实体的输出信息流开始，逆向寻的输出信息流开始，逆向寻找用
12、于生成该输出信息的输找用于生成该输出信息的输入信息流及相入信息流及相 应的处理功能。应的处理功能。7.1面向数据结构的系统开发方法面向数据结构的系统开发方法2024/8/2613国防科技大学计算机学院3. 3. 创建创建WarnierWarnier-Orr-Orr原型图原型图DSSDDSSD方法方法o分析人员以表格形式给出主要的输出信息元素分析人员以表格形式给出主要的输出信息元素o精确地表示为精确地表示为WarnierWarnier-Orr-Orr图图7.1面向数据结构的系统开发方法面向数据结构的系统开发方法2024/8/2614国防科技大学计算机学院创建创建WarnierWarnier-Or
13、r-Orr原型图原型图7.1面向数据结构的系统开发方法面向数据结构的系统开发方法2024/8/2615国防科技大学计算机学院7.2 Jackson7.2 Jackson系统开发方法系统开发方法o七十年代七十年代JacksonJackson提出了软件工程领域中著名的提出了软件工程领域中著名的JacksonJackson方法，当时它只用于软件设计。方法，当时它只用于软件设计。o八十年代初，八十年代初，JacksonJackson又对它进行了多方面的扩充和又对它进行了多方面的扩充和完善，最终发展成为一种需求分析方法。完善，最终发展成为一种需求分析方法。oJacksonJackson方法的核心思想是：
14、方法的核心思想是： 根据作用于数据的行为序列的结构根据作用于数据的行为序列的结构( (顺序、选择与顺序、选择与重复重复) )，建立目标软件系统的模型，然后在软件设计，建立目标软件系统的模型，然后在软件设计阶段将模型演化为相应的程序结构。阶段将模型演化为相应的程序结构。第七章第七章 面向数据的分析方法与形式化方法面向数据的分析方法与形式化方法2024/8/2616国防科技大学计算机学院JacksonJackson系统开发方法系统开发方法JacksonJackson方法在需求分析阶段的主要步骤方法在需求分析阶段的主要步骤(1)(1)标识实体与行为。标识实体与行为。(2)(2)生成实体结构图。生成实
15、体结构图。(3)(3)创建软件系统模型。创建软件系统模型。7.2Jackson系统开发方法系统开发方法2024/8/2617国防科技大学计算机学院7.2.1 7.2.1 标识实体与行为标识实体与行为oJacksonJackson方法针对初步需求分析形成的用户需求描述方法针对初步需求分析形成的用户需求描述进行语法分析。进行语法分析。o名词及名词短语是潜在的实体，相关的动词构成实名词及名词短语是潜在的实体，相关的动词构成实体的潜在行为。体的潜在行为。o分析人员根据应用问题的边界及自己的理解，决定分析人员根据应用问题的边界及自己的理解，决定对潜在实体和行为的取舍。对潜在实体和行为的取舍。7.2Jac
16、kson系统开发方法系统开发方法2024/8/2618国防科技大学计算机学院标识实体与行为标识实体与行为例例7. 17. 1o 某大学决定将分处两地的校园用直达交通车连接起某大学决定将分处两地的校园用直达交通车连接起来。在每个校园设一个站，站内配置一个按钮。学生来。在每个校园设一个站，站内配置一个按钮。学生通过按钮请求交通车搭载。交通车应尽快满足学生的通过按钮请求交通车搭载。交通车应尽快满足学生的请求。空闲时，交通车停在请求。空闲时，交通车停在 任意站等候。任意站等候。o 分析人员可从分析人员可从“大学大学”、“校园校园”、“交通车交通车”、“车站车站”、“学生学生”、“按钮按钮”等名词中选取
17、与应用等名词中选取与应用问题相关实体、行为、状态。问题相关实体、行为、状态。相关的实体：相关的实体：“交通车交通车”、“车站车站”、“按钮按钮”。相关的行为：相关的行为：“到站到站”、“离站离站”、“按键按键”。“交通车交通车”的状态：的状态：“等候等候”和和“运行运行”。7.2Jackson系统开发方法系统开发方法2024/8/2619国防科技大学计算机学院7.2.2 7.2.2 生成实体结构图生成实体结构图 在在JacksonJackson方法中，实体结构是指实体在时间坐方法中，实体结构是指实体在时间坐标系中的行为序列。这种序列以顺序、选择标系中的行为序列。这种序列以顺序、选择 和重复和重
18、复三种结构进行复合。三种结构进行复合。 Jackson Jackson给出的实体结构图示机制如图给出的实体结构图示机制如图7. 77. 7所示。所示。其中的子结点其中的子结点 既可以是行为，也可以是子实体。在既可以是行为，也可以是子实体。在后一情况下，子实体应该继续分解，不能作为实体结后一情况下，子实体应该继续分解，不能作为实体结构图的叶结点。构图的叶结点。7.2Jackson系统开发方法系统开发方法2024/8/2620国防科技大学计算机学院实体结构图的图形记号实体结构图的图形记号7.2Jackson系统开发方法系统开发方法2024/8/2621国防科技大学计算机学院实体结构图的图形记号实体
19、结构图的图形记号7.2Jackson系统开发方法系统开发方法2024/8/2622国防科技大学计算机学院7.2.3 7.2.3 创建软件系统模型创建软件系统模型 为了创建目标软件系统的模型，为了创建目标软件系统的模型，JacksonJackson方法要方法要求分析人员首先用图求分析人员首先用图7.97.9所示的图形记号建立系统规所示的图形记号建立系统规格说明图格说明图( (System Specification Diagram, SSD)System Specification Diagram, SSD)。o“数据流数据流”(”(Data Stream)Data Stream)记号表示现实世
20、界中的过记号表示现实世界中的过程或装置不断地向目标软件系统中的相应过程发送数程或装置不断地向目标软件系统中的相应过程发送数据，后者以先进据，后者以先进 先出方式消费数据。先出方式消费数据。o两者之间的缓冲区容量是无限的。两者之间的缓冲区容量是无限的。o“状态向量状态向量”(”(State Vector)State Vector)记号表示在两者之间记号表示在两者之间存在状态向量，发送方设置状态向量，接收方读取状存在状态向量，发送方设置状态向量，接收方读取状态向量。态向量。7.2Jackson系统开发方法系统开发方法2024/8/2623国防科技大学计算机学院创建软件系统模型创建软件系统模型o站内
21、按钮和目标软件中的按站内按钮和目标软件中的按钮处理过程之间以钮处理过程之间以“数据流数据流” ” 方式连接方式连接o交通车和交通车控制过程之交通车和交通车控制过程之间则应以间则应以“状态向量状态向量”方式方式连接。连接。7.2Jackson系统开发方法系统开发方法2024/8/2624国防科技大学计算机学院系统规格说明图示例系统规格说明图示例 利用利用JacksonJackson给出的给出的“结构结构正文正文” (” (Structure Text)Structure Text)将将实体结构图和系实体结构图和系 统规格说明统规格说明图综合起来，并针对目标软图综合起来，并针对目标软件系统中的每一
22、过程用正文件系统中的每一过程用正文方式给出更为精确、更为详方式给出更为精确、更为详尽的描述。尽的描述。7.2Jackson系统开发方法系统开发方法2024/8/2625国防科技大学计算机学院正文描述正文描述BUTTONBUTTON1 1 read read ButtonDownButtonDown信号信号 PUSHPUSHBODY BODY itritr while while ButtonDown ButtonDown 循环结构循环结构 PUSH PUSH 按键处理按键处理 read read ButtonDownButtonDown信号信号 PUSHPUSHBODY endBODY end
23、BOTTONBOTTON1 end1 end7.2Jackson系统开发方法系统开发方法2024/8/2626国防科技大学计算机学院正文描述正文描述SHUTTLESHUTTLE1 1 seq seq 顺序结构顺序结构 read read 状态向量状态向量 WAITWAITBODY1 BODY1 itritr while Wait(1) while Wait(1) 如果状态向量中等待如果状态向量中等待 标志置位，则循环等待标志置位，则循环等待 read read 状态向量状态向量 WAITWAITBODY1 endBODY1 end Leave(1) Leave(1) 控制交通车离开站控制交通车
24、离开站1 1 TRANSITTRANSITBODY1 BODY1 itritr while Transit(1) while Transit(1) 如果状态向量中运行标志如果状态向量中运行标志 置位，则一直运行置位，则一直运行 read read 状态向量状态向量 TRANSITTRANSITBODY1 endBODY1 end 7.2Jackson系统开发方法系统开发方法2024/8/2627国防科技大学计算机学院正文描述正文描述SHUTTLESHUTTLEBODY1 BODY1 itr itr 往返重复运行往返重复运行 STATION STATION seqseq Arrive(i) Ar
25、rive(i) 控制交通车减速，准备停靠站控制交通车减速，准备停靠站I I WAIT WAITBODY BODY itritr while Wait(i) while Wait(i) 如果状态向量中在站如果状态向量中在站i i的的 等待标志置位，则循环等待等待标志置位，则循环等待 read read 状态向量状态向量 WAITWAITBODY end BODY end Leave(i) Leave(i) TRANSIT TRANSITBODY BODY itritr while Transit(i) while Transit(i) read read 状态向量状态向量 TRANSITTRAN
26、SITBODY endBODY end STATION end STATION end SHUTTLE SHUTTLEBODY1 endBODY1 end Arrive(1) Arrive(1)SHUTTLESHUTTLE1 end1 end7.2Jackson系统开发方法系统开发方法2024/8/2628国防科技大学计算机学院正文描述正文描述 Wait(i) Transit(i) (i=1,2) Wait(i) Transit(i) (i=1,2) 现实世界的交通车现实世界的交通车 SHUTTLESHUTTLE0 0 向软件过程向软件过程 SHUTTLESHUTTLE1 1 发出的状态向量的
27、一部分。发出的状态向量的一部分。7.2Jackson系统开发方法系统开发方法2024/8/2629国防科技大学计算机学院结构正文的结构图结构正文的结构图7.2Jackson系统开发方法系统开发方法2024/8/2630国防科技大学计算机学院7.3 7.3 形式化方法形式化方法o前面对数据流图、面向对象的需求表示图等语言机前面对数据流图、面向对象的需求表示图等语言机制都未给出数学意义上严格的语法和语义说明。因此，制都未给出数学意义上严格的语法和语义说明。因此，这些需求模型都或多或少地带有不精确性、不完全性，这些需求模型都或多或少地带有不精确性、不完全性，甚至不一致性。甚至不一致性。o许多软件开发
28、实践希望借助于形式化方法严格地定许多软件开发实践希望借助于形式化方法严格地定义用户需求，并通过数学推演确保需求定义的一致性义用户需求，并通过数学推演确保需求定义的一致性和完全性。和完全性。o对于正确性至关重要的实时嵌入式系统关键部件的对于正确性至关重要的实时嵌入式系统关键部件的软件开发，形式化方法更是不可或缺的。软件开发，形式化方法更是不可或缺的。第七章第七章 面向数据的分析方法与形式化方法面向数据的分析方法与形式化方法2024/8/2631国防科技大学计算机学院形式化方法形式化方法o主要思想主要思想oZ Z语言语言 形式化规格说明语言形式化规格说明语言o简单实时操作系统内核的形式化需求描述方
29、法。简单实时操作系统内核的形式化需求描述方法。o形式化方法的现状和发展趋势。形式化方法的现状和发展趋势。7.3形式化方法形式化方法2024/8/2632国防科技大学计算机学院7.3.1 7.3.1 主要思想主要思想o形式化需求分析方法的主要思想是利用形式化规格形式化需求分析方法的主要思想是利用形式化规格说明语言定义用户需求，并采用数学推演的方法证明说明语言定义用户需求，并采用数学推演的方法证明需求定义的性质，例如一致性、实时系统的活性需求定义的性质，例如一致性、实时系统的活性( (LivenessLiveness) )和公平性和公平性( (Fairness)Fairness)等。对于复杂的应用
30、等。对于复杂的应用问题，尽管无法验证整个需求定义的完全性，但仍有问题，尽管无法验证整个需求定义的完全性，但仍有可能为避免某些要点的疏漏而建立数学断言，然后予可能为避免某些要点的疏漏而建立数学断言，然后予以形式证明或反驳。以形式证明或反驳。o形式化方法是克服需求分析阶段不精确性、不一致形式化方法是克服需求分析阶段不精确性、不一致性和不完全性的有效途径。性和不完全性的有效途径。7.3形式化方法形式化方法2024/8/2633国防科技大学计算机学院主要思想主要思想形式化规格说明语言的组成形式化规格说明语言的组成 语法语法 语义语义 数学推演规则数学推演规则 规则不仅说明了某些数学性质在软件规格说明中
31、规则不仅说明了某些数学性质在软件规格说明中是否成立，也说明了软件实现与软件规格说明之间的是否成立，也说明了软件实现与软件规格说明之间的关系。关系。7.3形式化方法形式化方法2024/8/2634国防科技大学计算机学院规格说明语言的语法规格说明语言的语法规格说明语言的语法规格说明语言的语法 集合论集合论 数理逻辑数理逻辑 代数学代数学Z Z语言语言 集合论集合论 属于属于 不属于不属于 子集关系子集关系 集合交集合交 集合并集合并 函数符号函数符号逻辑符号逻辑符号 任意任意 存在存在 非非 合取合取 析取析取 大多数宽谱语言包括，高级程序设计语言的控制流大多数宽谱语言包括，高级程序设计语言的控制
32、流机制，如顺序、条件、机制，如顺序、条件、 循环等等。循环等等。7.3形式化方法形式化方法2024/8/2635国防科技大学计算机学院规格说明语言的语义规格说明语言的语义规格说明语言的语义规格说明语言的语义 所有语法符号含意的数学描述。所有语法符号含意的数学描述。经典语义定义方法：经典语义定义方法： 指称语义指称语义 代数语义代数语义 操作语义操作语义7.3形式化方法形式化方法2024/8/2636国防科技大学计算机学院规格说明语言的语义规格说明语言的语义o指称语义指称语义 数学地确定规格说明语言的语义域，将所有语法成数学地确定规格说明语言的语义域，将所有语法成 分映射为语义域中的对象或语义域
33、上的函数。分映射为语义域中的对象或语义域上的函数。o代数语义代数语义 将软件规格说明中的某些结构化设施将软件规格说明中的某些结构化设施( (例如抽象数例如抽象数 据类型据类型) )解释为多类代数，通过代数工具解释为多类代数，通过代数工具( (例如范畴例如范畴 论论) ) 研究规格说明的代数性质、模块组装运算以及研究规格说明的代数性质、模块组装运算以及 软件设计相对于规格说明的实现关系。软件设计相对于规格说明的实现关系。o操作语义操作语义 形式地定义抽象机，将规格说明的语义解释为抽象形式地定义抽象机，将规格说明的语义解释为抽象 机的动作序列。机的动作序列。7.3形式化方法形式化方法2024/8/
34、2637国防科技大学计算机学院形式化规格说明语言的推演规则形式化规格说明语言的推演规则形式化规格说明语言的推演规则形式化规格说明语言的推演规则o与数学基础和语义定义方法密切相关。与数学基础和语义定义方法密切相关。o以集合论和谓词逻辑为基础的以集合论和谓词逻辑为基础的Z Z语言就包含了原数学语言就包含了原数学系统中有关的规则。系统中有关的规则。o规则必须在规格说明语言的语义系统中可证。规则必须在规格说明语言的语义系统中可证。o规则是派生的语义定义，它们可以直接应用于软件规则是派生的语义定义，它们可以直接应用于软件规格说明的性质证明并简化推演过程。规格说明的性质证明并简化推演过程。7.3形式化方法
35、形式化方法2024/8/2638国防科技大学计算机学院规则：规则：ifthenelseifthenelse结构的表示形式结构的表示形式EvalEval(e(e，e)e)表示表达式表示表达式e e可可计值为计值为ee。第一条规则的直观意义第一条规则的直观意义如果如果 e e0 0能计值为能计值为 TRUETRUE，e e1 1能计值能计值为为 e e1 1，则表达式则表达式 if eif e0 0 then ethen e1 1 else e else e2 2 可计值为可计值为e e1 1. . 7.3形式化方法形式化方法2024/8/2639国防科技大学计算机学院7.3.2 7.3.2 形式
36、化规格说明语言形式化规格说明语言用形式化规格说明语言描述用户需求用形式化规格说明语言描述用户需求oVDMVDM的的MetaMeta，CSPCSP和和Z Z是具有代表性的形式化规格是具有代表性的形式化规格说明语言说明语言 。oZ Z语言的语法设施及其语义说明语言的语法设施及其语义说明o实例及需求描述过程实例及需求描述过程7.3形式化方法形式化方法2024/8/2640国防科技大学计算机学院1. 1. 基本语法成分基本语法成分 Z Z的基本语法成份主要取自带类型的集合论和的基本语法成份主要取自带类型的集合论和一阶逻辑。一阶逻辑。7.3形式化方法形式化方法2024/8/2641国防科技大学计算机学院
37、基本语法成分基本语法成分7.3形式化方法形式化方法2024/8/2642国防科技大学计算机学院2. 2. 结构化设施结构化设施框架框架( (Schema)Schema)框架框架 变元说明变元说明 用一阶逻辑公式表示的变元取值约束条件用一阶逻辑公式表示的变元取值约束条件语法形式语法形式 框架名称框架名称 变元说明变元说明 约束条件约束条件 全局常元和函数的语法形式全局常元和函数的语法形式 常元及函数说明常元及函数说明 ( (说明常元及函数的类型说明常元及函数的类型) ) 约束条件约束条件 ( (说明常元及函数的取值约束说明常元及函数的取值约束) )7.3形式化方法形式化方法2024/8/2643
38、国防科技大学计算机学院结构化设施结构化设施框架框架( (Schema)Schema)o记号记号S S 如果框架如果框架S S中的所有变元为中的所有变元为v v1 1，v vm m，所有的约束条件为所有的约束条件为 P P，P Pn n，那么框架那么框架S S中的变元为中的变元为v v，v vm m， v v1 1,， v vm m， 约束条件为约束条件为P P1 1，,P Pn n，PP1 1，PPn n，其中其中v vi i与与vvi i的类型相同，的类型相同，PPj j是将是将P Pj j中所有中所有v vi i的出现替换为的出现替换为vvi i得到的得到的约束条件约束条件( (i=1,i
39、=1,，m, j=1, m, j=1, ，n n) )。o单引号单引号“”“” 用来区分操作发生前、后的变元取值。用来区分操作发生前、后的变元取值。o记号记号 s s = = s s 表示在操作发生前、后框架表示在操作发生前、后框架S S中的所有成员不发生变化中的所有成员不发生变化( (变元变元取值不变，约束条件也保持相同的真假值取值不变，约束条件也保持相同的真假值) )。7.3形式化方法形式化方法2024/8/2644国防科技大学计算机学院7.3.3 7.3.3 形式化需求描述形式化需求描述o例例 实时操作系统内核实时操作系统内核o用用Z Z语言描述软件需求语言描述软件需求 系统状态的表示系
40、统状态的表示 普通进程调度表示普通进程调度表示 中断处理进程调度表示中断处理进程调度表示7.3形式化方法形式化方法2024/8/2645国防科技大学计算机学院1. 1. 实例描述实例描述实时操作系统内核实时操作系统内核实时操作系统内核的主要任务实时操作系统内核的主要任务 提供进程调度和中断处理机制。提供进程调度和中断处理机制。o每个进程都有就绪标志，系统从已就绪进程中选择一个作为每个进程都有就绪标志，系统从已就绪进程中选择一个作为当前进程。当前进程。o当没有中断请求时，系统运行当前进程直至该进程显式释放当没有中断请求时，系统运行当前进程直至该进程显式释放处理器，然后系统再选取当前进程。处理器，
41、然后系统再选取当前进程。o当中断发生时，系统根据优先级高低选择最紧急的中断并运当中断发生时，系统根据优先级高低选择最紧急的中断并运行相应的中断处理进程。行相应的中断处理进程。o优先级高的中断可以打断优先级低的中断。优先级高的中断可以打断优先级低的中断。o普通进程可将自己登录为某一优先级的中断处理进程。普通进程可将自己登录为某一优先级的中断处理进程。7.3形式化方法形式化方法2024/8/2646国防科技大学计算机学院2. 2. 系统状态的表示系统状态的表示o 引进类型引进类型PIDPID表示所有进程标识符的集合。表示所有进程标识符的集合。o 虚构的进程标识符虚构的进程标识符nonenone用来
42、表示处理器的空闲状态。用来表示处理器的空闲状态。PIDPID表示不是表示不是nonenone的所有进程标识符：的所有进程标识符： none: PID none: PID PID PID1 1： P PID P PID PID PID1 1=PID=PIDnonenone PIDPID1 1是除是除nonenone外的所外的所 有进程标识符的集合有进程标识符的集合7.3形式化方法形式化方法2024/8/2647国防科技大学计算机学院系统状态的表示系统状态的表示进程调度机制框架进程调度机制框架Scheduler Scheduler * *框架名称为框架名称为Scheduler*Scheduler*
43、process: P PIDprocess: P PID1 1 * *变元变元process,readyprocess,ready和和 current current的说明的说明* *ready: P PIDready: P PID1 1current: PID current: PID readyreadyprocess process * *约束条件约束条件* *currentprocess currentprocess nonenone7.3形式化方法形式化方法2024/8/2648国防科技大学计算机学院系统状态的表示系统状态的表示o process表示由进程调度机制控制的所有进程的集表
44、示由进程调度机制控制的所有进程的集合。合。o ready是所有就绪进程的集合。是所有就绪进程的集合。o current是当前进程。是当前进程。o 框架框架SchedulerScheduler的约束条件的约束条件readyreadyprocessprocess表示就表示就绪进程必须是可调度的进程。绪进程必须是可调度的进程。o 约束条件约束条件currentprocess currentprocess nonenone表示当前表示当前进程要么是可调度进程，要么是进程要么是可调度进程，要么是none. none. 7.3形式化方法形式化方法2024/8/2649国防科技大学计算机学院系统状态的表示系
45、统状态的表示定义中断优先级的有穷集合定义中断优先级的有穷集合ILEVELILEVEL ILEVEL: FN ILEVEL: FN 0 0 ILEVEL ILEVEL ILEVELILEVEL是除是除0 0之外的自然数的有穷集之外的自然数的有穷集 不是中断处理进程的进程称为普通进程，普通进程的优先不是中断处理进程的进程称为普通进程，普通进程的优先级定义为级定义为0 0。7.3形式化方法形式化方法2024/8/2650国防科技大学计算机学院系统状态的表示系统状态的表示中断处理机制的描述中断处理机制的描述ohandlerhandler是内射函数，是内射函数， 所以两个优先级不能共用同一中断处理进程。
46、所以两个优先级不能共用同一中断处理进程。o中断可以是活跃的，并且不是未屏蔽的中断可以是活跃的，并且不是未屏蔽的, ,因为它可以在先前发生，而后因为它可以在先前发生，而后被更高优先级的中断打断并屏蔽。被更高优先级的中断打断并屏蔽。o集合集合activeactive不仅包含当前正被处理的中断优先级，也包括那些先前发生，不仅包含当前正被处理的中断优先级，也包括那些先前发生，而后又被打断的中断优。而后又被打断的中断优。7.3形式化方法形式化方法2024/8/2651国防科技大学计算机学院系统状态的表示系统状态的表示o实时操作系统的内核由进程实时操作系统的内核由进程调度和中断处理机制综合构调度和中断处理
47、机制综合构成成. .oKernelKernel包含了包含了SchedulerScheduler和和IntHandlerIntHandler的变元说明和约的变元说明和约束条件。束条件。o新加的约束条件说明普通进新加的约束条件说明普通进程不能兼为中断处理进程，程不能兼为中断处理进程，反之亦然。反之亦然。o系统状态应由正在运行的进系统状态应由正在运行的进程及其优先级构成。程及其优先级构成。7.3形式化方法形式化方法2024/8/2652国防科技大学计算机学院系统状态的表示系统状态的表示o系统的调度策略系统的调度策略7.3形式化方法形式化方法2024/8/2653国防科技大学计算机学院3. 3. 普通
48、进程调度普通进程调度普通进程调度操作普通进程调度操作o启动普通进程启动普通进程( (Start)Start)o设置或清除就绪标志设置或清除就绪标志( (SetReadySetReady) )o控制进程临时或永久性让出处理器控制进程临时或永久性让出处理器( (DetachDetach与与Stop)Stop)o当处理器空闲时选择新的进程运行当处理器空闲时选择新的进程运行( (Select)Select)7.3形式化方法形式化方法2024/8/2654国防科技大学计算机学院普通进程调度普通进程调度启动普通进程启动普通进程( (Start)Start)7.3形式化方法形式化方法2024/8/2655国
49、防科技大学计算机学院普通进程调度普通进程调度当处理器空闲时选择新的进程运行当处理器空闲时选择新的进程运行( (Select)Select)7.3形式化方法形式化方法2024/8/2656国防科技大学计算机学院普通进程调度普通进程调度o控制进程临时或永久性让出处理器控制进程临时或永久性让出处理器( (DetachDetach与与Stop)Stop)7.3形式化方法形式化方法2024/8/2657国防科技大学计算机学院普通进程调度普通进程调度StopStop操作将永久性终止当前进程的运行操作将永久性终止当前进程的运行StopStop7.3形式化方法形式化方法2024/8/2658国防科技大学计算机
50、学院普通进程调度普通进程调度设置或清除就绪标志设置或清除就绪标志( (SetReadySetReady) )7.3形式化方法形式化方法2024/8/2659国防科技大学计算机学院4. 4. 中断处理进程调度中断处理进程调度中断处理进程调度操作中断处理进程调度操作o将普通进程登录为中断处理进程将普通进程登录为中断处理进程IntEnterIntEntero中断屏蔽的设置与清除中断屏蔽的设置与清除MaskMasko中断响应中断响应InterruptInterrupto中断处理完成后相应的中断处理程序挂起中断处理完成后相应的中断处理程序挂起IntWaitIntWaito将自身降格为普通进程将自身降格为
51、普通进程IntExitIntExit7.3形式化方法形式化方法2024/8/2660国防科技大学计算机学院中断处理进程调度中断处理进程调度 IntEnterIntEnter操作定义操作定义7.3形式化方法形式化方法2024/8/2661国防科技大学计算机学院中断处理进程调度中断处理进程调度用于设置或清除中断屏蔽标志的操作用于设置或清除中断屏蔽标志的操作7.3形式化方法形式化方法2024/8/2662国防科技大学计算机学院中断处理进程调度中断处理进程调度InterruptInterrupt操作定义操作定义7.3形式化方法形式化方法2024/8/2663国防科技大学计算机学院中断处理进程调度中断处
52、理进程调度7.3形式化方法形式化方法2024/8/2664国防科技大学计算机学院中断处理进程调度中断处理进程调度 当中断处理完成后，中断处理进程可调用当中断处理完成后，中断处理进程可调用IntWaitIntWait操作将自操作将自己挂起。己挂起。IntWaitIntWait State State7.3形式化方法形式化方法2024/8/2665国防科技大学计算机学院中断处理进程调度中断处理进程调度中断处理进程还可调用中断处理进程还可调用IntExitIntExit将自己降格为普通进程将自己降格为普通进程7.3形式化方法形式化方法2024/8/2666国防科技大学计算机学院7.3.47.3.4形
53、式化方法的现状与发展趋势形式化方法的现状与发展趋势o形式化方法的优点性形式化方法的优点性 能够数学地表述和研究应用问题及其软件实现。能够数学地表述和研究应用问题及其软件实现。o要求分析人员具备良好的数学素质。要求分析人员具备良好的数学素质。o用形式化语言书写的大型应用问题的软件规格说明用形式化语言书写的大型应用问题的软件规格说明往往过于细化，难于为用户和软件设计人员所理解。往往过于细化，难于为用户和软件设计人员所理解。o形式化方法在目前的软件开发实践中并未得到普遍形式化方法在目前的软件开发实践中并未得到普遍应用。应用。7.3形式化方法形式化方法2024/8/2667国防科技大学计算机学院形式化
54、方法的现状与发展趋势形式化方法的现状与发展趋势近年来形式化方法在两方面改善了实用性近年来形式化方法在两方面改善了实用性(1)(1)形式化方法与图形语言机制相结合。形式化方法与图形语言机制相结合。 为图形语言机制赋予形式化的语法和语义，从而为图形语言机制赋予形式化的语法和语义，从而兼具了图形表示的直观、简洁，以及形式化方法的严兼具了图形表示的直观、简洁，以及形式化方法的严谨、精确等优点。谨、精确等优点。(2)(2)用用CASECASE工具支持形式化软件开发。工具支持形式化软件开发。 CASE CASE工具不仅可以简化需求分析和需求描述工作，工具不仅可以简化需求分析和需求描述工作， 而且还可以利用
55、自动定理证明技术帮助分析人员验证而且还可以利用自动定理证明技术帮助分析人员验证软件规格说明的数学性质。软件规格说明的数学性质。 7.3形式化方法形式化方法2024/8/2668国防科技大学计算机学院小结小结 本章介绍了面向数据结构的系统开发方法本章介绍了面向数据结构的系统开发方法( (DSSD)DSSD)和和JacksonJackson系统开发方法系统开发方法( (JSD)JSD)。 面向数据分析方法，首先描述问题域中的信息项及相关行面向数据分析方法，首先描述问题域中的信息项及相关行为，然后根据信息项具有的层次结构建造需求模型。为，然后根据信息项具有的层次结构建造需求模型。 面向数据分析方法的
56、适应面不如结构化分析方法和面向对面向数据分析方法的适应面不如结构化分析方法和面向对象的分析方法广泛，但在某些领域中仍具有一定的优越性。象的分析方法广泛，但在某些领域中仍具有一定的优越性。 形式化需求描述方法具有精确、无歧义、可数学推演等优形式化需求描述方法具有精确、无歧义、可数学推演等优点，软件系统中的某些关键部分采用形式化方法将有助于提高点，软件系统中的某些关键部分采用形式化方法将有助于提高软件质量。软件质量。 为了克服形式化方法难于理解、难于使用的缺点，可视形为了克服形式化方法难于理解、难于使用的缺点，可视形式化以及形式化方法和式化以及形式化方法和CASECASE工具相结合是行之有效的技术途径。工具相结合是行之有效的技术途径。第七章第七章 面向数据的分析方法与形式化方法面向数据的分析方法与形式化方法2024/8/2669国防科技大学计算机学院 谢谢谢谢2024/8/2670国防科技大学计算机学院
