UML类模型的VDM++形式化规约

摘要

利用目前使用最为广泛的形式化验证语言VDM++在描述系统模型的语法和语义上的精确、一致的特点,结合VDMTOOLS和Rational Rose工具把UML类模型中的各个元素转化成VDM++表示,从而实现对UML类模型中所包含的各个元素进行语法和语义的检查。进一步提高UML的建模质量。