软件工程SoftwareEngineering课件

软件工程

SoftwareEngineering

国防科技大学计算机学院2004.07齐治昌教授，谭庆平教授，宁洪教授，董威博士2023/7/201国防科技大学计算机学院第七章面向数据的分析方法与

形式化方法前面介绍的面向数据流和面向对象的分析是目前被广泛采用并具有较好发展潜力的需求分析方法。然而，在软件开发实践中仍有其它一些方法可供分析人员选择，它们在各自适用的领域也表现出了一定的优越性和生命力。这些方法包括面向数据结构的系统开发方法(DSSD)，Jackson系统开发方法(JSD)以及形式化软件规格说明技术。前两种统称为面向数据的需求分析方法。2023/7/202国防科技大学计算机学院面向数据的分析方法与形式化方法特点以信息对象及其操作为核心进行需求分析，与面向对象分析相似。复合信息对象具有层次结构，并且可按顺序、选择、重复三种结构分解为成员信息对象。提供将层次信息结构映射为程序结构的机制，从而为软件设计奠定较好的基础。第七章面向数据的分析方法与形式化方法2023/7/203国防科技大学计算机学院7.1面向数据结构的系统开发方法DSSD起源于七十年代Warnier在信息领域分析方面的杰出工作。利用顺序、选择、重复三种结构表示信息的层次分解，并指出可以从信息层次结构推导出程序结构。KenOrr对Warnier的工作进行了扩充，引进了数据流和处理功能，从而发展成为一种需求分析方法。本节介绍

Warnier图DSSD方法创建实体图、信息过程图、Warnier-Orr原型图。第七章面向数据的分析方法与形式化方法2023/7/204国防科技大学计算机学院面向数据结构的系统开发方法(1)首版标题新闻国内新闻本地新闻(2)商业金融版股市行情商业新闻广告(3)文化体育版文化、体育新闻散文新书评论7.1面向数据结构的系统开发方法2023/7/205国防科技大学计算机学院7.1.1Warnier图Warnier图是一种表示信息层次结构的紧致机制。Warnier图具有树形层次结构，可以用另外一些Warnier图继续分解图中的叶结点。例报纸自动组版系统图，花括符内的信息条目构成顺序关系，园括符内的数字表示重复次数，如，广告可以有1至5条，股市行情出现0到1次。符号“”表示不可兼具的选择关系。7.1面向数据结构的系统开发方法2023/7/206国防科技大学计算机学院7.1.2DSSD方法基于DSSD需求分析方法的步骤(1)标识与应用问题有关的实体。(2)创建一种类似于数据流图的信息—过程图。(3)创建Warnier-Err原型图。在详细介绍DSSD的具体步骤之前，首先用数据流图描述一个基于计算机的软件专卖店管理系统，见图7.2.注意，数据流图并非DSSD的组成部分。图7.2仅用于说明后面将要用到的应用问题实例。7.1面向数据结构的系统开发方法2023/7/207国防科技大学计算机学院软件专卖店管理系统的数据流图表示7.1面向数据结构的系统开发方法2023/7/208国防科技大学计算机学院1.标识实体图在DSSD中，与应用问题有关的实体及它们之间的信息流用实体图表示。它与面向对象分析中的对象消息传递图有相似之处，因此，识别实体和信息流的方法也类似于面向对象分析。7.1面向数据结构的系统开发方法2023/7/209国防科技大学计算机学院标识实体图在DSSD中，分析人员可通过对下述问题的回答来生成实体图(1)软件系统必须处理哪些信息项?(2)信息项的生产者和消费者分别是哪些实体?上述问题的有关实体是：客户、订单处理员、邮寄员、银行、结算员、管理员和邮局，见图7.3(a)。订单处理员的实体图如图7.3(b)所示。当所有实体的实体图都构造完成后，将它们综合起来便形成整个目标软件系统的实体图，见图7.4。

7.1面向数据结构的系统开发方法2023/7/2010国防科技大学计算机学院标识实体图7.1面向数据结构的系统开发方法2023/7/2011国防科技大学计算机学院标识实体图7.1面向数据结构的系统开发方法2023/7/2012国防科技大学计算机学院2.创建信息—过程图DSSD中的信息—过程图与数据流图的作用类似，都是用来表示信息流及其处理功能的。信息—过程图从每个实体的输出信息流开始，逆向寻找用于生成该输出信息的输入信息流及相应的处理功能。7.1面向数据结构的系统开发方法2023/7/2013国防科技大学计算机学院3.创建Warnier-Orr原型图DSSD方法分析人员以表格形式给出主要的输出信息元素精确地表示为Warnier-Orr图7.1面向数据结构的系统开发方法2023/7/2014国防科技大学计算机学院创建Warnier-Orr原型图7.1面向数据结构的系统开发方法2023/7/2015国防科技大学计算机学院7.2Jackson系统开发方法七十年代Jackson提出了软件工程领域中著名的Jackson方法，当时它只用于软件设计。八十年代初，Jackson又对它进行了多方面的扩充和完善，最终发展成为一种需求分析方法。Jackson方法的核心思想是：根据作用于数据的行为序列的结构(顺序、选择与重复)，建立目标软件系统的模型，然后在软件设计阶段将模型演化为相应的程序结构。第七章面向数据的分析方法与形式化方法2023/7/2016国防科技大学计算机学院Jackson系统开发方法Jackson方法在需求分析阶段的主要步骤(1)标识实体与行为。(2)生成实体结构图。(3)创建软件系统模型。7.2Jackson系统开发方法2023/7/2017国防科技大学计算机学院7.2.1标识实体与行为Jackson方法针对初步需求分析形成的用户需求描述进行语法分析。名词及名词短语是潜在的实体，相关的动词构成实体的潜在行为。分析人员根据应用问题的边界及自己的理解，决定对潜在实体和行为的取舍。7.2Jackson系统开发方法2023/7/2018国防科技大学计算机学院标识实体与行为例7.1

某大学决定将分处两地的校园用直达交通车连接起来。在每个校园设一个站，站内配置一个按钮。学生通过按钮请求交通车搭载。交通车应尽快满足学生的请求。空闲时，交通车停在任意站等候。分析人员可从“大学”、“校园”、“交通车”、“车站”、“学生”、“按钮”等名词中选取与应用问题相关实体、行为、状态。相关的实体：“交通车”、“车站”、“按钮”。相关的行为：“到站”、“离站”、“按键”。“交通车”的状态：“等候”和“运行”。7.2Jackson系统开发方法2023/7/2019国防科技大学计算机学院7.2.2生成实体结构图在Jackson方法中，实体结构是指实体在时间坐标系中的行为序列。这种序列以顺序、选择和重复三种结构进行复合。Jackson给出的实体结构图示机制如图7.7所示。其中的子结点既可以是行为，也可以是子实体。在后一情况下，子实体应该继续分解，不能作为实体结构图的叶结点。7.2Jackson系统开发方法2023/7/2020国防科技大学计算机学院实体结构图的图形记号7.2Jackson系统开发方法2023/7/2021国防科技大学计算机学院实体结构图的图形记号7.2Jackson系统开发方法2023/7/2022国防科技大学计算机学院7.2.3创建软件系统模型为了创建目标软件系统的模型，Jackson方法要求分析人员首先用图7.9所示的图形记号建立系统规格说明图(SystemSpecificationDiagram,SSD)。“数据流”(DataStream)记号表示现实世界中的过程或装置不断地向目标软件系统中的相应过程发送数据，后者以先进先出方式消费数据。两者之间的缓冲区容量是无限的。“状态向量”(StateVector)记号表示在两者之间存在状态向量，发送方设置状态向量，接收方读取状态向量。7.2Jackson系统开发方法2023/7/2023国防科技大学计算机学院创建软件系统模型站内按钮和目标软件中的按钮处理过程之间以“数据流”方式连接交通车和交通车控制过程之间则应以“状态向量”方式连接。7.2Jackson系统开发方法2023/7/2024国防科技大学计算机学院系统规格说明图示例

利用Jackson给出的“结构正文”(StructureText)将实体结构图和系统规格说明图综合起来，并针对目标软件系统中的每一过程用正文方式给出更为精确、更为详尽的描述。7.2Jackson系统开发方法2023/7/2025国防科技大学计算机学院正文描述BUTTON－1readButtonDown信号

PUSH－BODYitrwhileButtonDown／＊循环结构＊／

PUSH／＊按键处理＊／

readButtonDown信号

PUSH－BODYendBOTTON－1end7.2Jackson系统开发方法2023/7/2026国防科技大学计算机学院正文描述SHUTTLE－1seq／＊顺序结构＊／

read状态向量

WAIT－BODY1itrwhileWait(1)／＊如果状态向量中等待标志置位，则循环等待＊／read状态向量

WAIT－BODY1endLeave(1)／＊控制交通车离开站1＊／

TRANSIT－BODY1itrwhileTransit(1)／＊如果状态向量中运行标志置位，则一直运行＊／read状态向量

TRANSIT－BODY1end

7.2Jackson系统开发方法2023/7/2027国防科技大学计算机学院正文描述SHUTTLE－BODY1itr／＊往返重复运行＊／

STATIONseqArrive(i)／＊控制交通车减速，准备停靠站I＊／WAIT－BODYitrwhileWait(i)／＊如果状态向量中在站i的等待标志置位，则循环等待＊／read状态向量

WAIT－BODYendLeave(i)TRANSIT－BODYitrwhileTransit(i)read状态向量

TRANSIT－BODYendSTATIONendSHUTTLE－BODY1endArrive(1)SHUTTLE－1end7.2Jackson系统开发方法2023/7/2028国防科技大学计算机学院正文描述

Wait(i)Transit(i)(i=1,2)

现实世界的交通车SHUTTLE－0向软件过程SHUTTLE－1发出的状态向量的一部分。7.2Jackson系统开发方法2023/7/2029国防科技大学计算机学院结构正文的结构图7.2Jackson系统开发方法2023/7/2030国防科技大学计算机学院7.3形式化方法前面对数据流图、面向对象的需求表示图等语言机制都未给出数学意义上严格的语法和语义说明。因此，这些需求模型都或多或少地带有不精确性、不完全性，甚至不一致性。许多软件开发实践希望借助于形式化方法严格地定义用户需求，并通过数学推演确保需求定义的一致性和完全性。对于正确性至关重要的实时嵌入式系统关键部件的软件开发，形式化方法更是不可或缺的。第七章面向数据的分析方法与形式化方法2023/7/2031国防科技大学计算机学院形式化方法主要思想Z语言形式化规格说明语言简单实时操作系统内核的形式化需求描述方法。形式化方法的现状和发展趋势。7.3形式化方法2023/7/2032国防科技大学计算机学院7.3.1主要思想形式化需求分析方法的主要思想是利用形式化规格说明语言定义用户需求，并采用数学推演的方法证明需求定义的性质，例如一致性、实时系统的活性(Liveness)和公平性(Fairness)等。对于复杂的应用问题，尽管无法验证整个需求定义的完全性，但仍有可能为避免某些要点的疏漏而建立数学断言，然后予以形式证明或反驳。形式化方法是克服需求分析阶段不精确性、不一致性和不完全性的有效途径。7.3形式化方法2023/7/2033国防科技大学计算机学院主要思想形式化规格说明语言的组成语法语义数学推演规则规则不仅说明了某些数学性质在软件规格说明中是否成立，也说明了软件实现与软件规格说明之间的关系。7.3形式化方法2023/7/2034国防科技大学计算机学院规格说明语言的语法规格说明语言的语法集合论数理逻辑代数学Z语言集合论∈属于不属于子集关系∩集合交∪集合并函数符号逻辑符号任意存在～非∧合取∨析取大多数宽谱语言包括，高级程序设计语言的控制流机制，如顺序、条件、循环等等。7.3形式化方法2023/7/2035国防科技大学计算机学院规格说明语言的语义规格说明语言的语义所有语法符号含意的数学描述。经典语义定义方法：指称语义代数语义操作语义7.3形式化方法2023/7/2036国防科技大学计算机学院规格说明语言的语义指称语义数学地确定规格说明语言的语义域，将所有语法成分映射为语义域中的对象或语义域上的函数。代数语义将软件规格说明中的某些结构化设施(例如抽象数据类型)解释为多类代数，通过代数工具(例如范畴论)研究规格说明的代数性质、模块组装运算以及软件设计相对于规格说明的实现关系。操作语义形式地定义抽象机，将规格说明的语义解释为抽象机的动作序列。7.3形式化方法2023/7/2037国防科技大学计算机学院形式化规格说明语言的推演规则形式化规格说明语言的推演规则与数学基础和语义定义方法密切相关。以集合论和谓词逻辑为基础的Z语言就包含了原数学系统中有关的规则。规则必须在规格说明语言的语义系统中可证。规则是派生的语义定义，它们可以直接应用于软件规格说明的性质证明并简化推演过程。7.3形式化方法2023/7/2038国防科技大学计算机学院规则：if—then—else结构的表示形式Eval(e，e′)表示表达式e可计值为e′。第一条规则的直观意义如果e0能计值为TRUE，e1能计值为e1，则表达式ife0thene1elsee2

可计值为e1.7.3形式化方法2023/7/2039国防科技大学计算机学院7.3.2形式化规格说明语言用形式化规格说明语言描述用户需求VDM的Meta—Ⅳ，CSP和Z是具有代表性的形式化规格说明语言。Z语言的语法设施及其语义说明实例及需求描述过程7.3形式化方法2023/7/2040国防科技大学计算机学院1.基本语法成分

Z的基本语法成份主要取自带类型的集合论和一阶逻辑。7.3形式化方法2023/7/2041国防科技大学计算机学院基本语法成分7.3形式化方法2023/7/2042国防科技大学计算机学院2.结构化设施——框架(Schema)框架变元说明用一阶逻辑公式表示的变元取值约束条件语法形式——框架名称——变元说明约束条件全局常元和函数的语法形式常元及函数说明(说明常元及函数的类型)约束条件(说明常元及函数的取值约束)7.3形式化方法2023/7/2043国防科技大学计算机学院结构化设施——框架(Schema)记号△S

如果框架S中的所有变元为v1，…，vm，所有的约束条件为P１，…，Pn，那么框架△S中的变元为v１，…，vm，v’1,…，v’m，约束条件为P1，…,Pn，P’1，…，P’n，其中vi与v’i的类型相同，P’j是将Pj中所有vi的出现替换为v’i得到的约束条件(i=1,…，m,j=1,…，n)。单引号“′”用来区分操作发生前、后的变元取值。记号s’=s

表示在操作发生前、后框架S中的所有成员不发生变化(变元取值不变，约束条件也保持相同的真假值)。7.3形式化方法2023/7/2044国防科技大学计算机学院7.3.3形式化需求描述例实时操作系统内核用Z语言描述软件需求系统状态的表示普通进程调度表示中断处理进程调度表示7.3形式化方法2023/7/2045国防科技大学计算机学院1.实例描述——实时操作系统内核实时操作系统内核的主要任务提供进程调度和中断处理机制。每个进程都有就绪标志，系统从已就绪进程中选择一个作为当前进程。当没有中断请求时，系统运行当前进程直至该进程显式释放处理器，然后系统再选取当前进程。当中断发生时，系统根据优先级高低选择最紧急的中断并运行相应的中断处理进程。优先级高的中断可以打断优先级低的中断。普通进程可将自己登录为某一优先级的中断处理进程。7.3形式化方法2023/7/2046国防科技大学计算机学院2.系统状态的表示引进类型PID表示所有进程标识符的集合。虚构的进程标识符none用来表示处理器的空闲状态。PID１表示不是none的所有进程标识符：none:PIDPID1：PPIDPID1=PID\｛none｝／＊PID1是除none外的所有进程标识符的集合＊／7.3形式化方法2023/7/2047国防科技大学计算机学院系统状态的表示进程调度机制框架—Scheduler—／*框架名称为Scheduler*／process:PPID1／*变元process,ready和current的说明*／ready:PPID1current:PIDreadyprocess／*约束条件*／current∈process∪｛none｝7.3形式化方法2023/7/2048国防科技大学计算机学院系统状态的表示process表示由进程调度机制控制的所有进程的集合。ready是所有就绪进程的集合。current是当前进程。框架Scheduler的约束条件readyprocess表示就绪进程必须是可调度的进程。约束条件current∈process∪｛none｝表示当前进程要么是可调度进程，要么是none.

7.3形式化方法2023/7/2049国防科技大学计算机学院系统状态的表示定义中断优先级的有穷集合ILEVELILEVEL:FN0ILEVEL／＊ILEVEL是除0之外的自然数的有穷集＊／不是中断处理进程的进程称为普通进程，普通进程的优先级定义为0。7.3形式化方法2023/7/2050国防科技大学计算机学院系统状态的表示中断处理机制的描述handler是内射函数，所以两个优先级不能共用同一中断处理进程。中断可以是活跃的，并且不是未屏蔽的,因为它可以在先前发生，而后被更高优先级的中断打断并屏蔽。集合active不仅包含当前正被处理的中断优先级，也包括那些先前发生，而后又被打断的中断优。7.3形式化方法2023/7/2051国防科技大学计算机学院系统状态的表示实时操作系统的内核由进程调度和中断处理机制综合构成.Kernel包含了Scheduler和IntHandler的变元说明和约束条件。新加的约束条件说明普通进程不能兼为中断处理进程，反之亦然。系统状态应由正在运行的进程及其优先级构成。7.3形式化方法2023/7/2052国防科技大学计算机学院系统状态的表示系统的调度策略7.3形式化方法2023/7/2053国防科技大学计算机学院3.普通进程调度普通进程调度操作启动普通进程(Start)设置或清除就绪标志(SetReady)控制进程临时或永久性让出处理器(Detach与Stop)当处理器空闲时选择新的进程运行(Select)7.3形式化方法2023/7/2054国防科技大学计算机学院普通进程调度启动普通进程(Start)7.3形式化方法2023/7/2055国防科技大学计算机学院普通进程调度当处理器空闲时选择新的进程运行(Select)7.3形式化方法2023/7/2056国防科技大学计算机学院普通进程调度控制进程临时或永久性让出处理器(Detach与Stop)7.3形式化方法2023/7/2057国防科技大学计算机学院普通进程调度Stop操作将永久性终止当前进程的运行——Stop——7.3形式化方法2023/7/2058国防科技大学计算机学院普通进程调度设置或清除就绪标志(SetReady)7.3形式化方法2023/7/2059国防科技大学计算机学院4.中断处理进程调度中断处理进程调度操作将普通进程登录为中断处理进程IntEnter中断屏蔽的设置与清除Mask中断响应Interrupt中断处理完成后相应的中断处理程序挂起IntWait将自身降格为普通进程IntExit7.3形式化方法2023/7/2060国防科技大学计算机学院中断处理进程调度

IntEnter操作定义7.3形式化方法2023/7/2061国防科技