基于UML与PVS的严格建模技术研究----嵌入式实时系统的严格建模

摘要

该文在已有研究基础上提出了一种新方法用于嵌入式实时系统的严格建模.该文通过构造面向对象语言UML与形式化方法PVS之间的转换桥梁,为嵌入式实时系统开发团队提供了一个易用、可以实现模型阶段验证的软件方法.该团队包括UML建模人员以及形式化验证人员,UML建模人员首先使用一种带有扩展的UML子集对系统建立图形表示的最初模型,然后使用转换工具实现UML图形到PVS规范语言的转换,形式化验证人员使用PVS验证工具对规范进行验证,达到严格建模的目的.在UML建模方面,该文提出了使用类图以及带有时间扩展的状态图分别对系统的静态、动态模型建模的策略,可以比较完整地表达模型的内容,同时又有利于到形式化规范的转换.该文选用PVS作为支持的形式化工具,PVS是一种通用的形式化方法,提供基于高阶逻辑的规范语言,具有很强的描述能力,可实现对静态、动态模型的描述;它集成了模型验证(Model Checking)、定律证明(Theorem Proving)的工具支持,验证能力强.该文对这种软件方法的几个核心问题进行深入讨论,为该方法的设计提供理论依据.它包括两个部分:类图到PVS规范语言的转换,带有时间约束状态图到PVS规范语言的转换以及验证.