基于B方法的软件建模.ppt

基于BMethod的软件建模方法研究,2019/11/27,提纲,2019/11/27,研究背景与现状,研究背景需求规格说明与需求管理的缺陷是软件开发中常见的两类问题；当前流行的统一建模语言UML，被OMG采纳并作为工业标准，但缺乏精确的形式语义和严格的推理机制，它使用图形化的建模语言所描述的软件需求很难进行动态分析与验证；形式化方法建立在严格数学基础之上，能产生严密、精确、无二义性的形式规约，可进行模型验证与定理证明，与UML具有互补性；研究现状对于一些较成熟的基于模型的形式化方法，如VDM、Z、B等，在强大工具支持下，在欧美各国家得到成功应用，特别是安全攸关领域；国内基于转换法的UML模型到形式化B模型的转换，目前还没有定义一套标准的映射规则。,2019/11/27,存在问题,2019/11/27,研究定位及意义,研究定位为提高从软件需求分析阶段起的模型精确性，用形式化的方法弥补半形式化的统一建模语言（UML）的语义缺陷部分，采用基于转换法定义二者的映射规则，将二者结合的方法用于软件建模过程。研究意义采用形式化方法描述软件规范，可以提高软件系统的精确性、可靠性与开发效率，从而提高软件开发质量；形式化B方法在强大工具Atelier-B的支持下，能够对建模结果进行正确性分析与一致性验证，保证后续软件开发过程的精确、可靠性。,2019/11/27,研究内容及创新点,2019/11/27,基于转换的方法，将半形式化的UML模型图转换为具有精确语义定义的形式化B模型，其优点：B方法几乎可以用于软件开发的全过程，有强大工具支持，能够对形式规约进行动态分析与一致性检测，有助于实现、提高软件可靠性；UML模型作为B形式规约的起点，降低了直接使用形式化方法描述目标系统的难度，扩展了形式化方法在软件建模中的实际使用度。,1、UML与形式化B方法的结合,2019/11/27,研究内容,形式化软件工程方法,形式化方法：形式规约形式验证,2019/11/27,随计算机技术的发展，实时系统领域的研究呈现出突飞猛跃的态势，时间约束的作用便显得尤为重要；状态图（StateDiagram）：State，Event，Trisition；使用UML的自身扩展机制-”构造型”对UML状态图进行时间扩展；,2、UML状态图的时间扩展,2019/11/27,2、UML状态图的时间扩展,经过时间扩展的状态图，其状态迁移就由两类事件共同触发：一类是由状态图表示的对象外部输入事件；一类是在对象运行时，内部时钟所触发的时钟事件。,带有时钟扩展后的状态图的迁移过程用一个状态迁移矩阵表示：,sState:表示源状态OEvent：表示触发状态迁移的外部输入事件或动作TEvent:表示触发状态迁移的时钟事件tState：表示目标状态,2019/11/27,UML状态图的B形式化,定义UML状态图到B抽象机符号语言（AMN）的映射规则，如下：,2019/11/27,UML状态图的B形式化,UML状态图迁移过程的B形式化描述通过定义UML状态图到B抽象机符号（AMN）的映射规则实现基本状态图没有子结构；,BAMN表述,2019/11/27,UML状态图的B形式化,UML层次状态图是一种顺序复合状态（超状态），包含一个或多个不相交的子状态；,E,2019/11/27,UML状态图的B形式化,并发状态图也是一种复合状态，可分解为两个或多个并发子状态；,.,.,2019/11/27,UML类图的B形式化,MACHINEClassNameSETSCLASS.VARIABLESattribute1,attribute2,INVARIANTattribute1classClassNameType.INITIALISATIONattribute1=.,.OPERATIONS.PREPTHENSENDEND,类图是对系统静态结构的描述，以下定义了类图中类、类之间关系以及关联关系的多重性的B映射规则：,2019/11/27,UML类图的B形式化映射规则,二者都对数据和操作进行了封装，各个机器之间也存在一定的关系。具体给出了以下对应的映射规则：,2019/11/27,UML类之间的主要关系：,UML类图的B形式化映射规则,关联关系是非常重要的一种关系，B方法中的函数在语义上与关联的多重性存在某些关系，在BAMN中，我们将关联描述成一个变量，定义关联变量时，主要根据关联多重性来确定函数的类型。,2019/11/27,UML类图的B形式化映射规则,关联的多重性与B方法函数的对应关系,2019/11/27,矿井水泵控制系统（MPCS）,案例实现,矿井水泵控制系统属于实时控制系统的一个典型案例；,2019/11/27,MPCS系统类图,系统中的UML类图主要包括：甲烷触感器类（MethaneSensor）、水位传感器类(WaterSensor)、用户接口类(Interface)、水泵类(Pump)及控制器类(Controller)。,2019/11/27,MPCS系统中类图的B形式化规范（部分规约代码）,MPCS系统类图B规约,2019/11/27,MPCS系统状态图,控制器（Controller）状态图,水泵（Pump）状态图,系统中控制器与水泵的状态图,2019/11/27,MPCS系统中状态图图的B形式化规范（部分规约代码）,MPCS系统状态图B规约,2019/11/27,MPCS系统总体结构,MPCS系统结构,2019/11/27,MPCS系统模型的验证,借助B支持工具Atelier-B，对所建模型进行内部一致性检查与义务证明；,2019/11/27,MPCS系统模型的验证,2019/11/27,MPCS系统模型的精化与实现,B抽象机模型精化与实现的目的：弱化前置条件与选择，引进程序设计的典型控制结构，使形式规约更接近计算机识别的程序代码。,2019/11/27,对统一建模语言（UnitedModelingLanguage，UML）的动态行为语义进行了时间上的扩展；定义了UML静态模型与动态模型到形