摘要
将UML(统一建模语言)图形转换成形式化规范是一种精确化UML语义、扩大形式化软件方法适用范围的有效途径.PVS是一种通用高阶逻辑形式化规范语言,具有很强的描述能力以及丰富的定理证明、模型验证工具支持.本文论证了使用.PVS来对UML进行形式化的优势,并且给出了UML的状态图到PVS规范的转换模型与规则.
Formalizing UML diagrams is an effective way to get a precise UML semantics and extend the usage of formal meth-ods.PVS is a higher-order logic based general formal specification langugae with strong expressiveness and foraml analysis tools support. By compring with other formal methods,the advantages of PVS are given in formalizing UML. A hierarchical automata model and algorithms are provided for transforming UML Statechart to PVS specification.
出处
《电子学报》
EI
CAS
CSCD
北大核心
2002年第12A期2122-2125,共4页
Acta Electronica Sinica
基金
国家自然科学基金(No.69973032)