程勇[1]2002年在《基于场景和形式化方法的软件需求建模研究》文中研究表明信息时代的今天，信息技术(Information Technology，IT)产业已成为推动世界经济增长的主要动力之一。随着计算机硬件技术的不断成熟，产业竞争正逐渐转向软件开发领域。软件开发实践表明：用户需求是软件系统成功的关键。本文主要研究软件需求建模问题，其主要思想是：软件需求必须反映市场和用户的真实需要，这是开发新软件系统的基础。因此在需求建模初期采用场景概念来获取用户需求，在后期采用形式化方法加以描述。这样，具有形式化特点的需求规约说明为软件系统的后期开发奠定了坚实的基础。 具体来说，本文主要研究如下问题： (1)软件需求建模。论文采用场景概念来获取用户需求，并用Use Case Maps和Use Case相结合进行表示。 (2)软件需求形式化。基于Use Case Maps的软件系统全局行为模式，可转换为基于SDL表示的软件需求规约说明，这样的需求规约说明具有形式化的特点。 (3)需求规约的确认与验证。本文主要采用支持SDL语言的工具来进行需求的确认和验证。 本文主要贡献在于定义了一个基于UCM和SDL的软件需求描述模型，讨论了整个建模过程，并基于该方法描述了自动柜员机系统需求。另外，本文介绍了如何使用Telelogic Tau工具集确认和验证SDL规约说明以及将来进一步研究的方向。
郑宇恒[2]2009年在《基于场景的需求建模研究》文中认为随着软件工程的发展,需求工程日益得到人们的重视。需求分析作为软件生命周期极为重要的一个环节,关系到软件工程项目的成功与否,并且在很大程度上决定了软件产品的质量。本文主要研究软件需求建模问题,其主要思想是:软件需求必须反映市场和用户的真实需要。在需求建模的初期采用场景概念来获取用户需求,在后期则采用形式化方法加以描述。这样,具有形式化特点的需求规约说明为软件系统的后期开发奠定了坚实的基础。具体来说,本文主要简要讨论了场景和形式化方法的相关知识。详细介绍了一种新的场景表示法IA--UCM。对于形式化方法主要介绍了有关概念、分类、形式规约语言、使用现状和评价、基于形式化方法的软件开发过程等。最后还简要综述了两种标准形式化描述技术,即消息序列图(MSC)和接口自动机,然后将流体变量引入消息序列图和接口自动机,介绍了带注释的消息序列图和带注释的接口自动机。提出一种基于接口自动机的软件需求建模方法的全部过程,重点讨论了如何获取需求,并如何将捕获的需求进行形式化以及软件需求规约的确认与验证等问题本文定义了一个基于UCM和接口自动机的软件需求描述模型,讨论了整个建模过程,并基于该方法描述了自动柜员机系统需求。另外,本文还介绍了如何使用带注释的消息序列图和带注释的接口自动机确认和验证接口自动机以及将来进一步研究的方向。
张晓春[3]2007年在《基于用户场景的需求引出及其行为建模技术研究》文中指出随着软件工程学科的发展,需求工程日益得到人们的重视。需求分析作为软件生命周期极为重要的一个环节,关系到软件工程项目的成功与否,并且在很大程度上决定了软件产品的质量。因此,如何有效地捕获用户的真正需求已经成为软件工程学科研究的重点。场景被认为是引出、文档化和验证需求的较为有效的工具,其支持非形式化、叙述性和具体化的描述,关注用户与软件环境交互的动态特性,因而参与需求分析过程的实践者和用户都能很容易地使用场景来表达其对需求的理解,以达到最佳的交互状态,从而更好地获取用户需求。这样,通过让用户真正地参与到需求分析的过程中,可以更好地将应用领域问题映射到计算机领域,并且在需求获取的迭代过程中可以自动地适应系统需求的不断变化,避免了由于需求变更而导致的系统体系结构的改变,同时也能及时添加新的需求或修改已有的不符合用户实际需要的场景,有利于保证应用软件开发的正确性及完整性。由于在开始阶段得到的是对场景的非形式化描述,而作为工程目标的软件系统是由程序及其运行环境组成,二者不仅从内容到形式都存在巨大的差别。为此,需要在它们之间建立起映射,使得程序能够正确建模用户的需求。传统的结构化方法将软件系统视为数据加工的过程,其利用功能分解的办法将系统分为不同的功能模块,每个模块进行一个子加工。虽然结构化方法曾经是软件工程实践中的主流技术,并且至今仍具有重要的影响,但是随着现代软件系统日趋复杂,各组件之间具有的各种动态交互关系以及需求的不断演化,使结构化方法愈发难以胜任。因此,如何归纳出系统的功能以及各个组件和外部参与者之间的交互就成为工程实践的中心任务。如果能够据此合成出系统的状态模型并生成代码框架,将有助于提高软件质量及降低成本。对于传统的分析方法来说,需要运用非形式化的手段,发挥创造型思维来分析用户的需求。在这个过程中,对于不同用户和分析人员,由于各自不同的工作领域和思维模式,他们之间存在着交流上的障碍,造成得到的需求难以正确和完整。如何与用户交流以得到其真正需求也成为一个重要环节。根据以上构思,首先由用户提交目标系统的初始期望场景集和例外场景集;然后生成全局系统的状态图,在此过程中不断检验出隐含的期望场景和例外场景,并辅助状态图的合成,最终完成从用户提交的场景描述到利用形式化方法建立需求模型的过程。在这个过程中介绍了目前流行的形式化建模方法的基本概念,并着重描述了本篇实例中所用到自动机理论及相关技术。为了研究从场景需求规约得到系统功能规约的步骤,本篇将通过建模一个手机短信服务系统宋阐述基于MSC(Message Sequence Chart)-场景的需求引出过程。为了得到形式化的功能规约,需要由用户输入的场景合成出前缀树识别器(Prefix Tree Acceptor),即根据对场景的描述画出MSC,遍历MSC的消息得到若干个事件序列的集合,然后将多个事件序列在具有共同前缀的地方连接起来。由于前缀树识别器是直接根据用户场景的事件序列转换而来的,没有很好地揭示若干事件和状态之间的本质联系,并且包含大量的冗余状态,所以需要对这些状态进行合并。合并状态后的系统可能接受更多的事件序列,然后将这些新产生的序列提交给用户判断:目标系统中能否出现这样的事件序列,并根据得到的回答来辅助合并的过程。这个过程类似一个具有负反馈能力的抽象机器,它的控制部件是合并状态的算法,反馈部件是最终用户,系统输入是初始场景集,系统输出是完成状态合并的自动机模型,反馈输入是合并后新接收的事件序列,反馈输出的是最终用户对这个事件序列所作的判断。如果系统合并过多(或过少)的状态,通过反馈就会抑制这个过多(或过少)的合并,使得生成的自动机平稳、渐进地趋向于目标系统。由此就可以把用户场景的形式化过程映射为系统模型的归纳过程。根据合并好的自动机模型,依照映射规则就可以按部就班地编写组件的代码框架。最后利用面向对象的软件设计方法,将每个系统组件封装为一个进程并填充具体代码,从而完成从最初场景到最终代码的整个流程。
陈铭松, 鲍勇翔, 孙海英, 缪炜恺, 陈小红[4]2017年在《基于通信的列车控制系统可信构造:形式化方法综述》文中提出基于通信的列车控制系统(communication based train control system,简称CBTC)已经成为世界范围内建造轨道交通信号系统的标准制式.CBTC采用更加灵活和精确的列车控制,并提供连续的安全列车间隔保证和超速防护,在很大程度上提高了轨道交通运输的效率和安全性.尽管CBTC能够精确地实施实时控制,但由于CBTC涉及计算、通信与控制这3个方面的实时协同,系统设计与实现异常复杂.由设计缺陷而导致严重的灾难、事故和损失屡见不鲜.作为一个典型的安全攸关系统,如何保证CBTC的可信构造已成为领域研发人员关注的焦点与面临的最大挑战.鉴于在软硬件领域的成功经验,形式化方法目前已被公认为是保障CBTC可信性的一种有效方案.围绕CBTC的可信构造,从其生命周期的3个重要阶段,即系统需求分析、设计建模与底层实现入手,针对CBTC在可信方面的典型特征,梳理分析了CBTC系统在可信构造方面面临的挑战、国内外研究现状和发展趋势,全面介绍了形式化方法在CBTC可信构造中扮演的角色.
段建荣[5]2009年在《UML用例模型的B形式化描述方法研究》文中指出随着信息技术的飞速发展,计算机软件系统的应用逐渐扩展到了社会的各个领域。软件规模和复杂度在不断增加,软件出现错误的可能性也随之增加。如何保证软件的质量、提高软件的可靠性,已成为目前软件工程研究领域的一个热点。将形式化方法和主流的软件开发方法相结合是一种可行的方法。UML作为当前比较流行的一种可视化建模语言,已成为面向对象分析和设计中事实上的工业标准。UML模型直观、易懂,利于开发者与用户之间的沟通。但UML的大部分语义是用自然语言描述的,确乏精确的语义,容易产生模糊或歧义;UML缺乏有效的推理机制和完善的模型检查能力,不便于使用工具对其描述的规约进行动态分析和验证。形式化方法则是基于严格数学理论的,能产生精确、无二义性的形式规约,为软件开发提供了严格的数学基础,这对提高软件的可靠性有着非常显着的作用。但形式规约不够直观,可读性较差,不便于与用户进行交流,要求开发者具有良好的数学基础。因此,形式化方法的研究和应用目前仍局限在较小的范围之内。把形式化方法和UML相结合实现优势互补的研究对保证软件质量、提高可靠性有着非常重要的意义。本文选择B方法作为形式规约方法,把UML模型的图形规约映射到B形式规约。一方面,我们能够借助于强大的B方法支持工具,基于相应的B形式规约,对UML建模结果进行正确性分析和一致性检查;另一方面,可将UML规约作为形式化开发的基础,降低直接使用B方法建立形式规约的难度,增强B方法在软件开发中的实际作用。本文以UML用例模型为主要研究对象,在分析UML用例模型概念和B抽象机符号的基础上,对用例模型建模元素的抽象语法进行描述,建立两者之间的映射,实现UML用例模型图到B形式规约的转换。软件开发人员可以首先用半形式化的UML用例模型为目标系统建立需求模型,然后根据文中给出方法构建目标系统的B形式化规约,再利用B方法支持工具对规约进行动态分析和模型验证,得出可靠的形式规约,为在此基础上进行的形式推导和精化提供了正确的起点。最后,通过对电梯控制系统的实例分析,进一步详述了UML用例模型到B方法形式规约的转换方法及过程,并利用B方法的支持工具ProB对所得到的形式化模型进行了动态分析和模型检测。
赵榆琴[6]2008年在《基于领域本体知识和次协调逻辑的非规范需求分析研究》文中进行了进一步梳理尽管当前大多数的软件开发技术和开发环境都视一致性为基本假设,但在软件开发过程中试图强行维护一致性的观点已经受到质疑。在需求工程中的每一阶段试图强行维护绝对一致性不仅受到需求描述本身形式化程度的影响,而且受到维护一致性的计算代价等方面的影响。反之,从软件开发的角度来看,不一致性可以将注意力转移到问题领域,对于不一致性的系统管理,不仅有助于识别不确定的领域,还可以促进开发人员之间的共同理解、交流和合作。特别重要的是可以引导需求获取的过程,改进过程建模以及为需求的有效性和正确性提供检验依据。关于不一致性在软件工程中的普遍性以及对于软件开发的驱动作用已经成为软件工程领域日益关注的研究主题。总的来说,在需求工程中,乃至软件开发过程中,对于不一致性的容忍已经得到一定程度的共识,并且关注的范围从对不一致性的检测逐渐扩展到容忍不一致性的推理研究。领域本体作为一种语义模型描述了特定领域中概念和概念之间的语义关系,而面向对象的需求分析方法是当前软件需求分析方法中比较流行和实用的方法。因此,本文研究了融合本体和面向对象技术的需求表示和获取方法；并对需求分析过程中出现的非规范需求(Non-canonical Requirements)进行了探讨,利用次协调逻辑的理论和方法,针对这些非规范需求建立新的分析模型。本文具体研究内容如下：1)给出需求分析中的非规范知识表示的解决方案；给出了一个非规范需求详细的分类,并对各类非规范需求进行自然语言的描述和形式化定义,使得对非规范需求有一个比较全面和清晰的理解。2)提出了非规范需求的扩展管理框架；借鉴一般意义上的非规范需求管理框架,提出一个基于领域知识、本体库和推理规则的框架,采用六个机制导出改进的需求信息,建立容忍不一致的需求分析模型。3)实现了基于7-值信任半格逻辑的融合本体和面向对象技术的需求获取方式；利用领域本体构建知识模型,并融合本体和面向对象技术提出需求获取方式,利用7-值信任半格逻辑获取非规范需求。4)给出了非规范需求的检测和处理方法；借鉴非规范知识的处理方法,结合各类非规范需求的特点,遵循容忍和改进的基本思想,给出了非规范需求的检测和解决方案。5)利用次协调逻辑的理论和方法,建立容忍不一致需求的分析模型。以领域知识为支撑,利用次协调逻辑的理论方法和面向对象的需求分析方法,建立能够容忍不一致需求存在的需求分析模型。在软件生命周期的需求、设计、编码、测试和维护等各个阶段,需求处于软件工程的开始部分,它提供了构建软件项目其余部分的根基,因而对于软件项目的成败尤为重要。随着面向对象、可视化编程和CASE等软件开发技术的发展和应用,软件设计、编码、测试等环节的技术日益成熟和稳定。而需求工程却由于没有可现成套用的方法而称为一个困难的课题。80年代中期,形成了软件工程的子领域——需求工程(requirements engineering.RE)。从社会系统层次出发,需求工程是系统工程的一个分支,它涉及到软件系统的目标,软件系统提供的服务、和对软件系统的约束；从软件系统层次出发,需求工程提供与软件系统相关的所有用户的显示世界的需要,和软件技术所能提供的能力之间的一个桥梁。人们开始从需求描述、需求获取、需求分析、需求的一致性、需求管理和需求建模等几个方面来研究需求工程,即将传统意义上的需求分析扩展为一整套需求工程的理论和方法。因此目前软件工程学科的重点和难点正逐渐转移到前期的需求阶段,通过对需求工程的研究来解决需求分析涉及到的诸多问题。以往研究需求工程的前提条件是：我们所获得的需求都是确定的、无不一致性的、精确的、甚至是不变的。但是人们逐渐意识到,在需求工程中的每一阶段试图强行维护需求的绝对一致性不仅受到需求描述本身形式化程度的影响,而且受到维护一致性的计算代价等方面的影响。需求不一致性的研究可以引导需求获取的过程,改进过程建模以及为需求的有效性和正确性提供检验依据。即是说,在需求工程中,乃至软件开发过程中,对于不一致性的容忍已经得到一定程度的共识,并且关注的范围从对不一致性的检测逐渐扩展到容忍不一致性的推理研究。因此,在需求工程中,如何看待和处理需求分析中的非规范知识(以下简称为非规范需求)成为热点和难点问题,并且随着知识工程,人工智能和需求工程的不断发展,人们越来越关注需分析中面对的非规范知识。本文借鉴非规范知识的表示和处理方法,将非规范需求视为非规范知识,主要介绍几种针对非规范知识的表示和处理方法,分析了将它们应用于非规范需求可能性和意义。其中特别介绍了次协调逻辑的理论和推理方法,从而使得它特别适合表示和推理非规范需求。本体和面向对象技术是两种知识表示的方法。它们在知识表示方面各有优缺点,本文首先介绍了它们的基本概念、思想和方法,然后对两种方法进行了比较分析,说明了结合两种方法来进行知识表示的可能性和意义。本文从非规范需求的定义、分类、表示、产生原因、管理,处理、检测、度量和评估几个方面介绍了非规范需求在这些方面的已有研究成果,并且分析了这些成果解决了的问题,解决方法的优点和不足之处。最后,本文介绍了将以上的技术方法结合到需求工程的各个阶段来解决需求分析的问题,着重介绍了需求获取和需求分析的方法,并且对当前几种需求工程的技术方法和非技术方法进行了探索和分析。
李宪[7]2012年在《基于UML的列控系统建模方法与验证工具集成》文中认为近年来随着技术的发展,列车运行控制系统的功能不断增强,为实现不同厂商设备间、地面设备与车载设备间互联互通,使列车能够在轨道交通网中跨线安全运行,列控系统需求规范的作用正日益突显。但现有研究成果表明在需求层面对系统的关键属性进行分析和确认面临很多困难,需要提出一种合理的框架结构以对其关键属性进行建模并对系统进行验证。从建模方法来看,统一建模语言(UML)具有定义良好、易于表达、描述直观等优点,已被广泛应用到不同的领域,但当需要对影响列车安全可靠运行的连续和离散过程进行一体化建模时,对混成特性的描述已远远超出了这种建模语言本身的能力范围,这给列控系统需求规范的建模工作带来了巨大的挑战。从验证方法来看,形式化方法已成为保障安全苛求系统的安全性与可靠性的重要手段。针对不同的系统、同一系统的不同性质和系统分析的不同阶段,可供研究人员使用的形式化验证工具种类繁多。因此,本文从列控系统需求规范建模方法与验证工具集成着手进行研究,主要内容包括：1.对列控系统需求规范混成特性建模需求进行分析,研究UML扩展机制,充分挖掘UML的图形功能,设计面向列控系统需求规范的混成UML概要文件,使之能够包含更多的内容与信息去准确地刻画列控系统的混成特性。2.在论述列控系统需求规范的分析方法体系结构的基础上,重点分析了模型验证阶段的功能需求。在Eclipse平台上完成了验证支持工具的软件原型开发,对底层形式化建模过程和验证工具进行封装,通过自动化的模型检验技术来寻找需求中隐藏的错误,使现有的需求管理工具(IBM RequisitePro)、建模工具(IBM Rational Software Architect)和验证工具(NuSMV, PHAVer)实现高度集成,并具备良好的可扩展性。并给出从UML模型到形式化模型的转换规则,构造了面向对象语言UML以及NuSMV、PHAVer形式化语言之间的转换桥梁。3.从列控系统需求规范中选取了具有代表性的模式转换场景和RBC交接场景,利用所提出的混成UML概要文件对场景进行建模;将建好的模式转换场景模型转换为NuSMV模型,而将RBC交接场景模型转换为PHAVer模型；在开发的验证支持工具中完成两个形式化模型的验证分析工作。通过案例分析,证明文中所提出的基于UML扩展机制的列控系统需求规范建模方法的可行性,以及所开发验证支持工具的可用性。
祝义[8]2011年在《嵌入式软件需求规约到软件体系结构模型的转换研究》文中研究说明近年来随着嵌入式系统硬件性能的不断提高,嵌入式系统中软件的规模和复杂性也不断增加,软件对整个系统的影响逐渐占据了统治地位,从而使得嵌入式软件设计以及可靠性保障变得越来越困难。传统的嵌入式软件设计方法已经逐渐难以满足现代嵌入式软件设计的高可靠性需求,必须结合主流软件工程中处理复杂软件系统所采用的理论、技术与方法,如构件化设计、模型驱动架构、形式化规约与验证等。目前,模型驱动的嵌入式软件设计方法已经成为嵌入式计算领域中的研究热点。形式化方法是以数学为基础的用以对系统进行规约、设计和验证的语言、技术和工具的总称。对于具有高可靠性需求的嵌入式软件系统而言,建立有效的形式化验证技术具有非常重要的意义。因此,在嵌入式软件需求规约阶段引入形式化方法,并根据需求规约生成保留形式化语义的软件体系结构模型,可以极大提高嵌入式软件设计的可靠性。本文主要围绕嵌入式软件需求规约到软件体系结构模型转换的问题展开研究。重点研究了需求规约到软件体系结构模型的转换框架、基于MDE的LOTOS规约到UML-RT模型的转换方法、TCSP规约到UML-RT模型的转换方法、支持硬实时分析的进程代数规约与转换、支持资源分析的进程代数规约与转换问题。主要内容如下:(1)针对根据自然语言规约建立的软件体系结构模型的不精确性以及二义性问题,基于已有的自然语言规约到形式化规约的转换工作,提出了嵌入式软件需求规约到软件体系结构模型的转换框架,并在此基础上进一步提出了基于MDE的形式化规约到软件体系结构模型的转换框架。基于转换框架生成的软件体系结构模型保留了形式化语义,能够从本质上提高嵌入式软件软件体系结构设计的可靠性。(2)针对嵌入式软件时序规约到软件体系结构模型的转换问题,提出了基于MDE的LOTOS规约到UML-RT模型的转换方法。UML-RT是OMG组织专门针对实时与嵌入式系统软件体系结构建模的规范,然而基于自然语言规约建立的UML-RT模型往往是不精确的、存在二义性。为了使得UML-RT建模结果更为精确,需要赋予UML-RT模型形式化语义。LOTOS是一种适合于描述与验证嵌入式软件时序规约的进程代数方法。在需求规约到软件体系结构模型的转换框架下,使用LOTOS描述嵌入式软件时序规约,通过建立LOTOS到UML-RT的转换机制,实现了LOTOS规约到UML-RT模型的转换。实例分析表明该方法能够提高嵌入式软件软件体系结构设计的可靠性。(3)针对嵌入式软件实时规约到软件体系结构模型的转换问题,提出了TCSP规约到UML-RT模型的转换方法。时间通信顺序进程TCSP是进程代数通信顺序进程CSP的实时扩展,适合于描述与验证嵌入式软件的实时规约。在需求规约到软件体系结构模型的转换框架下,使用TCSP描述嵌入式软件实时规约,通过建立TCSP到UML-RT的转换机制,实现了TCSP规约到UML-RT模型的转换。实例分析表明通过该方法建立的UML-RT模型能够从整体上提高嵌入式软件软件体系结构设计的可靠性。(4)针对嵌入式软件缺乏有效的硬实时规约与验证机制,研究了支持硬实时分析的进程代数方法。通过扩展进程代数TCSP的硬实时语义,提出了硬时间通信顺序进程HTCSP,使之能够规约与验证嵌入式系统的硬实时动态行为。提出了时间最优调度算法,该算法有助于嵌入式系统硬实时的量化分析和优化设计。进一步给出了HTCSP规约到UML-RT模型的转换方法。(5)针对嵌入式软件缺乏有效的资源规约与验证机制,研究了支持资源分析的进程代数方法。通过扩展进程代数CSP的资源语义,提出了资源通信顺序进程RCSP,使之能够规约与验证嵌入式系统包含多种资源信息的动态行为。提出了资源优化检查算法,检查结果有助于嵌入式系统资源的量化分析和优化设计。最后讨论了RCSP规约到软件体系结构模型的转换方法。
梁云涛[9]2017年在《基于COMET的西部铁路列控系统RBC信息控制流程设计与验证》文中研究指明随着"一带一路"战略的推进以及我国中东部地区铁路网的不断完善,西部地区将迎来铁路发展的黄金时期。CTCS-LDL(Chinese Train Control System-Low Density Lines)级列控系统是针对我国西部地区低密度线路运营需求而研发的新型列控系统,目前该系统处于理论探索阶段。为降低运营成本,减少或免于地面设备维护,CTCS-LDL级列控系统使用GNSS技术实现列车定位及完整性检查,地面不设区间轨道电路和信号机,采用虚拟闭塞方式实现列车追踪,这样对地面设备的安全性和可靠性提出了更高的要求。无线闭塞中心(RBC)是CTCS-LDL级列控系统的地面核心设备,主要通过与车载及地面其他设备间的信息交互,实现虚拟轨道占用检查与区间闭塞管理,完成行车控制,因此设计合理的RBC信息控制流程是保证西部铁路列控系统安全行车的基础。通过分析我国低密度线路列控系统的运营需求,本论文将RBC信息控制流程分为地面信息控制流程与控车流程,对其进行设计、建模与验证。论文完成的主要工作如下:首先,通过比较基于 UML 的 COMET(Collaborative Object Modeling and Architectural Design Method)建模方法与基于时间自动机理论的形式化建模方法的优缺点,将二者结合,提出针对RBC的COMET软件建模与验证方法,该方法涵盖了软件开发周期中需求分析、软件建模、模型验证、架构设计、软件编码这一集成化过程。然后,对RBC系统进行功能需求分析,设计系统总体结构模型,将RBC信息控制流程分为地面信息控制流程和控车流程。地面信息控制流程包括轨道占用识别、区间信号点灯和区间改方;控车流程根据运行场景主要分为设备启动、列车注册、正常行车、列车注销、调车、RBC切换等。对上述流程进行详细设计,并建立COMET动态交互模型,再通过转换算法将其转换为时间自动机网络模型。结合RBC系统的功能需求,利用模型验证工具UPPAAL对建立的模型进行仿真,并从逻辑功能、时序功能和安全性的角度对模型进行分析验证。最后,根据建立的RBC信息控制模型,采用COMET分层抽象的软件体系架构,进行仿真软件设计并完成软件开发。通过实验室仿真联调,验证了本文设计的CTCS-LDL级列控系统中RBC信息控制流程的正确性和合理性。
罗浩[10]2007年在《形式化与可视化相结合的嵌入式实时软件建模和验证》文中研究说明随着硬件设备计算能力的迅速提高以及社会需求的不断变化和增长,嵌入式系统变得越来越复杂,这对嵌入式实时软件开发的各个阶段(从系统分析、设计到实现、验证)均带来了新的困难和挑战。为了保障嵌入式实时软件的实时性、安全性和可靠性等,本文将基于UML的建模方法与形式化建模方法相结合,为嵌入式实时软件的建模和验证提供一种解决方案。UML2.0顺序图是UML的中描述能力最强的视图之一,它着重体现对象间动态的交互关系,并且还具有良好的易理解性。但是UML2.0顺序图用来对嵌入式实时软件建模和验证还存在时间描述方面不足之处。因此提出一种利用UML的扩展机制对UML2.0顺序图进行扩展的方法。扩展后的UML2.0顺序图不但能够很好的保持原来的易理解性,而且能够清晰的描述嵌入式实时软件的时间需求。根据扩展后UML2.0顺序图与时间自动机的语义,提出一种将扩展后UML 2.0顺序图转换成时间自动机的方法,从而将UML 2.0顺序图与时间自动机结合起来,利用UML2.0顺序图对嵌入式实时软件建模,转换成时间自动机后利用工具加以验证。最后通过对一个电梯管理系统建模和验证,把本文提出的结合思想运用到实例系统的验证当中。本文的研究对嵌入式实时软件建模和验证、UML2.0顺序图的应用和形式化方法在软件验证过程中的使用都有一定的推动作用。
参考文献：
[1]. 基于场景和形式化方法的软件需求建模研究[D]. 程勇. 合肥工业大学. 2002
[2]. 基于场景的需求建模研究[D]. 郑宇恒. 浙江师范大学. 2009
[3]. 基于用户场景的需求引出及其行为建模技术研究[D]. 张晓春. 浙江师范大学. 2007
[4]. 基于通信的列车控制系统可信构造:形式化方法综述[J]. 陈铭松, 鲍勇翔, 孙海英, 缪炜恺, 陈小红. 软件学报. 2017
[5]. UML用例模型的B形式化描述方法研究[D]. 段建荣. 西安科技大学. 2009
[6]. 基于领域本体知识和次协调逻辑的非规范需求分析研究[D]. 赵榆琴. 云南师范大学. 2008
[7]. 基于UML的列控系统建模方法与验证工具集成[D]. 李宪. 北京交通大学. 2012
[8]. 嵌入式软件需求规约到软件体系结构模型的转换研究[D]. 祝义. 南京航空航天大学. 2011
[9]. 基于COMET的西部铁路列控系统RBC信息控制流程设计与验证[D]. 梁云涛. 北京交通大学. 2017
[10]. 形式化与可视化相结合的嵌入式实时软件建模和验证[D]. 罗浩. 苏州大学. 2007
标签：计算机软件及计算机应用论文; 自动机论文; 嵌入式软件论文; 形式化方法论文; 软件需求分析论文; 软件过程模型论文; 软件体系结构论文; 面向对象分析与设计论文; uml建模工具论文; 用户需求分析论文; 建模软件论文; 用户研究论文; 嵌入式系统设计论文; 实时系统论文; 工程信息论文; 软件开发流程论文; 软件开发模型论文; 用户分析论文; 软件过程论文; 一致性检验论文; 嵌入式论文;