（计算机应用技术专业论文）基于场景和属性的需求引出及形式化建模.pdf

“ i i 基于场景和属性的需求引出及形式化建模 摘要 场景是一种分析与验证需求的有效工具，因此基于场景的分析与设计受到广 泛关注。场景提供预期系统的行为实例，也就是说场景中的交互行为一定是预期 系统要出现的行为。一个场景一般情况下不能完整的描述整个系统的行为，所以 基于单个场景构建的行为模型只是最终预期系统的一个下界。属性是描述系统行 为必须要满足的一种状态说明，基于属性的构造的行为模型包含所有不违反属性 的可能轨迹。因此基于属性的行为建模为预期系统提供了一个上界。如何基于场 景构造预期系统的下界和基于属性构造预期系统的上界，以及在上界行为模型和 下晃行为模型之间得到最终的预期系统便是本文的研究重点。 本文首要解决是如何进行基于场景和属性的需求引出。消息序列图( m e s s a g e s e q u e n c ec h a r t s ，m s c ) ，一种场景的表示方法，用于描述场景中构件之间的通 信、交互行为，因此本文首先介绍m s c 的基本概念。3 一值流体线性时序逻辑公 式是一种描述系统属性的有效方法，因此在介绍3 一值克莱尼逻辑( k l e e n el o g i c ) 和流体之后，文中给出了3 一值流体线性时序逻辑公式的概念。然后通过一个论 坛发帖系统的实例，根据场景的描述将需求引出，生成m s c 图，然后又将需求形 式化为属性描述。 基于场景合成的标号迁移系统只能描述场景给出的行为，不能描述场景没有 给出的可能行为。基于属性合成的标号迁移系统不能区分哪些是为了满足安全属 性必须发生的行为和不违反安全属性的可能发生的行为。针对现有合成算法存在 的问题，并在现有合成算法的基础上，我们给出了合成模态迁移系统的算法。在 现有基于场景合成l t s 算法的基础上，提出一个算法使得l t s 变成m t s ，得到 一个预期系统必然行为的下界，同时合成的m t s 模型可以表达除场景描述之外 的可能行为。在基于属性合成l t s 算法的基础上，提出了合成m t s 的算法，得 到预期系统的一个上界，合成的m t s 模型可以区分必然行为和可能行为。最后 通过合并操作将这两个m t s 模型合并为一个m t s ，该模型保留下界的必然行为 和上界的可能行为。合并之后，系统行为可以进一步精化，模态迁移系统的精化 不仅保留了初期的属性和场景，而且支持新的属性和场景的抽取。 关键字：场景；标号迁移系统；模态迁移系统；合成 i l i j r e q u i r e m e n t se l i c i t a t i o na n df o r m a l i z a t i o n m o d e l i n gb a s e do ns c e n a r i o sa n dp r o p e r t i e s a b s t r a c t t h es c e n a r i o sa r ew i d e l yr e c o g n i z e da sa ne f f e c t i v ew a y sf o rr e q u i r e m e n t s e l i c i t a t i o n ，d o c u m e n t a t i o na n dc e r t i f i c a t i o n t h es c e n a r i o sp r o v i d ee x a m p l e so ft h e i n t e n d e ds y s t e mb e h a v i o u r , i e ，s e q u e n c e so fi n t e r a c t i o n st h a tt h es y s t e mi se x p e c t e d t oe x h i b i t as c e n a r i od o e sn o td e s c r i b eu n i v e r s a l r e q u i r e m e n tf o ra l ls y s t e m b e h a v i o u r sc o m p l e t e l y , s ot h eb e h a v i o u rm o d e lb a s e do i lt h es i n g l es c e n a r i oo n l y p r o v i d e s al o w e rb o u n do ft h ei n t e n d e ds y s t e m p r o p e r t i e sa r es t a t e m e n t sw h i c h c h a r a c t e r i z et h eb e h a v i o u r st h a tm u s t b es a t i s f i e d ，t h eb e h a v i o u rm o d e l 舶m p r o p e r t i e sc o n t a i n st h ep o s s i b l et r a c e sw h i c hd on o tv i o l a t ep r o p e r t i e s t h u s ，t h e b e h a v i o u rm o d e l i n gp r o v i d e sau p p e rb o u n df o rt h ei n t e n d e ds y s t e m t h er e s e a r c h e m p h a s i so ft h et h e s i si sh o wt oc o n s t r u c tt h el o w e rb o u n do ft h ei n t e n d e ds y s t e m b a s e d o ns c e n a r i o s ，h o wt oc o n s t r u c tt h eu p p e rb o u n do ft h ei n t e n d e ds y s t e m b a s e d - o np r o p e r t i e s ，a n dh o wt og e tm ef i n a li n t e n d e ds y s t e mb e t w e e nt h el o w e r b e h a v i o u rm o d e la n dt h eu p p e rb e h a v i o u rm o d e l t h ef i r s ts o l u t i o ni sh o wt od ot h er e q u i r e m e n te l i c i t a t i o nb a s e d o nt h es c e n a r i o s a n d p r o p e r t i e s m s c ，ar e p r e s e n t a t i o no fs c e n a r i o s ，i su s e dt od e s c r i b et h e c o m m u n i c a t i o n ，i n t e r a c t i o nb e t w e e nt h ec o m p o n e n t si nt h es c e n a r i o s ，t h u s ，t h et h e s i s f i r s ti n t r o d u c e st h em a i nc o n c e p to fm s c 3 - f l t li sa ne f f e c t i v ew a yt od e s c r i b et h e s y s t e mp r o p e r t i e s ，s o ，a f t e ri n t r o d u c i n gt h e3 - v a l u ek l e e nl o g i ca n df l u e n t , 3 - f l t li s i n t r o d u c e d t h e n ，b yt h ee x a m p l e so ft h ef o r u mp o s t ，t h er e q u i r e m e n ti se l i c i t e db a s e d o nt h ed e s c r i p t i o no f s c e n a r i o s ，g e n e r a t e st h em s c ，f o r m a l i z e st h er e q u i r e m e n ta st h e p r o p e r t i e sd e s c r i p t i o n l t ss y n t h e s i sb a s e do nt h es c e n a r i o so n l yd e s c r i b et h eb e h a v i o u r sp r o v i d e db y s c e n a r i o s ，a n dd on o td e s c r i b et h ep o s s i b l eb e h a v i o u r sw h i c hi sn o tp r o v i d e db y i i i s c e n a r i o s l t ss y n t h e s i sb a s e do nt h ep r o p e r t i e sb l u r st h ed i s t i n c t i o nb e t w e e nt h e b e h a v i o u r st h a tm a yo c c u ra st h e yw i l ln o tv i o l a t ep r o p e r t i e sa n dt h eb e h a v i o u r st h a t m u s to c c u ri no r d e rt oa v o i dav i o l a t i o no fp r o p e r t i e s w i t hr e g a r dt ot h e e x i s t e d s y n t h e s i sa l g o r i t h m ，w ep r e s e n tt h em t ss y n t h e s i sa l g o r i t h mo nt h eb a s eo ft h e e x i s t e ds y n t h e s i sa l g o r i t h m w ep r e s e n taa l g o r i t h mt ot u r nl t si n t om t s o nt h eb a s e o fe x i s t e dl t ss y n t h e s i sa l g o r i t h ms c e n a r i o s b a s e d ，a n d g e tal o w e rb o u n do f r e q u i s i t eb e h a v i o u r s o ft h e i n t e n d e d s y s t e m t h es y n t h e s i sm t sm o d e lc a l l d i s t i n g u i s ht h er e q u i s i t eb e h a v i o u r sa n dp o s s i b l eb e h a v i o u r s t h e nw em e r g et h et w o m t s st oo n em t sb yt h e m e r g i n go p e r a t o r , t h em o d e lp r e s e r v e st h er e q u i s i t e b e h a v i o u r so ft h el o w e rb o u n da n dt h ep o s s i b l eb e h a v o u r so ft h eu p p e rb o u n d a f t e r m e r g i n g ，t h es y s t e mb e h a v o u rc a nf u r t h e rr e f i n e ，t h em t sr e f i n e m e n tc a nn o t p r e s e r v et h ei n i t i a lp r o p e r t i e sa n ds c e n a r i o s ，b u ts u p p o r tt h ee l i c i t a t i o no ft h en e w s c e n a r i o sa n dp r o p e r t i e s k e y w o r d s ：s c e n a r i o s ；l a b e lt r a n s i t i o ns y s t e m ；m o d a lt r a n s i t i o ns y s t e m ； m e r g e i v 目录 摘要i a b s t l i a i ：? r i i i 目录v 第l 章绪论l 1 1 研究背景1 1 1 1 需求工程的过程和定义l 1 1 2 基于场景的需求工程3 1 2 国内外研究现状4 1 2 1 基于场景的需求工程的研究现状：4 ” 1 2 2 形式化方法的研究现状4 1 3 研究内容6 1 4 论文结构7 第2 章基于场景和属性的需求引出i 8 2 1 引言8 2 1 1 场景的基本概念8 2 2 用于场景描述的m s c 介绍8 2 2 1m s c 的基本概念8 2 2 2m s c 的主要元素9 2 3 基于场景和属性的需求引出9 2 3 13 一值流体线性时序逻辑( 3 - v m u ef l l 兄) 9 2 3 2 场景和属性的需求引出描述1 1 2 4 本章小结1 3 第3 章行为建模技术研究1 4 3 1 研究背景1 4 3 1 1 标号迁移系统的概念( l t s ) 1 4 3 1 2 模态迁移系统的概念( m t s ) 1 4 v 3 1 3f l t l 在迁移系统中的模拟和实现1 8 3 2 现有模型存在的问题2 1 3 3 基于属性的合成2 3 3 3 1 基于属性的标号迁移系统的合成2 3 3 3 2 基于属性的模态迁移系统的合成2 5 3 4 基于场景的合成2 9 3 4 1 基于场景的标号迁移系统的合成2 9 3 4 2 基于场景的模态迁移系统的合成3 0 3 5 基于属性和场景的合成3 2 3 5 1 基于场景和属性的模态迁移系统的合成3 2 3 6 本章小结3 6 ， 第4 章结束语j 3 7 4 1 主要工作j 3 7 4 2 未来工作i 3 7 参考文献3 9 致谢4 3 攻读学位期间取得的研究成果：4 4 浙江师范大学学位论文独创性声明4 5 学位论文使用授权声明4 5 v i 1 1 研究背景 第1 章绪论 1 1 1 需求工程的过程和定义 需求工程( r e q u i r e m e n t se n g i n e e r i n g ，r e ) 是随着计算机科学的发展而发展起 来的d 1 ，在计算机发展的初期，软件规模不大，软件开发所关注的是代码编写， 需求分析很少受到重视。后来软件开发引入了生命周期口1 的概念，需求分析成为 其第一阶段。随着软件系统规模的扩大和“软件危机 带来的软件工程的发展， 需求分析与定义在整个软件开发与维护过程中越来越重要，人们普遍认识到，进 行需求分析和定义可以避免系统开发时的盲目性。随着软件工程的研究和应用的 逐渐深入，人们同时认识到需求分析活动不再仅限于软件开发的最初阶段，它贯 穿于系统开发的整个生命周期乜1 。 8 0 年代中期，形成了软件工程的子领域一需求工程。进入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 r l a g 发行了一个新的刊物( r e q u i r e m e n t se 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 g n e t w o r ko ri n t e r n a t i o n a lc o o p e r a t i n gr e s e a r c hg r o u p s ) ，并开始开展工作。 需求工程的目标是深入描述软件的功能和性能，确定软件设计的限制和软件 同其它系统元素之间的接口细节，定义软件的其他有效性需求。需求分析的任务、 就是借助于当前系统的逻辑模型导出目标系统的逻辑模型，解决目标系统的“做 什么 的问题。需求活动以“工程化”的方法被提出、分析和组织，它鼓励用户 以一种积极的方式参与需求分析活动中，并在整个软件生命周期中强调用户参与 和领域专家的指导作用，促使目标系统最大地满足用户需求。 需求工程是系统工程和软件工程的交叉学科。之所以把需求作为“工程”来 第l 章绪论 研究，其目的是强调它是一个系统的、协同的和反复的过程，是一个由客户、用 户、系统设计、开发、实现和测试人员等众多风险承担人参与的复杂活动，涉及 社会、人们的认知、表达方式以及企业文化等众多领域的问题d 1 。目前“需求工 程 还没有标准的定义，一般认为需求工程是指应用己证实有效的原理、技术和 方法，描述目标系统的外部特征和相关约束，从而确定客户需求，帮助分析人员 理解目标系统的一门学科。 需求就是以一种清晰、简明、一致且无二义性的方式对一个待开发系统中 的各个方面有意义的陈述的集合。需求必须包含足够多的信息，足以使设计师和 工程师来产生一个使客户满意的产品。 软件需求包括三个不同的层次伽：业务需求、用户需求和功能需求( 也包括 非功能需求) 。业务需求( b u s i n e s sr e q u i r e m e n t ) 反映了组织机构或客户对系统、产 品高层次的目标要求，它们在项目视图与范围文档中予以说明。用户需求( u s e r r e q u i r e m e n t ) 文档描述了用户使用产品必须要完成的任务，这在使用实例口1 ( u s e c a s e ) 文档或场景嘲( s c e n a r i o ) 说明中予以说明。功能需求( f u n c t i o n a lr e q u i r e m e n t ) 定义了开发人员必须实现的软件功能，使得用户能完成他们的任务，从而满足了 业务需求。 值得注意的一点是，需求并未包括设计细节、实现细节、项目计划信息或测 试信息。需求与这些没有关系，它关注的是充分说明你究竟想开发什么。f r e d e r i c k b r o o k s 在他1 9 8 7 年的经典文章n 0s i l v e rb u l l e t ：e s s e n c ea n da c c i d e n t so f s o f t w a r ee n g i n e e r i n g ) ) 中充分说明了需求过程在软件项目中扮演的重要角色：“开 发软件系统最为困难的部分就是准确说明开发什么。最为困难的概念性工作便是 编写出详细技术需求，这包括所有面向用户、面向机器和其它软件系统的接口。 同时这也是一旦做错，将最终会给系统带来极大损害的部分，并且以后再对它进 行修改也极为困难。口1 可以说需求工程的核心就是获得关于目标系统稳定、准 确的描述，因此需求工程的最终产品是一组系统需求文档，其中最主要的文档是 项目管理文档和需求规格说明。这些文档是对需求“固化 的结果，是对系统的 功能性需求和非功能性需求的陈述嘲。系统需求文档是后继系统设计、实现和测 试的依据j 它必须完整嘲、一致n 们、没有二义性n 1 1 ，而且在系统开发、运行和维 护的过程中，还必须能够对其进行修改、跟踪、验证和使用n 幻。为了达到这个目 2 第1 章绪论 标，目前趋向于引入形式化方法进行一致性检查、类型检查、有效性验证、行为 预测以及设计求精验证。 1 1 2 基于场景的需求工程 需求工程领域中，基于场景的需求建模方法嘲正吸引越来越多人们的兴趣。 较之自然语言，场景可以更为精确地刻画系统行为。相比形式化描述技术，场景 概念则更为直觉，这种折衷的特性正是场景概念受到广泛重视的原因所在。系统 开发初期用户难以用某种抽象的方式来表述他们的需要，如果让用户试验一个假 想的系统，看用户是否满意，从而发现真正的需求，那么将有助于需求的正确获 取。实践证明：场景概念符合人类从具体到抽象的认识事物的过程及认知科学的 研究结论1 3 1 。 在需求工程、软件工程、人机交互等领域内基于场景的方法越来越受到重视。 这主要源于场景概念具有如下优点： ( 1 ) 场景特别适合于描述软件系统的行为和功能需求。 ( 2 ) 场景具有很强的直观性。因此用户、，系统分析员和设计员都能理解，这 极大地方便了系统开发者和用户之间的交流。 ( 3 ) 场景易与快速原型法结合获取用户需求。 ( 4 ) 场景可以引入到渐增式的设计过程中。 ( 5 ) 场景概念便于对系统结构进行抽象。 ( 6 ) 场景可以驱动设计过程、构建详细设计模型和实现模型。 ( 7 ) 场景便于文档编写和通信。 ( 8 ) 场景能指导测试实例生成并对不同抽象层次( 如说明，设计和实现) 加以 确认。场景便于指导构造更详细的模型直到实现。但凡事都有两面性，场景也不 例外。 场景的主要缺点有： ( 1 ) 因为场景是系统行为的部分表示，所以在一系列场景中保持完整性、一 致性是非常困难的n 们。 ( 2 ) 场景不适合于描述非功能需求。 3 第l 章绪论 ( 3 ) 由一系列场景合成出系统整体行为是一个非常困难的问题n 副。 ( 4 ) 在开发实践中，获取粒度合适的场景并加以维护比较困难n 硝。 ( 5 ) 当前基于场景的设计方法都尚不成熟，有待进一步的研究。 1 2 国内外研究现状 1 2 1 基于场景的需求工程的研究现状 目前，国外很多学者在面向场景的需求工程中做了很多工作。 在面向场景的需求分析方法中，a s u t e l i f f e 描述了整个面向场景的需求工程 方法，提供了面向场景的需求工程流程嘲；p h e y m a n s 在场景的细化和形式化验 证上m ，做了很多工作；s u c h i t e l 为场景的语法和语义建立了严密的形式化描述 n 町；r a l u r 、k e t e s s a m i 等在场景的描述上d 明、o h a u g e n 等在场景和u m l 的转 换工作上洲、m e l k o u t b i 等在场景的自动化描述上乜、s s o m e 等在从场景描述 到自动机的转化工作上吻1 、s v g h e o r g h i t a 等在场景侦测的自动化上汹1 、 s e r o b e r t s o n 等在从场景描述面向对象的设计描述上翻1 、j m c a n o l l 等在基手场 景的设计过程上嘶1 、j k a r a t 在场景的实践上s f i e k a s 等在使用场景描述需求上 渊、r o g a w a 等在基于场景的设计策略上1 、- l b a s s 等在从场景到体系结构上 嘲、t a a l s p a u g h 在场景的整合上嘲、r l h o b b s 在场景指导的框架设计上制等 等，都做出了很大的贡献。 1 2 2 形式化方法的研究现状 根据软件产品在不同业务领域具有的不同应用特点，研究人员提出了多种形 式化建模的方法。本节主要介绍线性时序逻辑( l i n e a rt e m p o r a ll o g i e ，l t l ) 、有 限自动机( f i n i t es t a t e a u t o m a t a ) 、状态图( s t a t e c h a r t s ) 、h 演算，至于其它形式 化建模方法，在这里就不再一一介绍了，有兴趣的读者可以查阅相关文献。 1 2 2 1 线性时序逻辑 4 第1 章绪论 线性时序逻辑( l i n e a rt e m p o r a ll o g i c ，l t l ) 线性时序逻辑是在命题逻辑的 基础上加上时序操作而得来的。基于线性时序逻辑的分析方法是一种重要的描述 和验证软件体系结构特性的形式化分析方法。它由m a n n a 和p n u e l i 首次开发出 来用以描述系统的并发特性跚1 。它以路径( 状态序列) 作为命题的论断对象，在状 态序列上解释其真值。线性时序逻辑可以方便准确地描述并发系统的重要性质， 如安全性( s a f e t y ) 和活性( l i v e n e s s ) 。安全性用于说明“坏事情永远都不会发生”； 活性用于说明“好事情最终会发生 。线性时序逻辑( l t l ) 作为一种系统规范描 述语言，有一些十分显著且不可替代的特征：直观、具有良好的兼容性。l t l ( l i n e a rt e m p o r a ll o g i c )与自动机之间有着紧密的联系，结合l t l 语义和语法， 可以将l t l 公式转换成b f i c h i 自动机。由l t l 生成的b i i c h i 自动机所接受的语言 能准确地表达了l t l 公式所描述的系统属性。从而，我们可以把对l t l 公式描述 的系统属性的验证问题转换成检验b i i c h i 自动机的包含问题。 1 2 2 2 有限自动机( f i n i t es t a t e a u t o m a t a ) 有限状态自动机( f i n i t es t a t e a u t o m a t a ) 是一种用于研究系统状态的数学模 型，简称自动机，最早出现于2 0 世纪4 0 年代，后来莫尔( m o o r e ) 在1 9 5 6 年 利用它建立了描述计算机的时序概念，f s a 是应用最为广泛的一种自动机。有限 自动机的优点在于状态与状态之间的关系比较清晰，容易使用。但也存在很多缺 点，比如它在系统的任何时刻都只能表示一种状态，即在任何时刻最多执行一个 操作，如此一来，有限状态自动机就不利于描述并发、复杂系统，而只能够描述 顺序系统问题。 有限自动机也是有限计算的基本模型，是许多形式化规格、验证方法的基础 模型，它常用于行为建模中。最为突出的特点就是f s a 非常适合描述包含有限个 状态，并且事件的发生将导致状态迁移的这类系统。 有限自动机可以用一个5 元组m = ( q ，6 ，q ，f ) 来表示，其中q = q 0 ，q l q n 是有限状态集合。在任一确定的时刻，有限状态自动机只能处于一个确定的状态 q i ；是字母表，6 ：q x _ q 是状态转移函数，q 0 是初始状态，有限状态自 动机由此状态开始接受输入。f 是识别可接受状态的q 的子集，即终结状态集合， 5 第l 章绪论 有限状态自动机在达到终态后不再接收输入。如果任何q 在q 内且任何e 在， ( q ，e ) 至多有一个成员，那么自动机就被认为是确定性的。 1 2 2 3 状态图( s t a t e c h a r t s ) 状态图( s t a t e c h a r t s ) 是由以色列的d a v i dh a r e l 建立的传统有限状态自动机 的一种扩展形式。状态图中通过引入状态的递阶、状态的与分解和或分解等高级 特性，使得问题规格的状态图的状态数目极大减少，从而也具备了更强的描述能 力n 3 1 。状态图也可以描述成对离散事件系统进行行为建模的图形化语言，由于使 用图形来表示系统的行为活动，所以与其他方法相比，它更易理解，并且具有很 好的交互性。 1 2 2 4 n 演算 n 演算是r o b i nm i l n e r 等人在c c s ( c a l c u l u so fc o m m t m i c a t i n gs y s t e m s ) 的 基础上提出的传名演算，n 演算包含两种类型的实体，其中一个是进程，另一个 为信道。名字是演算中最基本的实体，像端口、信道和链路都是名字。而信 道名字作为进程事件的符号元素出现。另外，n 演算还具有很好的描述能力，有 利于刻画出具有动态结构的单进程内部及多进程之间的交互过程。 1 3 研究内容 场景提供预期系统的行为实例，场景中的行为是预期系统一定要出现的行 为。一个场景一般情况下不能完整的描述整个系统的行为，所以基于单一场景构 建的行为模型只是最终预期系统的一个下界。现有的基于场景合成的标号迁移系 统只能描述场景给出的行为，不能描述场景没有给出但有可能发生行为。属性是 描述系统行为必须要满足的性质，基于属性构造的行为模型包含所有不违反属性 的轨迹。因此基于属性的行为建模为预期系统提供了一个上界。现有的基于属性 合成的标号迁移系统不能区分哪些是为了满足安全属性必须发生的行为和不违 反安全属性的可能发生的行为。 6 第l 章绪论 模态迁移系统可以区分必然行为和可能行为。因此本文主要是研究如何构建 场景的模态迁移系统来表示预期系统的下界，以及如何根据系统的属性合成模态 迁移来描述预期系统的上界。最后把从场景中合成的模态迁移系统和基于属性合 成的模态迁移系统进行合并，即求得最小共同精化，并根据合并后的模态迁移系 统的轨迹抽取出新的属性，对模态迁移系统进行进一步的精化。因此本文主要做 了以下工作： 1 ) 构建了用流体线性时序逻辑表达的安全属性模态迁移系统； 2 )在现有的基于场景合成标号迁移系统基础上，提出一个算法，支持 基于场景的模态迁移系统的合成。 3 )将基于属性合成的模态迁移系统和基于场景合成的模态迁移系统合 并，并进行进一步的精化。 1 4 论文结构 第1 章介绍了本篇的研究背景、国内外研究现状、本篇研究内容及论文结 构。 第2 章我们首先介绍了场景的概念和场景描述的m s c 和用于描述属性的 3 。值流体线性时序逻辑，进行需求引出。 第3 章，首先回顾了迁移系统以及f l t l 在迁移系统中的模拟和实现等有关 的概念与定理。在分析了现有合成方法的局限性的基础上，分别研究基于场景和 属性合成模态迁移系统的算法，最后通过合并得到最终系统模型。 第4 章对本文的工作进行了总结，并进一步介绍了未来还需要做的工作。 7 2 1 引言 第2 章基于场景和属性的需求引出 2 1 1 场景的基本概念 场景是一系列系统行为之间的交互，是对用户与系统交互的部分描述。而系 统在本篇里是指预期的应用软件及其周围的环境。系统是由控制系统行为的动态 组件构成，一些组件来自于环境，而另一些则来自于预期软件。场景也可以用来 描述可能发生的一系列事件。场景的交互来源于一些事件，通过事件触发场景间 的通信，这些事件是同步地从源组件发送到宿组件。一个场景的历史片断是一个 为达到某些目标( 包括一些暗含的) 的交互子序列。一个场景也可以由下面给出的 元素来描述： 主题：用于标识场景，区别场景。 目标：建立场景的目标。一个场景应该是描述为完成目标的交互过程。 语境( 上下文) ：确定场景的初始状态，它的前提条件，环境边界及后续影 响。 资源：确定参与者所能处理的被动对象。 参与者：是在场景里扮演角色的人或组织结构。 情节：每一个情节都表示一个参与者执行的一个动作，也可以包括其它参与 者及使用可得到的资源。 2 2 用于场景描述的m s c 介绍 2 2 1m s c 的基本概念 消息序列图可以定义为一种图形语言，其用于描述说明系统组件之间的通 8 第2 章基于场景和属性的需求引出 信、交互行为，是各种应用软件开发实践中使用较为广泛的一种场景表示方法。 因此很容易为最终用户、需求分析人员和系统设计人员所接受。消息序列图可以 有效地描述系统组件之间以及组件与系统环境之间的交互、通信。然而，其中的 每一个消息序列图又刻画了系统的部分、片段的行为活动。 一个简单的m s c 语言用于表现最终用户场景。一个消息序列图由代表时 间线的垂直线( 与a g e n t 实例关联) 与代表不同a g e n t 实例之间交互的水平箭头组 成n 刀。个时间线标记指明相应a g e n t 实例的类型。一个箭头标记指明一些定义 相关交互的事件。每个箭头标记单独决定源和宿a g e n t 实例。这些a g e n t 实例控 制、监视交互事件。事件被源a g e n t 同步控制，被宿a g e n t 监视。在消息序列图 中，用矩形框来表示实例。 2 2 2m s c 的主要元素 m s c 主要组成元素： 实例：作为m s c 基本的概念，构成了系统内在要素。实例可以是外部参与 者、软件构件或机械物理部件等。 消息：消息描述了实体间的相互影响方式。消息用带箭头水平直线从源实例 指向目的实例来表示。 。 外部环境：环境组成了消息序列图的外部边界。 2 3 基于场景和属性的需求引出 本节将举例说明在需求分析的初始阶段从场景引出需求的一般步骤。首先介 绍了流体和时序逻辑的概念，接着定义了3 一值流体线性时序逻辑，最后通过m s c 和属性将需求引出。 2 3 13 值流体线性时序逻辑( 3 - v a l u ef l t l ) 9 第2 章基于场景和属性的需求引出 本文，我们假设属性说明用流体线性时序逻辑( f l t l ) 描述。线性时序逻 辑被广泛用于描述行为需求。选择f l t l 的目的是因为在基于事件的模型中，在 模型检测基于状态的时序属性时，f l t l 可以提供一个标准的框架。 2 3 1 1 流体的概念 定义2 1 流体。一个流体只是由一对初始事件集，凡和终止事件集砀定义， 形式化定义如下：f l u e n tf i = i f l , t f i c - - a c t如n 聊 一个流体可能由初始的用属性来指定初始为真还是假，缺省这个流体初始 值为假。初始和终止事件集必须不相交。 每个行为a a c t 产生一个流体，即a 意味着 例如图2 3 中描述 的论坛发帖系统属性p 3 它使用来源于同样名字的行为和以上定义的流体q u i t 和 q u i t m s g m i l l e r 和s h a n a h a n 定义流体为“随时变化的世界属性，如果它们被较早发 生的事件初始化，且期间未被其它事件终止的话，其在特定时间点为真。类似， 如果它们较早被终止且期间没有初始化的话，其在特定时间点为假”嘞。 2 3 1 23 一值逻辑 真值t ( 真) ，f ( 假) ，和上( 可能的，未知的) 组成了3 中我们所称作的克莱尼 逻辑，这些真值有2 个序关系，e ( 真) ，其满足f _ _ l e t ，和妄n f ，其满足1 _ i ：= i n f t 和- = i n f f ( 即上提供的信息是最少的) ，两个规则都是幂等的。对于这个真值t 、 f 、上与v 。a 和一有以下关系： 上a t = 上上a f = f上v t - - t 上v f = - 上 一上= 上 2 3 1 3 l i 。l 假设流体集，一个f l t l 公式使用标准布尔连接符和时序操作符x ( 下一 个) ，u ( s t r o n gu n t i l ) ，w ( w e a ku n t i l ) ，o ( 终于) ，口( 总是) 表示， 定义2 2 时序操作符的定义如下： i d x = x 从现在开始为真： 0 x = x 永远为真； x u y = x 直到y 为真x 才为真； l o 第2 章基于场景和属性的需求引出 x w y = x 是弱的直到y 为真( i sw e a ku n t i lyi st r u e ) ，x 才为真。 定义2 3f l t l 公式归纳定义如下： 妒：2 用i1 9l 伊v | | f ，l 伊 j | f ，ix 尹i9 u yl 伊w l f ，l 伊i 9 f i e o 兀 = f i垒7 t 0 i = f i 兀# - v p 叁 一( 兀印) 兀# 伊v f ， 兀# 伊 杪 冗# x 缈 ( 7 c # 伊) v ( 兀仁杪) ( 兀印) a ( 兀仁妙) ， ， 兀lp9 兀 = c u p 叁 了f 0 一乍l f ，人v 0 _ ， 9 冗仁伊w f ， 叁 兀仁( 矽udv 口矽 7 c = 9 叁冗# tu 妒 兀扛口9 叁 兀仁一伊 图2 1 满意操作符语义 2 3 2 场景和属性的需求引出描述 首先，介绍一下本节中要用到的例子。假设需要建模一个简单的网上论坛系 统，用于网上发帖，其中包括用户、论坛服务器和管理员三个组成部分。用户为 了发送帖子，向论坛服务器请求验证，验证之后用户向论坛服务器发送帖子，接 着论坛服务器向用户返回一个发送成功的确认，用户退出时，收到一个退出确认 消息，管理员还可以在用户活动期间将用户排除系统。根据以上场景描述，做出 如2 2 所示m s c 图，提供了一些预期的系统行为，用一个标准的消息序列图引 出需求。r e p 盒子表示里面的行为是不断重复的，场景s c 描述了在两个行为序列 之间的重复交互：( 1 ) 首先用户向论坛服务器请求验证，验证之后向论坛服务 器发送帖子，接着论坛服务器向用户返回一个发送消息；之后用户退出，收到一 个退出消息。( 2 ) 管理员在用户活动期间使用户禁止，有效地将用户排除系统。 论坛发帖系统场景规约要求的一个事件序列的例子是 s c l2 v a l i d a t e , p o s t , p o s t m s g , d i s a b l e q u i t m s g , 第2 章基于场景和属性的需求引出 固匡习甲 a 1 t i v a l i d a t e i !j r e p p o s t p o s t m s g q u i t q u i t m s g v a li d a t e - r r e p p o s t p o s t m s g 1 i d i s a b l e q u i t m s g e n a b l e f l 图2 2 论坛发帖系统场景规约s c r e g i s t e r e d = - i n i t i a l l yt r u e l o g g e d l n = i n i t i a l l yf a l s e ( 合法访问) p l = ( l o g g e d l n = 争r e g i s t e r e d ) ( 私有访问) 胪( p o s t - - j l o g g e d l n ) ( 退出被确认) 胪( q u i t - - - j xq u i t m s g ) ( 发帖被确认) p 4 = ( p o s t - - j x p o s t m s g ) 图2 3 论坛发帖系统属性 这个论坛发帖系统被要求实施合法和私有的访问这个论坛。这些需求在图 2 3 中用流体线性时序逻辑形式化为属性p j 和肋。属性p ，即合法的访问，要求登 录论坛时用户一定是在论坛注册过的。属性肋即私有的访问，要求当用户向论 坛服务器发送帖子时，一定是登陆的。注册和登录是可以随着事件的发生而改变 值的流体。一旦用户已经被激活，尚未被禁止，则这个用户是注册的。一旦一个 用户已经验证，尚未退出，也未被禁止。则这个用户是登陆的。属性阳说明了 退出时用户应该收到一个退出消息。刃的形式化说明了如果q u i t 发生，则下一 1 2 第2 章基于场景和属性的需求引出 个发生的事件是q u i t m s g 。属性肌说明了用户发帖时应该收到一个确认消息。p , t 的形式化说明了假如用户发帖，则下一个发生的事件是返回一个确认消息。 2 4 本章小结 在这一章中，我们首先介绍了场景的概念和场景描述的m s c ，接着又回顾 了3 一值克莱尼逻辑和流体的概念，用它们定义一个3 值流体线性时序逻辑公式 来描述属性。然后通过一个论坛发帖系统