资源描述
需需 求求 工工 程程金芝中国科学院数学与系统科学研究院第九讲：文档驱动方法第九讲：文档驱动方法需求文档的重要性四变量模型SCR需求方法形式化SCR和表演算机制总结从软件工程师的职责谈起从软件工程师的职责谈起工程师的职责之一：保证产品的适用性要求和应用专家准确、细致地沟通沟通必须以写下来的需求陈述为基础用户和实现者能够阅读和分析能够在产品开发完成后用于评估这个产品能够用于评定产品完成后的关于产品缺陷的争论没有文档，任何工程师做不到这一点发现需求是一门艺术，文档化需求并验证它的完整性是一门学科需求文档需求文档需求文档不表达如何开发产品,需求文档是关于将开发什么产品要做什么的描述三个术语描述：关于该产品的一些信息,可以不完整,但必须是真实的规格说明：该产品需求属性的一个描述,软件产品的外部可见的行为模型：具有产品的部分属性，以及可能不属于产品的属性，维护完整性一致性，方便验证好文档的作用好文档的作用可以描述已经存在的软件我们可以不用读代码就能够回答关于该软件的问题可以描述还不存在的软件程序员和客户可以就需求达成一致意见验证产品是否满足需求（测试和/或审查）可以建立工具检查规格说明可以建立工具模拟系统并检查系统文档可接受的标准文档可接受的标准描述必须比代码容易理解文档必须用一种不限制解决方案的方式陈述需求测试和证明最终能够自动化程序与其它工程产品不同吗？程序与其它工程产品不同吗？在计算机出现之前，工程师使用经典数学来描述和分析产品在计算机科学中，大多数研究者发明新的“语言”我们将软件作为产品来开发程序与其它工程产品不同吗？程序与其它工程产品不同吗？我们为什么不能简单地用我们习惯的数学来建模？传统产品是无生命的东西（X）我们需要描述被程序遵循的过程（X）功能不是连续的（）需求阶段的目的需求阶段的目的在开始构建产品之前，决定要构建什么在设计之前显式地说出是“什么决定”，而不是象设计中那样隐式地给出确定你构建的是必需的让用户在产品构建之前进行评判为软件开发者提供有组织的参考文档提供精确，一致的信息关于约束的问题只涉及一次让他们不用决定什么对用户来说是最好的补偿他们对环境的知识的缺少给他们足够的信息进行设计决策让他们准确地估计需要的时间和资源需求阶段的目的需求阶段的目的容许人员的更替为质量保证组提供参考文档测试设计不应该以来程序授权的需要质量保证组和程序员可能不一致说明实现相关的所有约束知道你面临什么为应付客户的变化提供某种形式的保护能够评判可行性和代价说明未来修订的约束两变量模型两变量模型硬件/软件系统的传统模型基于两个假设：系统具有输入和输出输出是输入的数学函数其中，输入是系统的实际物理输入数学函数可能很复杂并难以描述难以得到应用专家的审查四变量模型四变量模型在系统的外部，存在物理变量，一些是监视变量、一些是控制变量、一些两者都是外部设备感应监视变量，决定计算机的输入，读取计算机输出，影响控制变量的值系统需求说明在监视变量和控制变量之间希望存在的关系领域专家根据监视变量和控制变量来审查需求，而不是根据输入和输出变量软件需求使用输入和输出变量来描述四变量模型四变量模型影响系统行为的环境量由系统控制的环境量度量被监测的量设置被控制的量NAT：物理世界的法则核系统环境引入的约束REQ：系统必须维护的被监视的量和被控制的量之间的其他约束IN：从被监视的量到输入数据项的映射OUT：从输出数据项到被控制的量的映射四变量模型的关系四变量模型的关系整个系统：满足监视变量和控制变量之间的关系输入设备：满足监视变量和输入变量之间的关系输出设备：满足输出变量和控制变量之间的关系软件系统：满足输入设备和输出设备之间的关系识别和声明监视和控制变量识别和声明监视和控制变量识别监视变量：(mt1,mt2,mtn)识别控制变量：(ct1,ct2,ctp)主要的监视变量是系统外的东西，它的值应该影响系统的输入，比如：客户计量器的读数蒸汽温度主要的控制变量是系统外的东西，它的值应该由系统来决定，比如：操作者来计算机屏幕上看到的东西什么将出现在帐单上定义变量之间的关系定义变量之间的关系NAT关系：mt ctmt：m在t时刻的取值ct：c在t时刻的取值(mt,ct)NAT 当且仅当ct描述的环境控制量是环境约束在mt描述的环境监视量下是允许的REQ关系：mt ctmt：m在t时刻的取值ct：c在t时刻的取值(mt,ct)REQ 当且仅当ct描述的环境控制量是计算机系统在mt描述的环境监视量下是允许的关系满足的条件1.domain(REQ)domain(NAT)2.domain(REQNAT)=domain(REQ)domain(NAT)其中，（1）表示系统需求文档的完整性；（1）和（2）表示系统需求文档的可行性定义变量之间的关系定义变量之间的关系IN关系：mt itmt：m在t时刻的取值it：c在t时刻的取值(mt,it)IN 当且仅当在mt描述的环境监视量下输入设备正常工作时可能产生的值OUT关系：ot ctot：m在t时刻的取值ct：c在t时刻的取值(ot,ct)OUT 当且仅当输出设备正常工作时并输出ot描述的取值时可能的环境控制量的取值文档化软件需求文档化软件需求软件需求由系统需求决定：REQ(mt,ct)IN(mt,it)OUT(ot,ct)NAT(mt,ct)实际软件描述为SOF(it,ot)：(it,ot)SOF 当且仅当ot描述的是软件在输出it描述的取值时可能的产生的输出变量的取值软件需求文档的检查软件需求文档的检查完整包含上述内容验证REQ在NAT定义的条件下的满足系统可行性条件一些其它简单检查SOF中出现的输入变量都是IN中的输入变量OUT中出现的输出变量都是SOF中的输出变量IN中出现的监视变量都是REQ中的监视变量OUT中出现的控制变量都是REQ中的控制变量REQ和NAT中的变量相同软件需求的可接受性软件需求的可接受性让软件是可接受的，SOF必须满足：mt it ot ct IN(mt,it)SOF(it,ot)OUT(ot,ct)NAT(mt,ct)REQ(mt,ct)采用功能表述：mt mt domain(NAT)(REQ(mt)=OUT(SOF(IN(mt)更简洁的表述：（NAT（INSOFOUT）REQ四变量模型蕴涵的需求过程四变量模型蕴涵的需求过程定义“控制变量”的完整列表定义“监测变量”的完整列表对每个监测变量，说明其可能的取值集合（如果和时间相关，则定义为时间函数）。这个监测变量的取值集合是NAT的值域对每个控制变量，将它的取值描述为监测变量的取值的函数四变量模型蕴涵的需求过程四变量模型蕴涵的需求过程说明系统：“理想”系统的行为假设能够获得被检测系统变量的精确值假设能够计算出被控制系统变量的精确值期望要保持的监测变量和控制变量之间的关系，用NAT和REQ表示定义可允许的软件行为：对软件系统行为的可容忍的程度，包括：对度量被检测的属性值和计算被控制的属性值的时间延迟和精度要求，用IN和OUT表示 SCR需求方法需求方法SCR：Software Cost Reduction提出：Heninger,K.L.,80年代初期成功应用领域：A-7操作飞行程序潜水艇通讯系统加拿大Darlington核电站安全组件Lockheeds C-130j操作飞行程序基本概念和表示法基本概念和表示法基本表示法表表示法状态机基本概念和表示法基本概念和表示法构造子一：模式类定义在被监护变量上一个状态机其中的状态称为系统模式变迁由事件触发 模式类刻画了系统运行的模式类刻画了系统运行的模式类刻画了系统运行的模式类刻画了系统运行的一段相互关联的上下文一段相互关联的上下文一段相互关联的上下文一段相互关联的上下文 主要目的是划分状态集合，主要目的是划分状态集合，主要目的是划分状态集合，主要目的是划分状态集合，简化函数的描述简化函数的描述简化函数的描述简化函数的描述基本概念和表示法基本概念和表示法构造子二：项定义在输入变量，模式，或者其它项之上的辅助函数是一个抽象概念，或者高层概念引入的目的是为了减少冗余说明基本概念和表示法基本概念和表示法构造子三：条件定义某个事件点上的一个或多个系统实体上的谓词，比如：关系式等其中，系统实体可以是输入/输出变量，模式或者项刻画系统某个特定可度量时期的某方面的性质当一个条件的值从真变为假，或者从假变为真，就发生一个事件。从这个意义上说，条件主要用于刻画事件发生的时机基本概念和表示法基本概念和表示法构造子四：事件当系统的任何实体的值发生了变化，就有一个事件出现SCR描述两类事件发生的时机：T（c）：当条件c变为真F（c）：当条件c变为假由检测变量的变化引起的事件为检测事件在特定条件下发生的事件为条件事件T（c）WHEN d：在条件d为真的情况下，当条件c变为真F（c）WHEN d：在条件d为真的情况下，当条件c变为假案例：安全注入系统案例：安全注入系统基本需求：负责打开和关闭安全注入阀。需要监测水压，当水压低于阈值以下时，打开注入阀，向反应堆内核填加冷冻剂系统操作员可以用Block（或Reset）开关阻止安全注入（或恢复安全注入）安全注入系统：安全注入系统：SCR需求需求Overridden：表示安全喷射被阻止三个被三个被监测量监测量每个感应器产每个感应器产生一个输入量生一个输入量被控制被控制的量的量两个模两个模式类式类重载重载三个系三个系统模式统模式安全注入系统：安全注入系统：SCR需求需求系统有两个模式类：“压力”模式“重载”模式模式类“压力”中有三个系统模式：压力太低，WaterPress=Low允许的范围，Low WaterPress=Permit压力高，Permit WaterPressSCR需求的表示需求的表示模式变迁表：定义软件可以处于的模式（状态）及其模式变迁一个系统将包含不同的模式类，每个模式类有一个模式表，展示引起模式之间的变迁的条件函数表示形式：模式 事件 模式当前模式事件下一模式TooLowT(WaterPress Low)PermittedPermittedT(WaterPress Permit)HighPermittedT(WaterPress Low)TooLowHighT(WaterPress，v TY(r)复合条件：简单条件通过连接词组合而成连接词：，形式化形式化SCR：事件事件基本表示法T事件种类原始事件：T(r=v),rRF,vTY(r)监测事件：T(r=v),rIR,vTY(r)基本事件：T(c),c是一个简单条件简单条件事件：T(c)WHEN d,T(c)是一个基本事件，d是一个简单条件或者复合条件条件事件：简单条件事件的和取或析取事件的语义事件的语义简单事件T(c)=c c如果c=rv，则c=(rv)=rv简单条件事件T(c)WHEN d=c c d老状态下老状态下老状态下老状态下的条件的条件的条件的条件c c新状态下新状态下新状态下新状态下的条件的条件的条件的条件c c形式化形式化SCR：事件例事件例T(Block=On)WHEN Reset=OffBlockOn Block=On Reset=Off形式化形式化SCR：系统模型系统模型一个系统为一个四元组：Em输入事件的集合S可能的系统状态的集合s0初始状态T系统变换，为Em S到S上的一个部分函数，表示被允许的系统状态变迁形式化形式化SCR：系统模型系统模型假设：单输入假设：每次系统变迁正好只有一个监测事件出现同步假设：系统在响应下一个监测事件之前，对当前的监测事件的响应必须全部完成实体排序实体排序构造实体的新状态依赖集监测变量的新状态依赖集为空由条件表定义的实体，其新状态依赖集包含所关联的模式类名，和出现在条件表中的所有实体名由事件表或模式变迁表定义的实体，其新状态依赖集包含出现在表中作为一个基本事件的一部分的所有实体新状态依赖集构成了RF上的一个偏序关系SCR需求的表示需求的表示条件表描述从模式和条件到控制变量或项上的一个函数函数表示形式：模式 条件 控制变量的取值|项的取值当前模式条件High,PermittedTrueFalseTooLowOverridden OverriddenSafetyInjectionOffOnSafetyInjection在新状态中依赖模式类Pressure和项OverriddenSCR需求的表示需求的表示模式变迁表：定义软件可以处于的模式（状态）及其模式变迁一个系统将包含不同的模式类，每个模式类有一个模式表，展示引起模式之间的变迁的条件函数表示形式：模式 事件 模式当前模式事件下一模式TooLowT(WaterPress Low)PermittedPermittedT(WaterPress Permit)HighPermittedT(WaterPress Low)TooLowHighT(WaterPress Permit)Permitted模式类Pressure在新状态中依赖WaterPressSCR需求的表示需求的表示事件表描述从模式和事件到控制变量或项的取值上的一个函数函数表示形式：模式 事件 控制变量的取值|项的取值当前模式 事件 HighFalseT(Inmode)TooLow,PermittedT(Block=On)WHEN Reset=Off T(Inmode)T(Reset=On)OverriddenTrue False Overridden在新状态中依赖模式类Pressure和监测变量Block和Reset偏序关系序列偏序关系序列一种可能性：R=表函数：条件表表函数：条件表当前模式条件High,Permitted TrueFalseTooLowOverridden OverriddenSafetyInjectionOffOn表函数：事件表表函数：事件表当前模式事件下一模式TooLowT(WaterPress Low)PermittedPermittedT(WaterPress Permit)HighPermittedT(WaterPress Low)TooLowHighT(WaterPress Permit)Permitted表函数：事件表表函数：事件表表函数：变迁表表函数：变迁表当前模式事件下一模式TooLowT(WaterPress Low)PermittedPermittedT(WaterPress Permit)HighPermittedT(WaterPress Low)TooLowHighT(WaterPress Permit)Permitted表函数：变迁表表函数：变迁表自动一致性检查自动一致性检查合适的语法类型正确性变量和模式定义的完整性初始值：模式类、输入变量、输出变量可达性：模式类忠的每个模式都是初始模式静态可达的互斥性：条件相互之间是互斥的覆盖：条件表中的变量，其域中每点有定义无循环性：实体依赖无循环规格说明的验证规格说明的验证检验的方面包括需求描述的良构性语法：我们是否正确地使用了这种表示法类型检查：我们是否正确地使用了每个变量互斥性：模式表的行之间是否存在重叠保证我们有确定的状态机覆盖面：每个条件表是否为所有可能的条件定义了值状态不变性和变迁不变性模式可达性：是否存在总是不能到达的模式循环性检查：我们是否在定义变量的时候用到了该变量本身SCR方法工具集方法工具集SCR*总结：文档驱动方法的特点总结：文档驱动方法的特点强调文档的内容而不仅仅是格式强调建立文档的标准而不仅仅是过程，这些标准可以用来验证文档的有效性强调严格的、可读性强的文档表示方法，Tabular表达式既具有严格的定义又具有较强的可读性总结：使用形式化方法总结：使用形式化方法有选择地使用形式化方法形式化的量可以变不需要构建完全的形式化模型应用到最关键的部位在存在的分析技术比较薄弱的地方使用不需要形式化分析每个系统特性比如：只检查安全性不需要在开发的每个阶段都使用形式化方法比如，用于为需求建模，但不对系统的设计形式化能够选择特定抽象级别（模型的详细程度）来建模总结：使用形式化方法总结：使用形式化方法轻量级的形式化方法已经变得很流行，作为使这个技术实用的一种方式有选择地应用形式化方法到部分的建模中存在问题存在问题主要针对实时系统，尽管后来的研究引入了非功能性需求的形式定义方法，但对非实时系统不很使用对需求的获取和精化缺乏具体的指导，只说明需要给出什么样的文档对更复杂的软件的支持程度不够未来的发展未来的发展开拓应用领域，特别是非实时的应用进行更多的实际应用，开发成功范例与其它需求工程方法结合，给出完整的需求工程过程开发更完善和全面的支撑工具
展开阅读全文