（计算机应用技术专业论文）早期需求工程中的形式化建模与模型检验应用研究.pdf

早期需求工程中的形式化建模与模型检验应用研究 摘要 软件需求分析是整个软件开发过程中极为重要的环节，它不仅仅 是技术问题，也涉及了组织、管理、商务、社会等问题。在早期的需 求分析过程中，描述建立了软件系统的动机、意向和原则，使得开发 能更好地理解组织关系和活动者的依赖关系，明确各种决策的原则； 解决意向系统如何满足组织的目标，为什么需要这样的系统，有什么 替代方法可以考虑，替代方法对用户的影响，用户的兴趣如何满足等。 早期需求的另一个重要特性就是获取系统的非功能需求( 即软目标) ， 即质量属性，如精确性、性能、安全性、可调整性等。所以在早期需 求开发中如能发现系统的潜在问题将比在后期开发中花费在解决所 暴露的问题节省数百倍的开销。 我们针对网上教学系统的特点对其进行早期的需求分析。提取了 系统主要角色细化分析了他们的意图、任务、资源依赖。然后用图形 化的方法对我们的分析进行了呈现，建立了系统的事务模型。通过程 序的自动翻译图形化表示的记录文件生成了相对应的模型形式化表 示的语言框架代码描述。经过手工加入更多的模态逻辑指定后形成了 系统完整的形式化语言描述的模型。为实现模型检查我们采用了 n u s m v 模型检查工具，并将前面所建立的模型形式化语言描述转换 为n u s m v 模型检查工具可以接受的脚本语言从而实现了对我们对模 型的检查过程。根据检查的结果一步步调整修改逻辑关系和指定，最 后得出趋向于反应系统真实情况的形式化模型表述，并在论文的附录 中给出了相应的结果和我们建立的模型。 关键词早期需求，形式化方法，模型检查 t h ea p p l i e dr e s e a r c ho ff o r m a l m e t h o da n d m o d e lc h e c k i n gi ne a r l y r e q u i r e m e n t e n g i n e e r i n g a b s t r a c t s o f t w a r e r e q u i r e m e n ta n a l y s i s i sa k e yp r o c e s s i ns o f t w a r e d e v e l o p m e n t i t sn o to n l yat e c h n i c a lp r o b l e mb u ta l s oap r o b l e mt h a t a s s o c i a t e dw i t ho r g n i z a t i o nm a n a g e r m e n tb u s i n e s sa n ds o c i a lr e l a t i o n s h i p i nt h ep r o c e s so fe a r l y r e q u i r e m e n t ， i th a se s t a b l i s h e dt h ea i m ， i n t e n t i o n ，a n db a s i so fs o f t w a r es y s t e m i tb e n e f i tt h el a t e rd e v e l o p m e n t i nb e t t e ru n d e r s t a n d i n go fs y s t e mo r g n i z a t i o na n d a c t i t i t i e s d e p e n d e n c y r e l a t i o n s h i pc l e a r i f yt h ep o l i c yp r i n c i p l e a l s ob e n e f i tb o t ht h ep r o b l e mo f h o wt os o l v et h es y s t e mi n t e n t i o nt os a t i s 黟t h en e e do fo r g n i z a t i o na n d c l e a r i f yw h a tt h ea l t e r n a t i o nc o u l db em a d et ot h es y s t e m ，t h ei m p a c t a f t e r m a k i n g t h ea l t e r n a t i o n a n o t h e r c r i t i c a l p r o p e r t y o fe a r l y r e q u i r e m e n ta n a l y s i si sw ec a nc a p t u r et h en o n f u n c t i o nn e e d so ft h e s y s t e mq u a l i t y a t t r i b u t e ss u c ha s a q u r a c y ，d e g r e eo fs a f e t y ， f i m c t i o n a l i t ya n da d j u s t a b i l i t y i fw ec a n td e t e c ta n df i xt h ep o t e n t i a l p r o b l e mi ne a r l yr e q u i e m e n ta n a l y s i s ，i nl a t e rd e v e l o p m e n t p r o c e d u r ei n o r d e rt of i xt h ep r o b l e mo c c u ri nt h a tp e r i o dm a yc o s tm o r et h a nt w o h u n d r e dt i m e st h a nt h ec o s tf o rw et of i xt h ep r o b l e mo c c u ri nr e q u i e m e n t i a n a l y s i s w ed oo u re a r l yr e q u m e n ta n a l y s i st o w a r d sa e l e a r n i n gs y s t e m e x t r a c t i n gt h em a i na c t o ri nt h es y s t e m ，t h e nd i s c o v et h ed e p e n d c yo f t h e i ri n t e n t i o n ，t a s ka n dr e s o u r c ea m o n gt h e m v i ag r a p h i c a lm e t h o d w e v em o d e l e dt h e i rr e l a t i o n s ，a n du s eo u rp r o g r a mt o g e n e r a t et h e s c r a t c ho ft h e i rf o r m a ld e s c r i p t i o n l a t e rt h ef o r m a l d e s c r i p t i o n i s a c c o m p l i s h e db ya d d i n gm o r el o g i cs p e c i f i c a t i o n st oi t t h e nw et a n s l a t e t h ed e s p c r i t i o nt ot h el a n g u a g et h a tc a nb ea c c e p t e db yn u s m vm o d e l c h e c k i n gt o o l s ，a n du s et h a tt o o l st oc h e c k i n gt h el o g i cs p e c i f i c a t i o n b a s e do nt h er e p o r to fr u n n i n gr e s u l tg e n e r a t e db yn u s m v ，w e a d j u s t m e n ta n dm o d i f yt h em o d e s ot h a tt oc o r r e c ti ts t e pb ys t e p f i n a l l y w eg e tt h em o d e lw i c hc a nr e p r e s e n tt h er e a l i t y i nt h ea p p e n d i xo u r m o d e la n dt h ec h e c k i n gr e s u l ti sp r e s e n t e d k e yw o r d s e a r l yr e q u i r e m e n t ，f o r m a lm e t h o d ，m o d e lc h e c k i n g 浙江工业大学 学位论文原创性声明 本人郑重声明：所提交的学他论文是本人在导师的指导f ，独立进行 研究l 作所取得的研究成果。除文中已经加以标注引用的内容外，本论文 不包含其他个人或集体已经发表或撰写过的研究成果，也不含为获得浙江 工业大学或其它教育机构的学位证书而使用过的材料，列本文的研究作出 重耍贡献的个人和集体，均已在文- p 以叫确方式标明。本人承担本声明的 法律责任。 作者虢a 砷 嗍砌6 年f 月1 日 学位论文版权使用授权书 本学位论文作者完全了解学校有关f 留、使用学位论文的规定，同意 学校保留并向国家有关部门或机构送交论文的复印件和电子版，允许论文 被查阅和借阅。本人授权浙江。l 业大学可以：恪本学位论文的全部或部分内 容编入有关数据库进行检索，可以聚用影印、缩印或扫描等复制手段保存 和汇编本学位论文。 本学位论丈属于 l 、保密口，在年解密后适用本授权书。 2 、4 i 保密口。 ( 清任以上相应力框内打“4 ”) 作者签名 导师签名 硼 k 卜 u 期? 聊6 年g 月日 闩期2 卯6 年6 月) 日 1 1 论文的背景 第一章绪论 软件需求分析是整个软件开发过程中极为重要的环节，它不仅涉及到技术问 题，需要考虑系统的功能问题，也涉及了组织、管理、商务、社会等问题，即要 也需要考虑非功能问题。尤其在早期的需求分析过程中，需要描述建立软件系统 的动机、意向和原则( 为什么) ，以便能更好地理解组织关系和活动者的依赖关 系，明确各种决策的原则；解决意向系统如何满足组织的目标，为什么需要这样 的系统，有什么替代方法可以考虑，替代方法对用户的影响，用户的兴趣如何满 足等。早期需求的另个重要问题就是获取系统的非功能需求( 即软目标) ，即 质量属性，如精确性、性能、安全性、可调整性等。 在软件需求分析过程中，目标一直是一个非常重要的组成部分，是系统要达 到的目的。通常系统的需求都可由其组织、操作和技术要求来决定，即由各种功 能需求和非功能需求来决定。其中，需求分析内容可分五类： ( 1 ) 组织关系：即明确哪些是相关活动者，这些活动者要做什么，他们有什 么义务，有什么能力? ( 2 ) 目标关系：即哪些目标是相关的? 他们如何关联? 如何相互满足? ( 3 ) 通信问题：即活动者之间如何交互? 如何对话? ( 4 ) 面向过程分析：即相关的商业和计算过程是什么? 哪些活动者承担这些 过程? ( 5 ) 面向目标分析：如何定义支持目标的意向、愿望、信念等，以及相互关 系。 从需求分析的过程上又可分为早期需求分析和后期需求分析。早期需求分析 主要是分析、研究系统的组织关系，建立组织模型，主要明确各活动者及其相关 目标；如分析和收集项目负责人的各种意向，即通过面向目标和软目标的分析， 得到系统的功能与非功能需求；后期需求分析是通过描述系统与环境的关系，确 定系统的功能与非功能需求，生成面向设计和实现的需求规范文档，同时对各种 非功能需求进行细化分析。 多伦多大学的p 模型框架旨在实现早期的需求建模，在该模型中提出了活 动者、目标和活动者依赖关系等概念，着重描述活动者的各种意向，并为这些意 向建立目标模型，以此来实现面向组织的需求分析；在该模型中，定义了一些重 要概念，如依赖概念，通过这些依赖关系柬实现系统间的各种约束：目标的实现、 任务的完成、资源的利用等；以此描述软件系统建立的动机、意向和原则。同时， 在该模型框架中提出了非功能需求( 软目标) 概念，即各种性能、质量属性等， 以解决意向系统如何满足组织的目标，并对各种替代方法进行评价，明确各种决 策的原则。i + 建模框架提供了一套图形化需求分析工具，即o m e ( o r g a n i z a t i o n m o d e l i n ge n v i r o n m e n t ) ，它提供了多种构件，用于表示需求过程中的各种概念， 主要分为三类：意向元素，意向关系和活动者。其中，意向元素包括目标、任务、 软目标、信念和资源。意向关系包括：m e a n s e n d s ，分解关系，贡献关系，相互 关系和依赖关系等。 模型检验是对有限状态系统的一种形式化确认方法，具体做法是：采用一种 形式语言描述系统的规范说明，构造一种算法来遍历根据系统规格说明设计的实 现模型，最后确认实现模型是否满足系统的规范说明。模型检查器能有效地搜索 有限状态模型所有的可能事件序列来判定系统性质是否得到满足。如果性质不满 足，则系统输出一个以状态序列形式表示的反例。形式化方法可以在明确定义的 规则的指导下，分析规范或或对形式规范进行变换。利用形式规范的可操纵性可 以证明规范的致性；可以推导出关于此规范的一些重要结果，还可以验证规范 的实现过程，至少可以验证源代码相对于其规范的正确性。更一般地说，有可能 将不同级别规范间的验证以及规范与程序间的验证问题简化为形式证明问题。这 样，形式化方法就可以提供描述对应其规范的非常高的可信度。所以，可操纵性 也有助于确认，并且由这种特性可以得到进一步的抽象( 推导出的性质) ，同样， 也有助于使得规范更清晰。形式化方法在早期需求分析中的应用对于改进软件质 量可以起到非常重要的作用。 1 2 本文研究工作 本论文正是针对当前软件工程中早期需求研究的逐渐成为需求工程领域研 究的一个新热点，用一个网上教学分析的案例作为研究切入点，主要完成了一下 这些工作： ( 1 ) 以教学系统为设计框架，用逐步细化的方法从识别软件的主体角色开 始，对教学系统进了面向目标的早期需求建模。 ( 2 ) 归纳总结了从i 图形化模型到形式化语言的转换，实现了将i 模型的 x m l 脚本语言翻译成g r l 描述语言的工具，并用例子说明了形式化语言的建模 方法。 ( 3 ) 采用n u s m v 模型检验工具对所建立的教学系统模型进行验证，实现早 期需求模型的验证方法。 2 本论文顺利完成了面向目标的软件早期工程的建模、形式化表示和模型检 查，从而为将来进一步向面向a g e n t 模型的建立、形式化方法的探究奠定了理论 与实践基础。 1 3 文章组织 第一章绪论介绍了本文的研究背景、技术概念关联性和本文的研究重点。 第二章基本理论和相关技术介绍了软件早期需求分析技术的基本理论， 然后介绍了为什么要研究软件的早期需求分析。随之引入并介绍了i 图形化表示 方法，章节最后还介绍了模型检查的概念及所用到的工具。 第三章网上教学系统的图示化建模通过对当前流行的网上教学系统构架 进行分析，建立了能突出反映网上教学系统的简化模型，并用案例说明了面向目 标的软件早期需求模型的逐步建立过程。 第四章介绍了模型的形式化表示使用我们所开发的工具根据i 的图形化 表示输出脚本自动生成了模型的形式化语言描述。 第五章模型的检查转化和验证介绍了将早期需求关系模型的形式化语言 向n u s m v 可接受语言的转换过程。然后用模型检查工具n u s m v 验证了我们的 模型，并且根据验证工具产生的结果报告对模型进行修改和完善。 第六章总结和展望总结本文内容，指出存在的不足和有待解决的问题， 展望了未来的发展趋势。 第二章基本理论与相关技术 本章主要介绍本文研究的理论基础与相关技术，首先简要地介绍了需求工程 的概念，接着介绍了需求分析中的早期需求分析以及一图形化建模表示，并重点 介绍了i 模型中x m l 语言格式，最后介绍了模态逻辑和模型检查的一些概念及 n u s m v 模型检查工具。 2 1 需求工程 软件需求是指用户对目标软件系统在功能、行为、性能、设计约束等方面的 期望。通过对应问题及其环境的理解与分析，为问题涉及的信息、功能及系统行 为建立模型，将用户需求精确化、完全化，最终形成需求规格说明，这一系列的 活动即构成软件开发生命周期的需求分析阶段。 需求分析是介于系统分析和软件设计阶段之间的桥梁。一方面，需求分析以 系统规格说明和项目规划作为分析活动的基本出发点，并从软件角度对它们进行 检查与调整；另一方面，需求规格说明又是软件设计、实现、测试直至维护的主 要基础。良好的分析活动有助于避免或尽早剔除早期错误，从而提高软件生产率， 降低开发成本，改进软件质量。 需求工程是随着计算机的发展而发展的，在计算机发展的初期，软件规模不 大，软件开发所关注的是代码编写，需求分析很少受到重视。后来软件开发引入 了生命周期的概念，需求分析成为其第一阶段。随着软件系统规模的扩大，需求 分析与定义在整个软件开发与维护过程中越来越重要，直接关系到软件的成功与 否。 人们逐渐认识到需求分析活动不再仅限于软件开发的最初阶段，它贯穿于系 统开发的整个生命周期。8 0 年代中期，形成了软件工程的子领域需求工程 ( r e q u i r e m e n t e n g i n e e f i n g ，r e ) 。进k 9 0 年代以柬，需求工程成为研究的热点之一。 从1 9 9 3 年起每两年举办一次需求工程国际研讨会( i s r e ) ，自1 9 9 4 年起每两年举办 一次需求工程国际会议( i c r e ) ，在1 9 9 6 年s p r i n g e r - v e f l a g 发行了一新的刊物 r e q u i r e m e n t s e n g i n e e r i n g ) ) 。一些关于需求工程的工作小组也相继成立，如欧洲 的r e n o i r ( r e q u i r e m e n t se n g i n e e r i n gn e t w o r ko f i n t e r n a t i o n a lc o o p e r a t i n g r e s e a r c h g r o u p s ) ，并开始丌展工作。需求工程是指应用已证实有效的技术、方法 进行需求分析，确定客户需求，帮助分析人员理解问题并定义目标系统的所有外 部特征的- f - 学科。它通过合适的工具和记号系统地描述待开发系统及其行为特 4 征和相关约束，形成需求文档，并对用户不断变化的需求演进给予支持。r e 可 分为系统需求工程( 如果是针对由软硬件共同组成的整个系统) 和软件需求工程 ( 如果仅是专门针对纯软件部分) 。软件需求工程是一门分析并记录软件需求的 学科，它把系统需求分解成一些主要的子系统和任务，把这些子系统或任务分配 给软件，并通过一系列重复的分析、设计、比较研究，原型开发过程把这些系统 需求转换成软件的需求描述和一些性能参数。 2 2 早期需求与i 角色标记建模和g r l 建模语言 复杂软件系统的开发，由于其对验证和有限预算的易感性，长期以来一直是 对软件工程师的重大挑战。目前也提出了一些辅助和支持高质量软件开发的技 术、方法和工具。但软件危机在许多方面依然存在。经常可以看到难以真正满足 用户需要的软件。其中主要的原因在于：缺乏对软件过程的有效定义，软件需求 没有被很好地理解或( 与用户) 达成共识，采用了不适合的技术以及复杂软件本 身所固有的难以表示的特性等等。 软件工程领域一直强调需求工程是软件开发过程中最为关键的活动。应该适 当地获得、分析、验证和管理系统需求以满足项目相关人员( 涉众) 的需要。不 完全、不一致的需求文档通常是导致软件产品质量低下，难以满足客户需要的原 因。因此，有效地开展需求工程的各项活动并尽力在软件开发的初期阶段消除需 求方面可能出现的问题非常重要。目前需求工程研究提出的方法和技术，都将目 标锁定在开发完整的、一致的需求文档方面。 所以有人认为在需求文档细化阶段必须考虑的主要问题包括：考虑软件执行 的组织环境中所有相关要素，获取功能性和非功能性需求，确保这些需求尽可能 完整是确保文档化的需求能够满足用户需要的基础。这也就是我们所说的早期需 求的分析。它旨在说明系统歼发的i ；i 提是已经建立了良好的组织过程。因此，需 要获取组织需求以定义系统如何完成组织的目标，为什么需要它，有哪些可能的 选择，在各个包含的部分中存在何种联系等等。在面向目标的需求分析方法中， 一个目标相当于系统通过软件和环境中代理的协作来获得的目的。目标在需求工 程过程中起着重要的作用，它们对需求说明提供一个完整的标准。目标有多种类 型。按层次可以分为高层目标和低层目标。高层目标是指具有策略性，粗粒度的 和组织范围上的目标：低层目标是指技术上的、细粒度的和设计上的目标。按照 涉及的类型可以分为功能目标和非功能目标。功能目标是所期望的服务，非功能 目标是指服务的质量，例如：保密性，安全性，准确性，可执行性，费用，可使 用性等，也可以指开发的质量，例如：适应性，互操作性，可重用性等。如果需 求说明满足了所有已陈述的目标，那么需求说明是完整的。目标一般比获得它们 5 的需求更加稳定，它们是需求存在的基础。在软件开发中系统所涉及的是软件以 及软件所运行的环境。目标是由系统将要获得的目的，它是对意向的一种说明性 的描述。 2 2 1p 体系中的模型元素 在需求工程中广泛地使用目标这个概念。引入目标概念，有助于完成需求工 程中的几个特定的子任务，对需求工程的面向目标的方法正受到越来越多的关 注。例如形式化的体系i ( a o s ，定性的体系i 牛这两个互补的体系已经用于需求模 型的集成和改进。而i 蛀芝术恰好可以应用予对组织需求建模的工作。i 率框架技 术适合于表达需求获取先期阶段的组织需求，它提供了适合的表达抉择，并提供 了基本的建模概念如软目标( s o f t g o a l ) 和目标。下面我们就介绍介绍i 体系中 的模型元素。在i 体系模型中主要有目标、任务、软目标和资源四种意愿元素。 他们的图形描述符号如图2 一l 。 曰 图2 - 11 + 体系中模型元素示图 在元素之间用关系来连接，意愿关系描述了模型中元素之间具有的意愿性关 系。元素连接被之间他们之间的关系连接线联系起来从而构成了完整的模型。意 愿关系包括方式一目的连接、任务分解连接、作用关系、相关关系和依赖关系等 五类关系。这些关系充分体现了他们元素之间的互相影响作用关系，细致地呈现 了他们在全局的地位和互相间作用。关系地图示描述符号如图2 2 和图2 3 。 图2 - 2 意愿关系图 6 图 干 在i 体系模型中行为者( a c t o r ) 是一个具有自身能力、知识和采取行动的策 略并能独立或相互合作来实现目标的具有主动性的实体单元。 具有意愿的行为 者是i 体系中的一个核心概念，它具有目标、理念、能力和承诺等意愿特征。 所以行为者能够包含具有目标、任务、资源、软目标这些意愿元素。同时行为者 不需要自己完成所有任务，当他自己能力不足以实现目标或周期太长、代价太大 时，他能将任务可以通过依赖关系来分派给其它行为者来实现。行为者又可以进 一步细分列举出为理( a g e n t ) ，角色( r o l e ) 和位置( p o s i t i o n ) 这四种，他们的图 示表示如图2 - 4 图2 4i 体系中的角色示例图 2 2 2i * 体系中的模型及推理机制 i 术体系主要包括策略依赖和策略推理这两个模型。策略依赖s d ( s t r a t e g i c d e p e n d e n c y ) 模型被用于描述组织环境中不同行为者之间的依赖关系。策略推理 s r ( s t r a t e g i cr a t i o n a l e ) 模型用于描述行为者的利益和事务，以及系统和环境 中的不同配置怎样来满足它们的需求。s d 模型在目的层上提供了一个行为者之 间相互关系的描述，模型人只需要知道角色的大致功能以及各角色在完成任务中 的作用而不需要知道过多行为者的内部配置。只有在s r 模型中当人们需要推理 选择的配置时，人们才需要明确这个目标和标准。甚至在这里，模型内部的目的 可以是没有被完整假定的。为了能获得他们希望的达成目的，模型仅包括那些由 行为者表达的事务。s d 模型提供了个对描述组织环境和组织环境中的信息系 统的抽象层。它显示了行为者中的包含意图等意愿元素的外部关系，并且在每个 行为者中隐藏了具有意图的模型。在帮助理解组织和系统配置时s d 模型很有用。 在i 术体系中，s r 模型通过寻找内部的行为者来模型化内部的有意图的关系从而 提供一个更详细的模型化层次。目标、任务、资源和软目标这些有意图出现在 s r 模型中的元素，不但可以作为外部的依赖，而且能作为被方式一目的关系和任 务分解关系所连接的内部元素。s r 模型提供了一个模型化行为者目的的方法， 怎样满足行为者目的，以及不同的选择方案对行为者的影响。 7 2 2 3 使用i * 体系进行软件需求分析的过程 在进行系统开发时，通常需要广泛深入地了解系统的组织环境和目标。i 木 框架提供了对构成系统需求的原因( 为什么) 的理解。该技术提供了实现策略性 角色关系的建模框架。当我们试图理解组织时，一般由标准建模技术如d f d 、e r 、 s t a t e c h a r t 获取的信息，主要关注实体、功能函数、流程、状态以及诸如此类 的信息。他们难以表达过程( 动机、意图、合理性) 产生的原因( 为什么? ) 。 i 木方法的主旨是获取这些高级的概念。因此，i 木方法允许对在组织环境中角色的 意图和动机进行描述。i 提供了两个模型：策略依赖模型和原理( 理性) 依赖模 型来表示这些涉及的方方面面的问题。i 技术可用于各种应用领域：需求工程、 商业过程再工程、组织影响分析，软件过程建模等等。 策略依赖模型主要处理组织角色间的意向性关系。策略性模型是由一个包含 节点和连线的集合构成，节点表示角色，两个节点间的连线表示角色间的依赖关 系。产生依赖的角色称为依赖者( d e p e n d e r ) ，被依赖的角色称为被依赖者 ( d e p e n d e e ) 。因此，该模型包含角色间关系的集合，这些关系用以获取角色之间 的意向和动机。i 牢框架定义了角色之间的4 种依赖关系，分别是：目标依赖、 资源依赖、任务依赖和软目标( s o f t g o a l ) 依赖。这些依赖关系分别表示组织环 境中不同的意向和动机。在目标依赖关系中，角色需要其它角色完成一个目标， 而其本身不用考虑该目标如何被完成。资源依赖关系，角色依靠其它角色提供物 理资源或信息。任务依赖关系，角色依靠其他角色实现系列的活动。角色间的软 目标依赖依靠其它角色完成模糊的目标。软目标依赖表示的依赖与其它几类不 同，它所表示的目标没有或无法进行精确的定义。在需求工程中，软目标代表非 功能需求。 在i 框架中还可以定义角色间依赖的程度：o p e n 、c o m m i t t e d 、c r i t i c a l 。 角色可提炼成主体、角色和形势。主体是一个具有具体物理表示的角色( 人或系 统) 。角色是对特定环境、领域或职责中社会角色的行为的抽象刻画。形势是由 一个主体驱动的角色的集合。 策略原理模型是策略依赖模型的补充模型。该模型可以对各个角色及他们之 间依赖产生的原因进行建模。角色从表面看来与其它角色具有某种依赖关系，实 际上，其本身包含的一定目标是产生和保持依赖关系的基础。为了实现该模型， 需要分析每个角色与其它角色产生依赖关系的原因。开始分解的好方法是观察被 依赖角色如何能够同时满足与其相关的依赖，然后从整体上分析和分解意图和策 略性组织原因。节点和连线共同构成该模型。节点在策略依赖模型中根据依赖分 类为：目标、资源、任务和软目标。连线可表示为两类连接：方法终点( m e a n s e n d s ) 和任务分解。连线可以如下描述： 方法终点：该连线获取一定的结果终点，这些终点可以是目标、资源、软目标 8 和任务。获取终点的方法被定义为需要结束的任务。 任务分解线：通过分解连接，节点任务与其子部件连接。可以连接的节点类型 有四类，对任务的分解通过这些连接类型进行。与完成任务有关的方法和原因的 表示可以通过连接分解成更小的任务单元。 2 2 4 需求分析的两个阶段 使用这个方法进行需求分析包括两个阶段： ( 1 ) 步骤1 ：获取早期需求。这个阶段的输出是两个模型。策略依赖模型( s d ) 来获取相关的行为者，它们各自的目标和它们的相互依赖。策略推理模型( s r ) 通过一个方式一目的分析来决定怎样通过其它行为者的促进来完成一个目标。 ( 2 ) 步骤2 ：在i 二中定义后期需求。这个阶段的输出是修正的策略依赖模 型( s d ) 和策略推理模型( s r ) 模型，在初始的s d 模型加入行为者来描述要开发的 软件系统。由系统行为者和方式一目的分析来产生一个新的s r 模型。如果有必要， 将系统行为者分解为几个子行为者并修正s d 和s r 模型。 2 2 5g r l 建模语言 g r l 建模语言和i + 是一一对应的，具体的语法如下所示： 严孤枷| 0 ，口吖 印扰归嘲卜哟ja c t o r m t - e l e m e m l 矗掣喇掰哕i g t o b a l - p r o p c r a e s ) a 姆勖口哼m w ，f m f 蛐叫 c r e a h o n p r a p e r a e s i i n v a r - p r o p e r a e s a 酣甘：- a c t o r m 掰8 鲥n 船苇甜】【c f 鲫咖巾嘲删l 甜j m v o r - p r o p e , l e j 】 i n t - e l e m e ，| ， o 律脚舯脚妇 d o r 加犍f 【鲫坷拉删扣e a n o u p r o p e r t w # j t 脚p r o p e l f f e $ h 惭“舢嘲 a e p e 姚, w y 卜舭d 肺烈旧骱c y 删m o d eo e p e 栅黼d 印科 d e e 删l 删删 c r e m l o u - p r o l w a * 叫【自删水嘣创 【i i | 捌幻哟伽硝 咖，d i s 哟圳t a s k ir e 嘞 m 础声m o d e 蛔糟l n _ i 越f b a h l 甜1 白忡& 啪轩i 啦! f a 的 产 n r 翻i 她 耐髓坊船声胁加l e 捌打咖“矿 戚州妇船产面搿灯船口孵：删 扫呻产【憎枷t 】【呷t i o n 】 脚“卜， 册口i 椭e 咎睇 b k 8 n l 产1 k i m 口l n 弭ii c r e a t l o n - p r o p e r u e | c r e o n a e o l - 啪一p 俅n p c r e a t l o n p r o p e , y 弘伊叩e 唧删。雷。碍e e r d c a t e g o r y t e m p o r a l - f o , m d a l n w r r o p e r t l c s ，l n 月n a 啊u w a r - p r o p e r o , + 加嘲m 甲盯驴：= p m p e r t y q v a t e g m y t e m p o r a l f o r m u l a 廊雕坤忧妒岫瞄产f u 腑i m 盯r 加弼哟孵印功一 扣拍舰卿- t p 砰竹莎删卿 钟y 髀棚押融笤n i y 细掣蹦耐和，嬲出 p r o p e r t y - c a t e g o r y ，陋m 妇n i a s l 蛐咐】 e v e n t c a t e g o r y 岍r lc o a d i f d a ld 8 断h 产g l o b a jp r o p e r t i e s ， g l o b a l p r o p e r t i e s ，g l o b a l d o o a l - p r o p e r f y + g l o b u l - p m t w r t y = p t c g , e , y c a t e g o r y e m p o r a l - f o r m u l a 9 后面的4 1 章节中将详细地对该语法进行逐个地分析，并加以案例分析。我 们将根据g r l 语法描述来建构造我们的模型并用形式化的方法来对所构造的模 型进行检验。 2 3 形式化方法和模型检查 2 3 1 形式方法的定义 形式方法是”软件危机”出现以后才在欧洲出现并广泛应用的软件开发方法。 一般而言，形式方法这个术语是指在计算机软件和硬件设计与分析过程中使用数 学技术的开发方法。关于形式方法定义可分为广义和狭义的定义。 形式方法的广义定义包括所有应用数学方法来解决软件工程中的问题，这些 应用通常包括建模和分析过程，而分析和建模的过程是由形式方法内在的数学基 础所定义的。形式方法狭义定义基本可分为两个部分，首先，形式方法包括形式 规格说明语言的使用。形式规格说明语言则是某些定义良好符号系统上字符串的 集合。在符号系统中，还应有区分这些字符串的各种规则。其二，形式方法应支 持对形式规格说明语言中公式的形式证明。 在讨论了形式方法的广义和狭义定义后，我们认为形式方法可定义为： 软件开发的形式方法是一种提供了描述软件产品，如规格说明，设计，和源 代码的形式语言，并支持对描述的产品的性质进行推理和验证的方法。一旦构造 了形式规格说明后，我们就可以对系统和软件的性质进行分析和证明，常用的技 术有定理证明技术和模型检查技术。 2 3 2 定理证明的作用 定理证明技术是形式方法的核心，定理证明是基于某个形式系统的公理推导 出系统应具有的性质的过程。一个证明任务包含下列的部分： ( 1 ) 要被证明的定理； ( 2 ) 所对应的形式规格说明，或者是描述系统性质的公式： ( 3 ) 公理和理论的集合； ( 4 ) 源逻辑。 使用定理证明技术，我们可以对系统的性质进行证明，例如可以证明系统不 会死锁或具有其它所需的安全特性。此外，定理证明还可以消除规格说明中的模 糊性和不一致性。 尽管我们可以使用纸和笔来进行定理证明，但通常的定理证明过程需要工具 的支持。定理证明器主要分为两大类：一类是半自动定理证明器，半自动定理证 i o 明工具支持的逻辑有高阶逻辑，集合论，类型理论等。证明的过程是在用户引导 下进行的，使用项重写技术、启发式搜索和策略来提高证明的效率。典型的代表 有n u p r l 、p v s 、i s a b e l l e 、h o l 、l a r c h 等。另一类是自动定理证明器，多数自 动定理证明工具是为一阶谓词逻辑而设计的，对于一阶逻辑存在着有效的推理规 则和证明过程，自动定理证明器是能自动证明一个逻辑公式的正确与否，自动定 理证明器的代表有o r r e r 、s p a s s 、s e t h e o 等。 2 3 3 模型检查的作用 模型检查是一种自动验证系统正确性的方法，它已经被成功地应用到许多实 际问题中，包括硬件设计，协议分析，交互式系统分析等问题。模型检查器的输 入通常是一个系统的有限状态模型以及一组用时态逻辑表达的系统预期属性。 模型检查器能有效地搜索有限状态模型所有的可能事件序列来判定系统性 质是否得到满足。由于系统的模型是有限的，因此系统状态空间的搜索总是能终 止。假如系统的性质有效，则模型检查器输出一个肯定结果。如果性质不满足， 则系统输出一个以状态序列形式表示的反例。 模型检查器的好处在于模型检查的过程是全自动的，与定理证明技术相比， 用户无需掌握很复杂的数学技术。检查器输出的反例信息可以用于产生测试信息 或是用于其它分析用途。模型检查器的不足之处在于它只有在用户能非常具体描 述系统的情况下才能很好地工作。因为模型检查器需要知道整个系统空间，才能 进行搜索。模型检查的主要缺点是状态爆炸问题，因为随着系统复杂程度的增加， 系统的状态数量将成指数级地增长，甚至一个简单的系统也会产生上百万个空 间。为了减少有限模型的规模，必须使用抽象技术，例如减少离散变量的范围， 使用布尔判定图( b d d s ) 来表示一个逻辑公式。模型检查器只能用于分析系统 的抽象空间，而不是系统的整个的空间。尽管存在这些局限性，模型检查器已在 工业界广泛地使用，特别是在集成电路设计和密码协议等领域。著名的例子包括 应用s m v 来验证缓冲的一致性协议和用s p i n 来验证a t & t 5 e s s 电话交换系统。 目前的研究趋势是如何将模型检查技术应用到软件规格说明的验证方面。将模型 检查技术应用到软件验证规格说明方面的一个最大的障碍是软件的数据结构复 杂性会造成巨大的系统状态空间，当前最好的模型检查技术可以处理1 0 2 0 个的 状态空间。现在广泛使用的模型检查器有f d r 、s c r 、s d t 、s m v 、s p i n 等。 表2 1 总结了定理证明器和模型检查器性能之f b j 的主要区别。 表2 一l定理证明器和模型检查器特性比较表 模型检查器定理证明器 i 典型输入语言f s m ，时态逻辑 一阶或高阶逻辑 i 输出 确定或是给出反例证明的过程 l 状态空间 有限模型，最高约可到1 0 2 0没有限制 i 自动化程度完全自动半自动，通常需要用户的指导 2 4 模型检查工具n u s m v 我们的工具基于n u s m v 结构。n u s m v 是工业级模型检查器，基于符号表 现技术。符号化技术是其中一种技术开发应用于处理现实尺度应用的空间爆炸闯 题。符号化技术潜在地，而不是显式地表现建模系统地状态和转换。通常的表示 是一个称为二进制决策图有效的布尔编码。n u s m v 有二个元件。一个是输入语 言，他( 潜在地) 定义一个自动机来表现系统。另一个是一个模态逻辑语言定义将 被检查自动机器的性质。模型检查是一种证实有限状态系统的形式化方法。被分 析的系统被表现为一个有限自动机f f s m ) ，而要满足的需求则用时序逻辑表示， 例如计算树逻辑( c t l ) ，或线性时序逻辑( l t l ) 。模型检验算法是对f s m 的状态 空间进行穷举分析。 它们能证明系统是否满足需求，或当一个违反需求的f s m 行为发生时能生 产一个反例。模型检查是一种极为有效的除错技术，并且被应用于从远程通信协 议的分析、反应性控制器到硬件设计的各个应用领域。最初，模型检查是用“显 式状态”技术实现的，f s m 的单个状态被分析和存储。”显式状态”模型检查最 有名的例子是s p i n ，它在分析不协调的系统时非常有效，通常，许多应用领域 大规模地计算的资源需要分析研究真实情况( r e a l s i z e ) 设计，所谓的状态爆炸问 题可能是一个重要的限制。符号化模型检查的引入使探测极大状态空间成为可 能。在符号化模型检查中，算法操作状态的集合而不是个体状态。 命题的公式的正则形式被通过二元判定图简洁地表现和有效地构造。因为 m c m i l l a n 的基本的工作，许多有限自动机的分割和不同的探测风格的机制被开 发，增加了基于b d d 模型检查的适用性。最近引入了一种称为有界模型检查的 新的符号化模型检查方法。 有界的模型检查受益于命题的可满足性领域的巨大的发展。这个过程在当前 许多工业领域受到了极大的成功，而且成为一个新的研究方向。基于b d d 和基 于s a t 模型检查常常能解决不同的问题，并且能够看作是两种互补的方法。有 效集成基于b d d 和基于s a t 模型检查方法对扩大符号化模型检查的适用面非常 重要。 后面将描述基于b d d 和基于s a t 方法的符号化模型检查怎样成功地集成到 n u s m v 模型检查的内部。n u s m v 是一符号化模型检查工具源自对s m v 再设计 重实现而进行的扩充。最始基于b d d 模型检查由m c m i l l a n 在c m u 开发，n u s m v 工程旨在发展一个现代化的符号化模型工具，适用于技术转换工程。它结构优良、 开放灵活，并且在健壮性上接近于工业标准。n u s m v 的第一个版本，称作 n u s m v i ，基本上实现基于b d d 符号化模型检查。n u s m v 的第二版本，继承前 版本的实现风格以及所有功能，而且较大地扩展了n u s m v i 的功能，其内部结 构与n u s m v l 相比有很大改进。n u s m v 2 主要的新颖性在于集成了基于命题的 可满足性的模型检查方法。显著地集成覆盖了n u s m v l 的所有输入语言。 n u s m v 2 是当前仅有的系统允许共同使用基于b d d 和基于s a t 两种方法的模型 检查工具。 图2 5 系统体系结构图 n u s m v 的一个最重要的特色是它是一个开放系统，而且很容易地能够修改 它，对它进行用户化或扩展。这是因为n u s m v 的结构是以模块化来构造和组 织的。每个模块实现一组功能而且通过一个精确定义的接口和其它模块通信。图 2 5 展现了系统总体结构图。实现r e d u c t i o n 方法模块设计为的是直接对b d d 表 示进行操作，这样独立地实现它们的功能性。它提供后端和前端之间的一个明确 区别。正因为这个明确的区别所以n u s m v 是开放的，而且在不同的场合中都 有着可用性，只需简单地替换或移动某种输入模块。结构包含许多的模块，它们 罨 四圈詈 口四田团 的功能性描述如下： ( 1 )