基于B方法的软件建模

《基于B方法的软件建模》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、基于BMethod的软件建模方法研究提纲研究背景和国内外研究现状1研究定位与研究意义2本论文研究内容、创新点3案例实现42021/7/19研究背景与现状研究背景需求规格说明与需求管理的缺陷是软件开发中常见的两类问题；当前流行的统一建模语言UML，被OMG采纳并作为工业标准，但缺乏精确的形式语义和严格的推理机制，它使用图形化的建模语言所描述的软件需求很难进行动态分析与验证；形式化方法建立在严格数学基础之上，能产生严密、精确、无二义性的形式规约，可进行模型验证与定理证明，与UML具有互补性；研究现状对于一些较成熟的基于模型的形式化方法，如VDM、Z、B等，在强大工具支持下，在欧美各

2、国家得到成功应用，特别是安全攸关领域；国内基于转换法的UML模型到形式化B模型的转换，目前还没有定义一套标准的映射规则。2021/7/19存在问题2021/7/19研究定位及意义研究定位为提高从软件需求分析阶段起的模型精确性，用形式化的方法弥补半形式化的统一建模语言（UML）的语义缺陷部分，采用基于转换法定义二者的映射规则，将二者结合的方法用于软件建模过程。研究意义采用形式化方法描述软件规范，可以提高软件系统的精确性、可靠性与开发效率，从而提高软件开发质量；形式化B方法在强大工具Atelier-B的支持下，能够对建模结果进行正确性分析与一致性验证，保证后续软件开发过程的精确、可

3、靠性。2021/7/19研究内容及创新点1为建立精确、一致、可验证的系统模型，将半形式化的统一建模语言（UML）与形式化B方法结合；2为增强实时系统的实时性、可靠性，通过UML自身扩展机制对UML中的动态行为模型进行时间扩展；3基于转换法，定义UML模型图到形式化B模型转换的映射规则，主要包括类图、扩展后的状态图以及顺序图；2021/7/19基于转换的方法，将半形式化的UML模型图转换为具有精确语义定义的形式化B模型，其优点：B方法几乎可以用于软件开发的全过程，有强大工具支持，能够对形式规约进行动态分析与一致性检测，有助于实现、提高软件可靠性；UML模型作为B形式规约的起点，降

4、低了直接使用形式化方法描述目标系统的难度，扩展了形式化方法在软件建模中的实际使用度。1、UML与形式化B方法的结合2021/7/19研究内容形式验证器逐步求精的方法自动生成代码根据形式规范自动生成测试最终产品用户需求高层形式规范形式验证器系统特性系统模型系统特性正确/错误？正确/错误？需求分析设计编码测试系统模型形式化软件工程方法形式化方法：形式规约形式验证2021/7/19随计算机技术的发展，实时系统领域的研究呈现出突飞猛跃的态势，时间约束的作用便显得尤为重要；状态图（StateDiagram）：{State，Event，Trisition}；使用UML的自身扩展机制-”构造

5、型”对UML状态图进行时间扩展；新增事件构造型具体说明超时事件：To某状态保持稳定时间，超时后，系统迁移到另一状态；操作的延迟时间：Td迁移中附带的操作时间不能为0；受时钟约束的迁移：Tc时钟约束也是迁移的约束条件，迁移发生在某时间段；周期事件：Tp某些操作周期性执行或事件、迁移在状态图中周期性发生；2、UML状态图的时间扩展2021/7/192、UML状态图的时间扩展经过时间扩展的状态图，其状态迁移就由两类事件共同触发：一类是由状态图表示的对象外部输入事件；一类是在对象运行时，内部时钟所触发的时钟事件。带有时钟扩展后的状态图的迁移过程用一个状态迁移矩阵表示：sStatetSt

6、ateOEventTEventS0***Si…*………**sState:表示源状态OEvent：表示触发状态迁移的外部输入事件或动作TEvent:表示触发状态迁移的时钟事件tState：表示目标状态2021/7/19UML状态图的B形式化定义UML状态图到B抽象机符号语言（AMN）的映射规则，如下：UML状态图B的AMN表示S0:实例对象初始状态S：除初始状态外的所有状态集合SETS//分别建立对应的有限集合；S0={…}S={…}定义相应的变量、并满足其不变式规则初始状态的初始值机器的初始值INITIALISATION定义状态迁移过程：基本状态图迁移层次状态图迁移并发状态图迁

7、移OPERATIONS//通过操作完成GSL在监控条件或不变式规则满足的前提下，事件发生后，实例对象上的状态发生迁移。E（OE/TE）=//事件发生PREP//满足一定前提条件THENS//完成状态迁移行为END2021/7/19UML状态图的B形式化UML状态图迁移过程的B形式化描述—通过定义UML状态图到B抽象机符号（AMN）的映射规则实现基本状态图—没有子结构；BAMN表述S1S1’……Si’……SiE（OE,TE）[cond1]act1E（OE,TE）[condi]actiSETSS