（计算机软件与理论专业论文）基于用户场景的需求引出及其行为建模技术研究.pdf

摘要 随着软件工程学科的发展，需求工程日益得到人们的重视。需求分 析作为软件生命周期极为重要的一个环节，关系到软件工程项目的成功 与否，并且在很大程度上决定了软件产品的质量。因此，如何有效地捕 获用户的真篮需求已经成为软件工程学科研究的重点。场景被认为是引 出、文档化和验证需求的较为有效的工具，其支持非形式化、叙述性和 具体化的描述，关注用户与软件环境交互的动态特性，因而参与需求分 析过程的实践者和用户都能很容易地使用场景来表达其对需求的理解， 以达到最佳的交互状态，从而更好地获取用户需求。这样，通过让用户 真正地参与到需求分析的过程中，可以更好地将应用领域问题映射到计 算机领域，并且在需求获取的迭代过程中可以自动地适应系统需求的不 断变化，避免了由于需求变更而导致的系统体系结构的改变，同时也能 及时添加新的需求或修改已有的不符合用户实际需要的场景，有利于保 证应用软件开发的正确性及完整性。 由于在开始阶段得到的是对场景的非形式化描述，而作为工程目标 的软伴系统是由程序及其运行环境组成，二者不仅从内容到形式都存在 巨大的差翱。为此，需要在它们之间建立起映射，使得程序能够正确建 模用户的需求。传统的结构化方法将软件系统视为数据加工的过程，其 利用功能分解的办法将系统分为不同的功能模块，每个模块进行一个子 加工。虽然结构化方法曾经是软件工程实践中的主流技术，并且至今仍 具有重要的影响，但是随着现代软件系统臼趋复杂，各组件之间具有的 各种动态交互关系以及需求的不断演化，使结构化方法愈发难以胜任。 因此，如何归纳出系统的功能以及各个组件和外部参与者之间的交 互就成为工程实践的中心任务。如果能够据此合成出系统的状态模型并 生成代码框架，将有助于提高软件质量及降低成本。对于传统的分析方 法来说，需要运用非形式化的手段，发挥创造型思维来分析用户的需求。 。 在这个过程中，对于不同用户和分析人员，由于各自不同的工作领域和 思维模式，他们之间存在着交流上的障碍，造成得到的需求难以正确和 完整。如何与用户交流以得到其真正需求也成为一个重要环节。根据以 i 上构思，首先由用户提交目标系统的初始期望场景集和例外场景集；然 后生成全局系统的状态图，在此过程中不断检验出隐含的期望场景和例 外场景，并辅助状态图的合成，最终完成从用户提交的场景描述到利用 二 。 形式化方法建立需求模型的过程。在这个过程中介绍了目前流行的形式 化建模方法的基本概念，并着重描述了本篇实例中所用到自动机理论及 相关技术。 为了研究从场景需求规约得到系统功能规约的步骤，本篇将通过建 模一个手机短信服务系统来阐述基于m s c ( m e s s a g es e q u e n c ec h a r t ) 一场 景的需求引出过程。为了得到形式化的功能规约，需耍由用户输入的场 景合成出前缀树识别器( p r e f i xt r e ea c c e p t o r ) ，即根据对场景的描述 画出m s c ，遍历m s c 的消息得到若干个事件序列的集合，然后将多个事 件序列在具有共同前缀的地方连接起来。由于前缀树识别器是直接根据 用户场景的事件序列转换而来的，没有很好地揭示若干事件和状态之间 的本质联系，并且包含大量的冗余状态，所以需要对这些状态进行合并。 合并状态后的系统可能接受更多的事件序列，然后将这些新产生的序列 提交给用户判断：目标系统中能否出现这样的事件序列，并根据得到的 回答来辅助合并的过程。这个过程类似一个具有负反馈能力的抽象机器， 它的控制部件是合并状态的算法，反馈部件是最终用户，系统输入是初 始场景集，系统输出是完成状态合并的自动机模型，反馈输入是合并后 新接收的事件序列，反馈输出的是最终用户对这个事件序列所作的判断。 如果系统合并过多( 或过少) 的状态，通过反馈就会抑制这个过多( 或 过少) 的合并，使得生成的自动机平稳、渐进地趋向于目标系统。由此 就可以把用户场景的形式化过程映射为系统模型的归纳过程。根据合并 好的自动机模型，依照映射规则就可以按部就班地编写组件的代码框架。 最后利用面向对象的软件设计方法，将每个系统组件封装为一个进程并 填充具体代码，从而完成从最初场景到最终代码的整个流程。 【关键词】：需求工程，场景，需求捕获，需求分析，有限自动机，消 息序列图( m s c ) ，标号迁移系统( l t s ) m a b s t r a c t w i t ht h er a p i dd e v e l o p m e n to fs o f t w a r ee n g i n e e r i n g , p e o p l e h a v e a l r e a d yb e g u n t or e a l i z et h ei m p o r t a n c eo fs o f t w a r ee n g i n e e r i n g a ss o f t v 鹏 r e q u i r e m e n t sa n a l y s i si s a ne x t r e m e l yi m p o r t a n ts t a g ei ns o f t w a r el i f ec y c l e t h a th a sa ni i l n u e n c eo nt h es o f t w a r ep r o j e c tw h e t h e ri ss u c c e s s f u lo rn o t ，a n d t oal a r g ee x t e n ta f f e c t e dt h eq u a l i t yo fs o f t w a r ep r o d u c t s t h e r e f o r e ，h o wt o m o r ee f f e c t i v e l yc a p t u r et h er e a ln e e d so f u s e r si sb o u n d t ob e c o m et h ef o c u s o ft h es t u d y a n dt h es c e n a r i o sw 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 r r e q u i r e m e n t se h c i m f 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 ，a n dt h e ys u p p o r t a f o r m a l ，i n f o r m a l ，n a r r a t i v ea n dc o n c r e t es t y l ed e s c r i p t i o n , a j n dt h e y a l s o c 。n c e 翻st h ed y n a m i cc h a r a c t e r i s t i c so fi n t e r a c t i v es o f t w a r ee n v i r o n m e n t t h u ss y s t e md e v i s e r sa n dn s e r si nt h ep r o c e s so f n e e d sa n a l y s i sc a ne a s i l y u s et h es c e n 剐j o st oe x p r e s st h e i ru n d e r s t a n d i n ga b o u t t h en e e d sf o ra c h i e v i n g o p r i m a ls t a t eo f t h ei n t e r a c t i o n ，a n db e t t e ra c c e s st ou s e rr e q u i r e m e n t s o n l y i nt h i sw a y , u s e r st a k eg e n u i n ep a r t i c i p a t i o ni nt h er e q u i r e m e n t sa n a l y s i s p r o c e s sc a r le a s i l ym a pa p p l i c a t i o nf i e l dp r o b l e m i n t oc o m p u t e rf i e l d ，a n di 1 1 t h ep r o c e s so fi t e r a t i v er e q u i r e m e n t sc a p t u r e c a na u t o m a t i c a l l ya d a p tt o a p p l i c a t i o ns y s t e mr e q u i r e m e n t sc o n s t a n t l yc h a n g i n g , a n d a v o i dr e q u h m e n 协 c h a n g i n gr e s u l t i n gi nt h ec h a n g i n go f t h es t r u c t u r eo ft h es o f t w a r es y s t e m n k a n w b i l e t h e r ee x i s tat i m e l yw a yt oa d dn e w o rm o d i f i e dn o tm e e tt h e a c t u a lr e q u i r e m e n t so ft h eu s e r s w h i c hc a nh e l pe n s u r et h ec o l l e c ta n d i n t e g r i t yo fa p p l i c a t i o ns o f t w a r e a tt h eb e g i n n i n g 。w eg e ti n f o r m a ld e s c r i p t i o n sa b o u ts c e n a r i o ，b u t b e c a u s es o f t w a r es y s t e ma sa ne n g i n e e rg o a lc o n s i s t so f r u n t i m ee n v i r o n m e n t ， t h e yh a v el a r g e d i f f e r e n c e sf r o mc o n t e x tt of o r m t h e r e f o r e ，m a p p i n g b e t w e e nt h e mi se s s e n t i a l ，7w h i c hc a nc o r r e c t l y g e tm o d e l i n go n u s e r r e q u i r e m e n t s t r a d i t i o n a ls t r u c t u r e dm e t h o dw i l lr e g a r ds o f t w a r es y s t e ma s d a t ap r o c e s s ，a n du $ ef u n c t i o nd e c o m p o s em e t h o dt om a k es y s t e mi n t o d i f f e r e n c ef u n c t i o nm o d u l e ，e a c hm o d u l eh a sas u bp r o c e s s a to n et i m e s t r u c t u r e dm e t h o di st h em a i n s t r e a mt e c h n o l o g yi ns o f t w a r ee n g i n e e r i n g p r a c t i c e ，a n d h a sa l l i m p o r t a n t i n f l u e n c ea sy e t w i t ht h ei n c r e a s i n g c o m p l e x i t yo fm o d e ms o t t w a r es y s t e m s ，c o n t i n u a l l yc h a n g i n gb e t w e e n t h e v a r i o u sc o m p o n e n t so fd y n a m i ci n t e r a c t i v er e l a t i o n s w h i c hm a k et h e s t r u c t u r e dm e t h o dm o r ed i f f i c u l tt ou s e t h e r e f o r e , h o wt oi n d u c es y s t e mf u n c t i o n sa n di n t e r a c t i o n s b e t w e e n c o m p o n e n t sa n dp a r t i c i p a n t sh a sb e c o m e m a i nt a s ki ne n g i n e e r i n gp r a c t i c e i f s t a t em o d e la n dc o d ef r a m ec a nb es y n t h e s i z e da c c o r d i n g l y , i tw i l lb eo f g r e a t b e n e f i tt oi m p r o v i n gs o f t w a r eq u a l i t ya n dt os a v i n gc o s t w i t ht r a d i t i o n a l a n a l y s i s ，i n f o r m a lm e t h o da n dc r e a t i v et h i n k i n gw i l lb eu s e di nt h ea n a l y t i c p r o c e s s i nt h em e a n t i m e ，d u et od i f f e r e n tw o r k i n g r e a l n = l sa n dt h i n k i n g m o d e l s ，p e o p l et e n dt oh a v ec o m m u n i c a t i o nd i f f i c u l t i e s ，r e s u l t i n g i na n i n c o r r e c ta n di n c o m p l e t er e q u i r e m e n ts p e c i f i c a t i o n s oi ti sa l s oi m p o r t a n tt o v f u l f i l le f f e c t i v ec o m m u n i c a t i o n o u to f t h e s ec o n s i d e r a t i o n s ，u s e rs h o u l df i r s t s u b m i ti n i t i a lp o s i t i v ea n dn e g a t i v es c e n a r i o s ，a n do nt h eb a s eo fw h i c ha g l o b a ls y s t e m s t a t en l a c h i n ew i l lb ec r e a t e d a tt h es a m e t i m e ，m o r ei m p l i c a t e s c e n a r i o s ( b o t hp o s i t i v ea n dn e g a t i v e ) w i l lb eg e n e r a t e d , w h i c hw i l la s s i s tt h e g e n e r a t i o no ft h es t a t em a c h i n e a tl a s t , w ew i l lf i n i s ht h ep r o c e s sw h i c h i n v o l v e ss u b m i t t i n gs c e n a r i o so fu s e ra n dr e q u i r e m e n tm o d e le s t a b l i s h m e n t u t i l i z i n gf o r m a lm e t h o d m e a n w h i l e ，b a s i cc o n c e p t so f s o m ep r e v a l e n tf o r m a l m o d e l i n gm e t h o d sw i l lb ei n t r o d u c e dw i me m p h a s i so na u t o m a t o na n d r e l a t e dt e c h n o l o g i e s i no r d e rt os t u d ya c q u i r i n gs y s t e mb e h a v i o rs p e c i f i c a t i o nf r o ms c e n a r i o s r e q u i r e m e n ts p e c i f i c a t i o n , t h i sp a p e rw i l li l l u s t r a t ep r o c e d u r e so fam s c l ( m e s s a g es e q u e n c ec h a r t ) b a s e dm e t h o df o ra n a l y z i n gt h er e q u i r e m e n t s p e c i f i c a t i o nb ya ne x a m p l eo fm o d e l i n gas h o r tm e s s a g es y s t e m f o rt h e p u r p o s eo fa c q u i r i n gf o r m a lb e h a v i o rs p e c i f i c a t i o n ，p t a ( p r e f mt r e e a c c e p t o r ) w i l lb es y n t h e s i z e df r o ms c e n a r i o ss u b m i t t e db yu s e r , t h a ti st os a y , d r a wm s cf r o md e s c r i p t i o n so fs c e n a r i o s ，t h e nt r a v e r s em e s s a g e si nm s c a n dg a i nas e to fs t r i n g so fm e s s a g e s ，f i n a l l yc o n n e c tt h em e s s a g e ss t r i n g sa t t h ep o i n tw h e r et h e yh a v em a x i m u mc o m m o n p r e f i xt of o r m at r e e b e c a u s e t h ep t ai sd i r e c t l yc o n v e r t e df r o mm e s s a g e ss t r i n g so fu s e rs c e n a r i o s ，i th a s n o tu n c o v e rt h ee s s e n c ec o n n e c t i o nb e t w e e nm e s s a g e sa n ds t a t e s i ta l s o i n c l u d e sm a n yr e d u n d a n ts t a t e sw h i c hs h o u l db em e r g e d a u t o m a t o nw i t h m e r g e ds t a t em a ya c c e p tm o r es t r i n g st h a nu n m e r g e dc o u n t e r p a r t t h e s en e w v i s t r i n g ss h o u l db es u b m i t t e dt ou s e r , s oh ec a nj u d g ew h e t h e ro b j e c ts y s t e m p e r m i t st h e s em e s s a g e ss t r i n g s t h e8 n s w e rw i l la s s i s tt h em e r g i n gp r o c e s s t h ep r o c e s si sl i k ea na b s t r a c tm a c h i n ew i t hi n v e r s es i g n a lf e e d b a c k c a p a b i l i t y i t s c o n t r o lu n i ti ss y n t h e s i sa l g o r i t h m , f e e d b a c ku n i ti su s e r , s y s t e mi n p u ti si n i t i a ls c e n a r i o s ，s y s t e mo u t p u t i sa u t o m a t o nm o d e lw i t hs t a t e w e l lm e r g e d ，f e e d b a c ki n p u ti sn e w m e s s a g e ss t r i n g sg e n e r a t e df i o mm e r g i n g s t a t e ，f e e d b a c ko u ti s u s e rv i e wo i lt h e s es t r i n g s i fh a v et o om a n yo rf e w m e r g es o r t s ，t h e s ee x c e s sw i l lb e s u p p r e s s e db yn e g a t i v ef e e d b a c k , m a k i n g r e s u l t a n ta u t o m a t o ns t a b l ea n dg r a d u a lt e n d st oo b j e c ts y s t e m t h u st h e f o r m a ls y n t h e s i so f u s e rs c e n a r i o sc a nb eo b t a i n e db yi n d u c i n gs y s t e mm o d e l f r o mr e s u l t a n ta u t o m a t o n ，u s i n gas e to ft r a n s i t i o nr o l e s ，c o d ef r a m ec a l lb e w r i t t e nb yh a n d f i n a l l yu s i n go b j e c t - o r i e n t e dp r o g r a m m i n gm e t h o d , e a c h s y s t e mc o m p o n e n tw i l lb ei m p l e m e n t e da sap r o c e s sa n dr i f l e db yc o n c r e t e c o d e s ，t h ep r o c e s s e sf r o mi n i t i a ls c e n a r i o st of i n a lc o d e sw i l lb ec o m p l e t e 【k e yw o r d s 】：r e q u i r e m e n te n g i n e e r i n g ，s c e n a r i o ，r e q u i r e m e n t e l i c i t a t i o n ，r e q u i r e m e n ta n a l y s i s ，f h l i 钯s t a t ea u t o m a t a ，m e s s a g es e q u e n c e c h a r t i 学位论文独创性声明 本入声明所星交的学位论文是我个人在导师指导下进行的研究工作及取得 的研究成果。论文中除了特另q 加以标注和致谢的地方外。不包含其他人或其饱机 构已经发表或撰写过的研究成果。其他同志对本研究的启发和所傲的贡献均已在 论文中作了明确的声明井表示了谢意。 研究生签名；弘磁焉日期；工一斗目功日 学位论文使用授权声明 本人完全了解浙江师范大学有关保留、使用学位论文的规定，即：学校有权 保留送交论文的复印件和电予文档，允许论文被查阅和借阅，可以采用影印、缩 印或扫描等手段傈存，汇编学位论文。同意浙江师范大学可以用不同方式在不同 媒体上发表、传播论文的全都或部分内容。保密的学位论文在解密后遵守此协议。 砑究生签磐； 够略 导师签 犰妒7 、p 浙江师范大学学位论文诚信承诺书 我承诺自觉遵守浙江师范大学研究生学术道德规范管理条 例。我的学位论文中凡引用他人已经发表或未发表的成果、数据、 观点等，均已明确注明并详细列出有关文献的名称、作者、年份、 刊物名称和出版文献的出版机构、出版地和版次等内容。论文中 来注明的内容为本人的研究成果。 如有违反，本人接受处罚并承担一切责任。 承诺人( 研究生) ： ? 麟 i 指导教研亭 f7 厂7 l 缈 第一章绪论 ( 一) 研究背景 第一章绪论 自从n a t o ( 北大西洋公约组织) 于1 9 6 8 年在德国格密斯( g a r m i s h ) 举行的学 术会议上正式提出“软件工程”概念以来m ，软件工程一直发展迅速，至今已有3 0 多年的历史。然而由于软件产品自身具有的功能多样性、实现多样性、能见度低、 软件结构合理性差等特点，直接影响了整个软件工程的质量和成本，而衡量软件系 统是否成功的方法主要是看其功能是否满足用户的预期需要。简单的说，需求工程 是通过识别参与者及其需求，并将结果用形式化方法记录下来的过程。交流困难是 这个过程所面临的主要问题之一。参与者( 包括购买客户，使用者和开发者) 可能 人员众多并且分布在不f 司地点，而工作内容的差异性又会造成不同的视野。因而他 们的目的可能各异或者产生冲突，他们的目标可能不明确或不容易清楚豹表达出来， 所以满足他们的需求必然受限于一些外在的环境因素。另外，对于用户来说，他们 只关心其个人如何使用系统。并不知道也不想了解系统的内部结构、设计及整体的 运行情况，他们所关心的只是系统所能提供的服务，也就是被开发出来的系统将是 如何被使用的。这些用户所关注的重点也将影响到需求获取的实施过程，而具有作 为软件生存周期关键过程的需求分析( r a ) 对于项目的所有参与者来说都是至关重 要的。髓着系统逐渐庞大，逻辑扫趋复杂，完全依赖非形式化的分析方法将越来越 力不从心。随着问题域和实现域的差距增大，理论和实践都期待着形式化方法能更 有效地辅助软件生产过程。因此，如何获取用户对应用系统的需求( 需求引出) 并将 其应用于后续阶段将成为本篇研究的重点。 目前已有若干技术用于需求分析，选择基于什么样的技术来做好需求分析也是人 们争论的焦点，有些研究人员认为其中i v a rj a c o b s o n 在爱立信公司开发a x e 交换 机时所研究的用例分析技术具有其一定的优势，用例分析技术嘲是完全以用户的角度 ( 也就是从系统外部) 来描述系统的功能，它不去关心系统内部的功能实现，而仅仅 描述被定义韵系统与外部参与者的交互行为，然后针对每一个参与者来描述系统为 这些参与者提供的服务，从而有效地界定了系统的使用范围和功能行为。由于用例 浙江师范大学硕士学位论文 具有的诸多优点，后来，也就是在1 9 8 6 年被总结发展成一项来源于实践的需求分析 技术0 1 。除此之外，也有很多研究人士认为场景比较适合描述应用软件的系统行为及 其功能，其具有很好的直观性并且易于用户与设计开发者之间的交流，因此基于场 景的需求工程也得到广泛的推广，并取得了丰硕的成果。与此同时，基于场景引出 需求的过程还有部分尚未得到解决的问题，例如缺乏有效的工具支持等等，其主要 原因就是难于设计一种合适的表示方法来描述场景。 对于传统的非形式化需求建模方法容易产生用户实际需求与系统设计人员的理 解发生不一致的情况，因而难以得到确认及验证。另外，由于用户需求的频繁变更， 甚至导致系统结构发生根本改动，这也影响到需求分析的整体效率。建立在数学基 础之上的形式化方法用于描述需求规约则能够避免语义的二义性，有助于修改和验 证，是目前较为实用的一种行为建模工具。 ( 二) 国内外研究现状 1 2 1 需求分析工具的研究现状和发展趋势 许多国外专家在面向场景的需求建模技术研究领域做出了贡献，已建立并被实践 证明的理论丰富并发展了需求工程学，也给我们现在的研究提供了坚实可靠的理论 基础。但是这些方法并非尽善尽美，也存在一些不足之处，这正为我们的研究工作 提供了明确的方向。另外，国内的一些专家研究并实现的用于需求建模的实用工具， 具有很好的发展前景。接下来将介绍其中的部分方法及其在具体实践中的应用。 w h i t t l e 和s c h u m a n n 提出了一种从仅捕获期望场景的序列图产生u m l 状态图的 技术刚。他们的方法受限于先决条件和事后条件，需要对场景交互进行注释，这些注 释作用于全局状态变量并通过约束语言来表达。与此类似，k r u g e r 等人提出一种将 m s c 翻译到状态图嘲的技术。该技术也需要为m s c 输入额外的状态信息为前提条件。 两种方案都无法确定最终用户能否提供这样的附加信息。 m a k i n e n 和s y s t a 发展了一种从捕获期望场景的序列图合成u 札状态图的交互式 方案鲫。他们为避免不期望的概括，用最小充分分析器( 姒s ) 使用语法推论和向用户 2 第一章绪论 追踪提问来实现，其中追踪提问是一个自动机相对于一个特定的a g e n t 的路径。砒s 关注单一的a g e n t ；因而概括只是针对于每个软件a g e n t 独立实现。最终用户也许很 难理解独立的问题，因为其未揭示全局系统行为。用潜在假设观点追踪具有相同标 号且转到相同组件的事件很容易发生过度概括，除非其中指明例外场景。因此，为 去掉不正确的概括，用户需要理解和验证a g e n t 产生的自动机，并提供反例的自动 机追踪，以指出不希望的行为且重新进行概括过程。 ，u c h i t e l 等人开发了一个为场景的每个消息序列图规约( 1 l s c ) 的a g e n t 产生标号 迁移系统技术( l t s ) 啊。这个方案需要额外的输入信息。即高层消息序列图( h 淞c ) ， 也就是指定m s c 场景怎样建造流程图。根据以往研究人员的经验，这样的h m s c 对于 现实系统会变得相当复杂。在需求规约中增加新的m s c 也可能需要对h m s c 蛔进行一 定的重复工作，而向最终用户索要正确并完整的h m s c 作为输入信息看来也不太现实， 并且l t s 的合成技术没有把反例考虑进去，其合成的l t s 的数字标记也不容易理解。 v a nl a m s w e e r d e 和w i l l e m e t 为了使用线形时间逻辑，从类似m s c 形式的期望 例外场景产生目标规格开发了一种感应学习技术嘲。可以使用已知算法从l t l 规格产 生b u e h i 自动机，然而产生的自动机非常难以理解和验证。用户需要迸一步为场景 交互提供先决事后条件。 中国科学院数学所陆汝铃教授等入设计的支持管理信息开发环境的p r 侧i s “， 二 主要实现的是基于内容丰富的知识库来支持管理信息系统的开发。知识库不仅涵盖 领域知识而且涉及软件工程知识领域。p r o m i s 通过对用户的领域业务信息进行模型 匹配、扩展、修改、补充等工作，最终转化用户需求为目标管理信息系统原型。 南京大学计算机软件所通过对需求级软件自动化技术及系统的初步研究探索，设 计了o r a s s 1 ( o b j e c t - o r i e n t e dr e q u i r e m e n ts y s t e m ) 。o p n s s 由需求定义支撑子 系统o r s 和需求定义自动转化子系统f u n s 组成。o r s 支持面向对象的需求模型h o r m 的架构，形成软件需求定义。f u n s 实现从图形化语言o r l 描述的需求定义到面向对 象规格语言o o z e ( o b j e c t - o r i e n t e dze n v i r o n m e n t ) 书写的形式功能规格的自动转换 【l 对 浙江师范大学硕士学位论文 ， 1 2 2 形式化方法的研究现状 根据软件产品在不同业务领域具有的不同应用特点，研究人员提出了多种形式化 建模的方法。本节主要介绍有限自动机( f i n i t es t a t ea u t o m a t a ) 方法、状态图 ( s t a t e c h 8 r t s j 方法、演算和p e t r in e t 方法，至于其它形式化建模方法，在这 里就不再一一介绍了，有兴趣的读者可以查阅相关文献。 1 2 2 1 有限自动机 有限状态自动机( f i n i t es t a t ea 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 非常适合描述包含有限个状态，并 且事件的发生将导致状态迁移的这类系统”1 。 有限自动机可以用一个5 元组m - ( q ，6 ，q ，f ) 来表示，其中q = q o ，q l ，q r i 是有限状态集合。在任_ 确定的时刻，有限状态自动机只能处于一个确定的状态q i ； 是字母表，6 ：q x 一q 是状态转移函数，q o 是初始状态，有限状态自动机由 此状态开始接受输入。f 是识别可接受状态的q 的子集，即终结状态集合，有限状态 自动机在达到终态后不再接收输入“”。如果任何q 在q 内且任何e 在，6 ( q ，e ) 至多有一个成员，那么自动机就被认为是确定性的。 4 第一章绪论 1 2 2 2 状态围 状态图( s t a t e c h a r t s ) 是由以色列的d a v i dh a r e l 建立的传统有限状态自动机 的一种扩展形式。状态图中通过引入状态的递阶、状态的与分解和或分解等高级特 性，使得问题规格的状态图的状态数目极大减少，从而也具备了更强的描述能力“”。 状态图也可以描述成对离散事件系统进行行为建模的图形化语言，由于使用图形来 表示系统的行为活动，所以与其他方法相比，它更易理解，并且具有很好的交互性。 1 9 8 7 年，d a v i d 1 a r e l 又在计算机编程科学中发表论文“扩展状态图，解决复杂 系统设计的可视化方法”“”。在此对状态图进行了更为详细地描述。介绍了如何扩 展传统的状态图，并增加了分层、并行等功能，从而使状态图具有并发性及层次性 的特点，为复杂交互式系统创造了强大的可视化编程条件，随着用户复杂需求的不 断涌现，复杂式交互系统越来越受到人们的青睐。扩展状态图主要适用于通讯、制 造业和自动化工业等广泛领域，并且快速发展为这些行业的统一标准。扩展状态图 也广泛用于面向对象方法论中的对象建模技术( 0 岍) 和统一建模语言( u m l ) 中。 i 2 2 ：3p e t r i 翻 p e t r i 网：最早是由德国的c a r la d a mp e t r i 于1 9 6 2 年在其博士论文自动机 通信里提出的。它是一种适合并发、异步、分布式软件系统规格与分析的形式化 方法。p e t r i 网分为位置迁移p e t r i 网和高级p e t r i 网【“。它是模拟并行系统和分 布式系统的种强有效的形式化工具。能够很好地刻画系统的动态行为、分析系统 的总体性能。由于p e t r i 网具有很好的异步并发性，所以适合分布式系统的建模“”。 p e t r i 网是用计算机语言表达了客观世界的普遍联系规律的系统模型。p e t r i 网在计 算能力上与图灵机等价。显而易见，软件系统是属于自动机范畴的，而通信又是软 件系统各组件或系统间的协作、交互方式，所以软件系统的协同计算可以认为是遵 循p e t r i 网理论的。 浙江师范大学硕士学位论文 1 2 2 4n 演算 h 演算是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 u n i c a t i n gs y s t e m s ) “。 的基础上提出的传名演算，n 演算包含两种类型的实体，其中一个是进程，另一个 为信道。名字是n 演算中最基本的实体，像端口、信道和链路都是名字。而信道名 字作为进程事件的符号元素出现。另外，n 演算还具有很好的描述能力，有利于刻 画出具有动态结构的单进程内部及多进程之间的交互过程。 ( 三) 研究内容 本篇研究了以场景为出发点引出需求，然后利用形式化方法分析出相应的行为模 型，从而迈出从客观世界到计算机实现的第一步，得到问题空间与解空间之间的初 步过渡，使得从场景自动生成目标系统成为可能。通过使用抽象及形式化方法，减 少了因使用非形式化方法所带来的工作量，降低了软件系统的总造价，而形式化验 证场景更降低了软件的测试成本，潜在地提高了软件的正确性、质量、效率和可靠 性“”。同时，为了适应用户的需求变更和需求不确定性，通过捕获需求相关的用户 场景将产生一系列软件系统与周围环境的交互，以此来获取系统行为，对其具体的、 描述性的表达使其可有效引出软件需求和验证行为模型。 本篇将构造一种从最终用户场景产生行为模型的技术，主要思路包括： 1 根据用户描述产生最终用户场景，并且不要求用户提供更多的额外输入信息。场 景将主要使用简单符号图形来表示。 2 期望场景和例外场景都被包括在内。例外场景不但经常出现在用户提供的描述中， 而且其对合成最后的模型也是必不可少的。 3 由于人类思维的有限性和局部性，最初给出的场景很难具有完整性。产生的模型 应当支持引出额外的场景作为对最终用户提供的初始场景的补充，即隐含的场景。 4 从场景转化成行为模型应当是增量修改、提交的过程。 5 考虑到分析问题的渐进性，行为模型应当在填充具体代码前能够被验证和修改。 6 第一章绪论 本篇弓l 入消息序列图、前缀树识别器和标号迁移系统。作为主要的形式规约的描 述工具。随后，阐述了将场景的自然语言描述转化为功能规约的步骤。最后，根据 上述步骤建立了自动售票系统的行为模型并给出了部分系统组件的实现。 ( 四) 论文结构 第一章介绍本篇的研究背景、国内外需求建模方法的现状、本篇研究内容及文章结 构。 第二章叙述了场景的概念、分类及用于描述场景间交互的消息序列图( m s c ) 的概念。 介绍了由消息序列图转换成一种形式化的中间结构一前缀树识别器，并用一个简单的 短信服务系统来举例说明其转换步骤。 ， 第三章详细介绍了形式化功能规约方法，分析了本篇所用建模方法的优势所在，并 解释i 了后续章节里所用到的符号含义。继续以短信服务系统为例说明了利用标号迁 移系统从前缀树识别器到目标系统的实现步骤，同时详细说明了这个过程中使用到 的算法思想及部分伪代码。 第四章通过给出自动售( 电影) 票机实例，呈现了一个从场景到需求模型生成、不断 完善的完整步骤，其中包括场景的文本描述、m s c 描述、l t s 表示及代码实现。 第五章对本篇的工作进行了总结，归纳了通过自动售( 电影) 票机实例所解决的预期 问题，并且探讨了进一步的研究方向。 ( 五) 本章小节 本章是绪论部分，着重介绍了论文的研究背景、国内外研究现状及研究内容，同 时对论文的组织结构做了简要的说明。 第1 节阐述了本篇的来源与研究背景。 第