没有合适的资源?快使用搜索试试~ 我知道了~
理论计算机科学电子笔记133(2005)237-254www.elsevier.com/locate/entcs关键任务系统的早期验证和确认C. Ponsard,P. Massonet,A. Rifaut和J.F. Molderez1CETIC研究中心,比利时A. van Lamsweerde和H.陈文2Universit'ecatholiquedeLouvain,Depa rmentofComputerScience,Belgium摘要我们的世界越来越依赖复杂的软件和系统。在越来越多的领域,如运输、金融、电信、医疗设备等,它们现在发挥着关键作用,需要高度的保证。为了实现这一点,必须生产高质量的要求。KAOS面向目标的需求工程方法为此类系统的需求获取和管理提供了一个丰富的框架。本文展示了该方法的实际工业应用。非关键部分使用面向目标需求工程的图形语言进行半正式建模。在需要的时候和地方(例如)对于系统的关键部分),可以使用实时时序逻辑在形式级别指定模型。这种正式的层次无缝地扩展了半正式的层次,这也有助于为非专业人士隐藏正式为了确保在早期阶段构建正确的系统以及需求模型是正确的,验证和验证工具被应用于该模型。早期验证检查有助于发现遗漏的需求、被忽视的假设或不正确的目标细化。从操作生成的状态机提供了一个可执行模型,用于验证目的或用于导出初始设计。验收测试用例和运行时行为监视器也可以从模型中导出。这一过程得到了一个综合工具箱的支持,该工具箱通过将KAOS要求级符号往返映射到模型检查器、SAT引擎或约束求解器等正式技术工具的语言来实现上述工具。图形化可视化框架也可以显著帮助使用基于域的表示进行验证。关键词:需求工程,目标导向,早期验证,确认,动画,监控,验收测试1571-0661 © 2005 Elsevier B.V. 在CC BY-NC-ND许可下开放访问。doi:10.1016/j.entcs.2004.08.067238C. Ponsard等人/理论计算机科学电子笔记133(2005)237----1介绍复杂的软件和系统在当今世界无处不在。在越来越多的领域,他们开始发挥关键作用,因为他们的不正确行为可能导致灾难性的损失,包括成本、对环境的破坏,甚至是人类生命。为了产生高度可靠的系统,建议使用正式的方法。它们指的是基于数学的语言,技术和工具,用于指定和验证这些系统。尽管有一些成功的故事,但正式方法尚未获得广泛的工业采用-主要障碍是学习困难技术的重大投资以及通常对数学的心理抵制。为了克服这些问题,现在正在探索替代方法,例如轻量级形式化方法[4]和隐形形式化方法[17]。前者是一个目标应用程序,其范围和分析有限,以最小的成本得出相关结论后者旨在为从业者提供足够方便、强大和有用的技术,使他们愿意采用这些技术为了实现高保证,许多研究也强调了需求阶段的重要性[5][6]。一些严重的失败可以以某种方式追溯到需求问题[11][12]。目前,大多数需求工程方法依赖于结构化的自然语言或半形式化的符号,如UML,缺乏精确的语义,从而具有较差的推理能力。形式化方法通常应用于软件规格说明,而需求则考虑由软件及其环境组成的复合系统。通常,所使用的方法缺少基本的需求工程问题,例如捕获基本原理、对需求详细说明的充分指导和对替代方案探索的支持。在[23]中,有人认为目标需要正确的抽象来解决这些不足之处,特别是在高保证系统的背景下;这是一种需要令人信服的证据的系统,该系统以满足安全性,安全性,容错性和生存性要求的方式提供服务[15]。面向目标的需求工程的关键活动是目标模型的建立。目标是正在构建的系统必须实现的目标。因此,目标公式是指要确保的预期特性。它们是在不同的抽象层次上制定的,这些抽象层次来自高层次的战略问题(如1封电子邮件:cp,phm,ari,cetic.be2电子邮件:avl,info.ucl.ac.be3这项工作得到了欧盟(ERDF和ESF)和瓦隆大区(DGTRE)的财政支持。C. Ponsard等人/理论计算机科学电子笔记133(2005)237239我们将在整个本文中考虑的加速系统)到低级技术问题(例如“及时传递加速命令”)。目标模型还允许分析师捕捉和探索给定目标的替代细化。目标模型的结果结构是一个AND-OR图。这里考虑的特定目标导向框架是KAOS方法学[2][24],它有两个层次的语言:(1)外部半正式层,用于捕获需求工程概念,结构化和呈现它们;(2)内部正式断言层,用于精确定义和推理。本文的目的是提出一个概述FAUST正式工具箱,详细说明个人的工具,并显示如何,在一起,他们提供强大的推理能力,在系统开发的早期阶段。图1显示了位于软件生命周期顶层• 早期验证是为了确保系统是正确的,特别是在目标模型的形式化语义• 验证是关于确保正在构建的系统是用户期望的系统。• 伪像生成是关于自动生成在软件生命周期后期使用的产品,例如验收测试用例或运行时监视器。Fig. 1. FAUST工具箱FAUST工具箱旨在通过以下方式使需求工程满足实际的形式化方法:• 无缝集成半正式和正式描述,允许一将后者的范围限制在所模拟系统的关键部分;• 隐藏了大部分的正式方面,例如。通过基于领域级表示的动画生成;• 提供面向目标的正式工具,这些工具封装了现有的正式技术,240C. Ponsard等人/理论计算机科学电子笔记133(2005)237∼例如定理证明器、模型检查器、SAT引擎、约束求解器等。• 在可能的情况下重用标准符号-例如,UML类图、序列图、状态机图。本文其余部分的结构如下。第二节介绍了KAOS的背景知识及其形式语义.第3节概述了工具箱支持的功能。第4节和第5节分别详细介绍了两个成熟的工具:早期分析器(主要是关于验证)和动画器(主要是关于验证)。该工具在列车控制系统上的演示可以在http://www.cetic.be/faust/demo上下载。该系统包括多列火车沿着一组圆形单轨块移动,这些块具有多个车站,块信号,铁路道口门和车厢。这里只说明这个模型的一个子集2混沌的背景KAOS需求模型由四个子模型组成:目标模型,对象模型,代理模型和操作模型;这些模型使用面向目标的方法进行了系统的阐述,参见[20]。目标是关于某个系统(现有系统)的意图的规定性声明。 或将来),其满足通常需要形成该系统的一些代理的合作。代理是活跃的组件,例如人,设备,遗留软件或软件组件,它们在实现目标方面发挥着一定的作用。因此,一些代理定义软件,而其他代理定义其环境。目标可以指要提供的服务(功能性目标)或服务质量(非功能性目标)。与目标不同,领域属性是对环境的描述性陈述,如物理定律、组织规范或政策等。2.1建立目标模型目标以AND/OR细化抽象层次结构组织,其中较高级别的目标通常是战略性的,粗粒度的,涉及多个代理,而较低级别的目标通常是技术性的,细粒度的,涉及较少的代理[2][3]。在这样的结构中,AND-精化链接将目标与一组可能与域属性结合的子目标(称为精化)联系起来;这意味着满足精化中的所有子目标是域中满足目标的充分条件。OR-细化链接可以将目标与一组替代细化相关联目标细化结束C. Ponsard等人/理论计算机科学电子笔记133(2005)237241当每个子目标都可以由分配给它的某个个体主体实现时,也就是说,可以用主体可监控和可控制的条件来表达。需求是软件中主体负责的最终目标;期望是环境中主体负责的最终目标。目标规定了预期的行为;它们可选地在实时时序逻辑中形式化[2][8][14]。关键词,如实现,避免,保持是用来命名的目标,根据时间的行为模式,他们预先。图二. 用于列车控制系统图 2 显 示 了 我 们 的 列 车 控 制 系 统 的 目 标 模 型 片 段 。 叶 目 标Maintain[DoorsClosedWhileMoving]可以用以下时间逻辑断言来注释,该时间逻辑断言声明在每个未来状态中,当列车正在移动时,列车门将被关闭(火车)动了门关上了。还请注意,对目标NoTrainCollision的替代细化导致了完全不同的设计:NoTrainOn-SameBlock的基于块的设计和WorstCaseStop-pingDistanceMaintained的速度控制设计(或移动块)。目标指的是可以从目标规范中逐步派生的对象,以产生系统的结构模型(类似于UML类图)。对象的状态由其属性值和与其他对象的关联定义。 它们是被动的(实体、关联、事件) 或活性(代理)。代理通过它们各自监视和 控 制 的 对 象 属 性 和 关 联 组 成 的 接 口 相 互 关 联 [9] 。 在 上 述 目 标DoorsClosedWhileMoving的形式化中,Moving和doorsState是对象模型中声明的Train实体的属性242C. Ponsard等人/理论计算机科学电子笔记133(2005)237如果将目标DoorsClosedWhileMoving分配给TrainController代理,则后者必须能够监视属性Moving并控制属性doorsStateof trains。目标规范规定了一组预期的系统行为,其中行为被定义为系统状态的时间序列。目标细化的形式语义在[3]中给出定义2.1(目标细化的语义)一组目标G1,.,Gn在域理论D中精化目标G,如果以下条件成立:完备性:G1,G2,.,Gn,D| = G最小值:j/=Gij, D|= Gi∈{1,2, . ,n}一致性:G1,G2,. G n,D| = false2.2使目标目标被操作化为实现目标的具体操作[2][10]。操作是对象上的输入输出关系;操作应用程序定义了沿着目标模型规定的行为的状态转换。在操作的规范中,在(描述性的)域前置/后置条件和(规定性的)前置、后置和触发条件之间进行了重要的区分,这些条件是实现某些潜在目标所需的• 一对(域前置条件,域后置条件)捕获由域中的操作应用定义的基本状态转换;• 某个目标所需的前提条件捕获仅当条件为真时执行操作的许可;• 某个目标的所需触发条件捕获在条件变为真的情况下执行操作的义务,前提是域前提条件为真(为了产生一致的操作模型,关于操作的所需触发条件隐含地暗示其所需前提条件的结合);• 所需后置条件定义了操作的任何应用必须建立的某些附加条件,以便实现相应的目标。例如,操作OpenDoor是目标DoorsClosedWhileMoving的操作化之一;它可以部分指定如下:开门行动输入tr:列车输出tr:列车/门状态C. Ponsard等人/理论计算机科学电子笔记133(2005)237243◦DomPretr. doors关闭DomPost<$tr. door关闭移动时门关闭的要求:<$tr.移动目 标 可 操 作 化 就 是 一 组 这 样 的 具 体 化 。 例 如 , 我 们 的 目 标DoorsClosedWhileMoving的操作化包括影响该目标满足的所有操作的规范,即 操 作 OpenDoors 、 CloseDoors 、 StartT rain 和 StopTrain 的 DomPre 、DomPost、ReqPre、ReqTrig和ReqPost条件;这些操作影响目标满足,因为它们的规范捕获了目标规范中出现的状态变量moving和doorsClosed的值的变化。营运投入及产出的确切范围于实体╱关系层面(如:tr:Train)或更精确地在属性级别使用/符号(例如tr:train/doorState)。在本文中,我们假设操作化是从目标规范中推导出来的。对于每个目标指定模式,推理规则可用 于 正 式 推 导 正 确 和 完 整 的 DomPre , DomPost , ReqPre , ReqTrig 和ReqPost条件,以实现相应的目标[10]。在[10]中,操作和操作化的语义定义如下:定义2.2(操作的语义)对于操作模型中的每个操作op,谓词[|op|]定义如下:[|op|](arg1,.,arg n,res1,.,res n)DomPre(op)和DomPost(op)其中arg i表示输入变量,res i表示输出,并且是线性时序逻辑中的“下一状态”运算符。定义2.3(前置条件、触发条件和后置条件的语义)对于操作模型中操作op上的每个必需条件R,pred- icate[|R|]定义如下如果R ∈ ReqPre(op),则[|R|]= def(int n)[|op| [[英]如果R ∈ ReqTrig(op),则[|R|]= def(函数)R DomPre(op)[|op|]如果R ∈ ReqPost(op),则[|R|]= def(int n)[|op| [美国其中(n)P是P的泛闭包。定义2.4(目标可操作化的正确性)一个集合R1,...,如果以下条件成立,则操作模型中的操作的所需条件中的Rn个正确地操作目标模型中的目标G:完整性:R1,...,R n|= G一致性:R1,...,R n|=false最小值:G| = R1,...,Rn244C. Ponsard等人/理论计算机科学电子笔记133(2005)237目标细化和操作化的语义在一个重要的点上是不同的。而子目标则细化了父目标(即,细化目标的模型也是父目标的模型,但并不涵盖父目标的所有模型),每个操作规范和强制要求之间存在逻辑等效性。此外,这种等价性独立于任何域属性:它只依赖于系统上强制执行的要求。这意味着操作和需求可以互换地提供给开发人员。当然,更多的时候是表示向他们提供两种2.3产生稳健的需求目标模型中所有细化的正确性并不能确保规范是一致的:目标之间可能会出现不一致。冲突是这些目标之间逻辑上的不一致。发散是在某些(可行的)边界条件下的逻辑不一致。与目标细化相反,检查不一致性不是目标的局部过程第一草图模型也往往过于理想化,并且由于意外的行为,在运行的系统中可能不时地被违反的代理人。缺乏对这些行为的预期可能会导致不切实际、无法实现和/或不完整的需求。这些异常行为被称为目标满足障碍的正式断言因此,执行冲突和障碍分析对于实现高质量要求至关重要但是,由于FAUST工具箱还不完全支持它们,因此本文不会详细介绍。感兴趣的读者可以参考[22]和[21],了解它们的正式定义以及如何手动发现和处理它们。3关于FAUST本节介绍FAUST工具箱支持的主要形式化活动。这些活动及其数据流如图3所示:• 早期分析器检查关于目标模型的正确性。在错误的情况下,它将产生一个反例跟踪,可以在动画工具中重放。它也可用于验证目的,以生成受约束的动画轨迹。• FSM编译器从操作模型生成有限状态机。这些可以在以后的开发生命周期中使用,也可以在模拟器中执行以进行验证。C. Ponsard等人/理论计算机科学电子笔记133(2005)237245• 模拟器是运行有限状态机实例的引擎它负责捕获来自控制动画的人员的输入命令,以触发相关的转换并将发生的更改通知受影响的可视化组件• Animator是一种可视化工具,允许一个或多个人(可能同时)与模拟交互或重放现有轨迹。它提出了不同的方式来查看/控制设计的系统:符号FSM表示和图形域为基础的可视化。• 测试数据生成器生成验收测试,这些测试可以在开发的系统上进行,以检查它是否满足要求。它们也可以直接在动画中播放• 监控器生成能够检测目标、要求或假设的违反的监控器。这些监视器也可以在运行时部署,也可以在动画制作器中部署。该工具包被开发为Obje t iver需求工程工具的正式扩展[18]。这种集成允许FAUST正式工具依赖于一组强大的服务,用于KAOS建模,持久化,一致性检查和文档生成。下一节将详细介绍早期分析器和动画制作器(包括模拟器、FSM生成器和监视器)图三. 正式活动246C. Ponsard等人/理论计算机科学电子笔记133(2005)237∧ ∧ ∧ ∧∧¬4早期分析师在并行建立四个互补模式的渐进过程中,利益攸关方所作非正式发言的正式化往往会出现分析器的主要目的是在过程的早期阶段验证它们的形式一致性。该工具的另一个用途是生成可能的系统历史以用于验证目的。4.1早期验证所有形式化分析都是基于元素(目标、冲突、障碍、需求、对象、操作等)的形式化语义。. )载于四个模型。大多数情况下,分析器可以自动正式验证给定有限域上这些元素的有效性或无效性作为一个例子,我们将考虑一个目标细化的验证。给定目标细化的语义(见第2节),可以进行以下分析来证明三个必要条件的有效性• 完备性:找到满足G1的迹G2...GnD如果没有找到痕迹,则细化是“证明”(即。在所考虑的有限域)。• 极小性:为了“证明”极小性(在所考虑的有限域上),不应该找到迹:j / = G i j D<$G,i ∈ { 1,2,. ,n}• 一致性:为了“证明”一致性(在所考虑的有限域上),找到一个满足G 1<$G 2 <$的迹。联系我们与操作化、冲突或障碍相关的条件的验证与目标细化所显示的非常相似,在此不再详述。 让我们简单地说明已经陈述的需求DoorClosedWhileMoving的操作化。大多数分析师将通过加强可能导致不安全状态的操作的先决条件来执行该要求:启动列车和打开车门的操作(见图4)。还需要指定安全初始状态。然而,在尝试验证运行模型和要求之间的等效性时,早期分析器将生成以下反例跟踪(考虑单个列车tr#1)1. tr#1. door关闭门<$tr #1.moving2. <$tr#1.doorClosed门关闭tr #1.moving循环回到状态1。这个反例很容易理解:操作Start和Open- Doors在相同的状态下触发,并且“竞态条件”导致系统允许不安全状态在这种情况下,C. Ponsard等人/理论计算机科学电子笔记133(2005)237247对于分析人员来说,理解起来相当简单,但在更复杂的系统中,它们的分析可能会变得相当复杂。动画师将在这项任务中提供很大的帮助,并且当系统行为必须显示给一些利益相关者以进行验证时,动画师是绝对必要的(参见第5节)。见图4。DoorClosedW hileM运行的尝试性实现为了解决同步问题,一种方法是明确禁止这种行为,例如通过声明以下断言:(train:train)tr.moving(火车)<$$>@<$tr. door关闭其责任当然应该受到审查。另一种方法是强制执行后置条件而不是前置条件。事实上,后一种方法被记录为一种众所周知的操作化模式[10],如果分析师首先查看该库,错误就不会发生。在这两种情况下,形式分析器停止返回反例。4.2验证分析器可以自动展示系统及其环境的行为的示例,其满足目标,或显示冲突情况或障碍物的发生,或满足与对象相关联的属性,或显示操作的发生例如,为了显示障碍物O阻止目标G(“列车在穿越街区时没有延迟地前进”)被完成的情况,它表面上显示系统及其环境的迹(状态序列)满足域属性D(“列车不能穿越车厢”)的形式定义当分析器自动生成的轨迹被解释给利益相关者时(例如,轨迹显示一辆汽车被堵在交叉路口),他们可以确认这种情况表明存在障碍物(例如,“汽车撞在交叉路口”),或者这种情况指出了应该修改的目标的248C. Ponsard等人/理论计算机科学电子笔记133(2005)237当交叉路口上没有汽车时在交叉路口上4.3映射到标准形式化技术当用户要求时,分析器必须从一阶线性实时时序逻辑中表达的公式自动产生迹线和证明。与规范分析活动中所做的工作相比,每次分析中使用的公式非常小。分析仪利用这一点如下:1. 对于每个请求,可以选择一个特定的正式工具,它最适合所使用的分析和公式。例如,使用有界模型检查更容易找到跟踪:如果解释符号(例如,整数运算)时,最好使用约束编程技术,而如果不使用解释符号,则基于SAT的技术非常有效。2. 小的公式允许分析器和其他工具之间的简单和未优化的映射:这导致了容易适应新工具的正确代码。3. 运行时间保持很小(通常是秒,很少是分钟)。如果没有得到答案,分析师可以要求使用另一种工具或进行另一次局部分析。因此,分析器主要帮助使用不同的著名的形式化工具,做KAOS形式主义和这些工具的形式主义之间的前向和后向翻译。与其他人的不同之处在于,分析的分裂和他们的结果的整合自然地融入了面向目标的方法论。所使用的工具是NuSMV [1]的基于BDD的引擎和基于SAT的引擎以及Oz [16]的CLP引擎。Alloy [7]的实验表明,最好使用提供高级输入形式主义的工具,这些工具优化了它们到SAT,BDD,...计划使用Alloy,一些自动定理证明器和著名的定理证明器,如StepP或PVS(主要是使用它们强大的决策过程)。不同的映射用有限域替换有限域(例如,“以一个人为中心,以一个人为中心。有界模型检查)。分析员必须解释所获得的结果。例如,如果对约束为无限增大的计数器进行建模,则无法找到有界迹。分析师通常会预见到这一点,因为分析的公式很小。C. Ponsard等人/理论计算机科学电子笔记133(2005)2372495需求动画师面向目标的需求规格说明的动画旨在帮助非技术利益相关者通过与他们熟悉的示例中的规格说明进行交互来验证它们。动画工具是基于混沌的运作模式。它由以下部分组成1. 状态机编译器从KAOS操作描述产生有限状态机描述。在本文中,这些状态机被称为面向目标的状态机(GSM),以强调他们的起源。2. 模拟器允许一个或几个分析师实例化和动画的GSMs,无论是交互式或使用previoulsy计算轨迹。3. 动画制作者界面,包括控制面板和渲染引擎,包括通用GSM查看器和用于设计用户级视觉效果的工具箱。4. 动画监视器,用于监视动画范围内的目标是否违反。5.1从目标操作生成GSM需求动画师需要一个可执行的模型。有限状态机具有这种属性,也具有许多其他有趣的动画特性:它们可以追溯到目标/操作规范语言,它们是组合的以支持并行行为,并且它们已被广泛接受的状态图式符号用于可视化它们。生成算法将目标范围(允许分析部分模型)作为输入,并输出一组可扩展有限状态机。该算法的主要步骤如图5所示。对于完整的算法,读者可以参考[19]。图五. 状态机生成:原理(左)和示例(右)250C. Ponsard等人/理论计算机科学电子笔记133(2005)2375.2模拟器模拟器负责实例化GSMs并管理这些实例。它可以使用以下功能进行控制,这些功能可从动画界面获得。1. 实例浏览器:用于查看所涉及的对象并创建新实例;2. 操作编辑器:用于通过应用启用的操作来触发GSM转换;3. 状态查看器:获取当前GSM实例的原始概览4. 回放工具:用于在生成的动画轨迹中来回播放5.3Animator界面该组件的作用是提供一个适当的接口,以便与动画进行全面的交互。它包括了许多可视化和控制GSM实例的方法。它还部署在客户端-服务器架构上,多个同步接口连接到同一服务器。这允许多用户验证:每个用户模拟系统的一个特定代理,该代理可能行为不端(可能是故意的,例如在设计安全系统时的入侵者为了方便验证,可视化工具以两种形式提供1. 符号GSM查看器允许分析员以其经典的状态图形式显示GSM实例。2. 域级别的图形表示可以映射到GSM上,这些当前基于Scene Bean框架[13]。图6显示了4.2节中讨论的反例的这种图形表示。第一个状态在图片的左边,第二个在右边。两张图片显示:一个象征性的GSM可视化(右下),一个显示列车门的场景(左上),一个列车轨道的场景(右上,与此无关)和一个大的控制面板(在前景中),其中分析仪生成的轨迹正在重放。左边的状态显示了一列停着的火车,车门关闭,右边的状态显示了一列行驶中的火车,车门打开。虽然GSM可视化是通用的,但开发新的域级视图需要一些工作:图形场景必须通过组合图形动画原语来描述,该图形动画原语定义了可用的“精灵”、它们如何移动或改变以及哪些变量与它们相关联。的C. Ponsard等人/理论计算机科学电子笔记133(2005)237251图六、第4.1节反例场景的图示这里使用的SceneBean框架提供了良好的抽象级别,以简单的XML格式描述。它允许设计人员生成一个新的视图,并在几分钟内将其与模拟引擎连接,对于简单的场景(如火车门),对于更复杂的场景(如作为全局轨迹视图)。映射工具有助于将视图连接到基础模型的过程。5.4动画看门狗由于分析人员或验证用户通常希望在使用系统时检查目标满足度,因此模拟器还包含动画监视器。该工具监控动画范围内的所有目标/需求/假设,并报告任何违规行为。它依赖于另一种能够接受有限目标跟踪的有限状态机这些是在GSM生成的同时编译的,但运行完全独立于它们。它们仅在初始化时以及通过侦听系统中发生的状态更改回到我们的例子,图6中的第二个不安全状态在图片的左下角显示了一个监视器弹出窗口。此弹出窗口报告刚刚发生的与目标DoorClosedWhileMoving有关的冲突。这样的工具可以极大地帮助指出缺陷,但是,当然,不能提供任何保证模型没有不期望的行为:这就是为什么动画师和早期分析器是互补的工具。用于监测的算法详见[19]。正如其设计为了按比例放大,它不限于动画,也可以在实际系统中的运行时部署。6讨论和结论FAUST工具箱的目的是在早期阶段实现形式化保证,同时避免形式化方法应用的障碍和隐藏-252C. Ponsard等人/理论计算机科学电子笔记133(2005)237尽可能多的符号。KAOS方法论在电信、钢铁、新闻出版等不同领域的工业案例中已经应用了十多年。典型的需求文档范围从几十个到几百个目标,并通过对象工具(KAOS CASE工具)成功管理[18]。FAUST工具箱现在扩展了该工具的关键功能,用于分析关键任务系统。紧密集成允许分析人员仅在需要的时候和需要的地方以增量的方式进行正式化,使正式部分保持较小且易于管理。在半形式化层面上对模式的识别也会有所帮助,因为它们的形式化可以被一次性证明本文中的示例摘自一个大型铁路信号规范,其中包括比利时铁路公司在更换大量平交道口过程中输入的平交道口模型。最初的工作文档是基于通过状态机图的在一些附件中。我们的方法展示了如何从这些属性开始指导需求文档的细化,然后生成满足这些属性的状态机。早期分析仪还显示了在空气传输控制中关于空气冷凝检测的推理的有希望的结果。目标模型由200多个概念(目标、需求、冲突和障碍)组成,其中一个子集以增量方式形式化,首先不考虑时间方面的推理,然后引入实时约束,最后考虑代理负载。重复出现的特定领域模式的发现也有助于结构化和形式化过程。现在考虑在同一个域中使用Monitor和Animator对空中交通数据进行分类,以检测一些事件和未遂事件并将其可视化。在未来,早期的分析器将被扩展到支持解决障碍和冲突的检查AnimatorMapping也正在改进,一个用于设计控制面板(如火车/飞机/自动驾驶舱)的新组件验收测试生成器和障碍生成器等其他工具正在实施阶段或正在规划中。引用[1] A. Cimatti,E.Clarke,E.Giunchiglia,F.Giunchiglia,M.Pistore,M.罗韦里河阿斯塔纳,和A. Tacchella,Nusmv版本2:一个符号模型检查的开源工具,Int。Conf. 计算机辅助核查(CAV02,LNCS 2404),丹麦,2002年7月C. Ponsard等人/理论计算机科学电子笔记133(2005)237253[2] Anne Dardenne,Axel van Lamsweerde,and Stephen Fickas,Goal-directed requirementsacquisition,Science of Computer Programming20(1993),no. 1-2,3-50.[3] R. Darimont和A. van Lamsweerde,目标驱动需求细化的形式化细化模式,FSE-4 - 4th ACMSymp.软件工程的基础,旧金山,1996年10月。[4] 史蒂夫伊斯特布鲁克,罗宾R。陈晓,应用形式化方法进行需求建模的经验,北京:软件工程出版社,1998年。[5] Standish Group,http://www.standishgroup.com/chaos,1995年。[6] 欧洲软件研究所,欧洲用户调查分析,usv eyr 2.1 espiti项目报告,1996年1月。[7] D. Jackson , Automating first-order relational logic , ACM SIGSOFT in Proc. Conf.Foundations of Software Engineering,2000年11月。[8] R.李国忠,时间逻辑与时间关键系统,国立成功大学计算机科学研究所硕士论文,1992年。[9] E. Letier和A. van Lamsweerde,面向目标的需求细化的基于Agent的策略,2001。[10] E. Letier和A.van Lamsweerde,从系统目标导出操作软件规范,FSE软件工程的基础,查尔斯顿,2002年11月。[11] N.G. Leveson,Safeware,系统安全和计算机,Addison-Wesley,1995年。[12] R. R. Lutz,分析安全关键嵌入式系统中的软件需求错误,IEEE国际需求工程研讨会(加利福尼亚州圣地亚哥),IEEE计算机协会出版社,1993年,第100页。126比133[13] Je Magee,Nat Pryce,Dimitra Giannakopoulou和Je Kramer,行为模型的图形动画,国际软件工程会议,2000年,第100页。499-508[14] Z. Manna和A.林志玲,等.反应式系统的反应行为.北京:计算机科学出版社,1992.[15] J. McLean和C.高可靠性计算机系统:研究议程,信息时代的美国,国家科学技术委员会信息和通信论坛委员会,贝塞斯达,1995年。[16] T. Muller,Promoting constraints to first-class status,First International Conference onComputational Logic(CL00,LNAI 1861),London UK,July 2000.[17] 李文,“系统工程中的形式化方法”,北京:计算机科学出版社,2000年11月,第100页。95比96[18] Objectiver工具,http://wwww.objectiver.com。[19] H. Tran Van,A. van Lamsweerde、P. Massonet和C. Ponsard,面向目标的需求动画,第12届IEEE国际需求工程会议,京都(日本),2004年9月,接受。[20] A. Van Lamsweerde,Goal-oriented Requirements Engineering:A Guided Tour,2001.[21] A. 范拉姆斯韦尔德河Darimont和E.1998年,李捷,管理目标驱动需求工程中的冲突,IEEE软件工程学报,管理软件开发中的不一致性特刊。[22] A. van Lamsweerde和E.李明,面向目标的需求工程中的障碍处理,IEEE软件工程学报,异常处理特刊26(2000),第10期。10个。254C. Ponsard等人/理论计算机科学电子笔记133(2005)237[23] A. van Lamsweerde和E. 从面向对象到目标导向:需求工程的范式转换,软件系统工程的根本创新,Montery'02研讨会,威尼斯(意大利),LNCS,2003年[24] Axel van Lamsweerde,2000年的需求工程:一个研究视角,国际软件工程会议,2000年,pp.5-19
下载后可阅读完整内容,剩余1页未读,立即下载
cpongm
- 粉丝: 5
- 资源: 2万+
上传资源 快速赚钱
- 我的内容管理 展开
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
最新资源
- C++多态实现机制详解:虚函数与早期绑定
- Java多线程与异常处理详解
- 校园导游系统:无向图实现最短路径探索
- SQL2005彻底删除指南:避免重装失败
- GTD时间管理法:提升效率与组织生活的关键
- Python进制转换全攻略:从10进制到16进制
- 商丘物流业区位优势探究:发展战略与机遇
- C语言实训:简单计算器程序设计
- Oracle SQL命令大全:用户管理、权限操作与查询
- Struts2配置详解与示例
- C#编程规范与最佳实践
- C语言面试常见问题解析
- 超声波测距技术详解:电路与程序设计
- 反激开关电源设计:UC3844与TL431优化稳压
- Cisco路由器配置全攻略
- SQLServer 2005 CTE递归教程:创建员工层级结构
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功