论文部分内容阅读
统一建模语言（UML）所建立的模型的正确性无法通过其本身进行形式化验证，为解决这个问题，根据UML模型的静态性质和动态模块行为两个方面提出结合形式化规格说明语言的模型形式化方案，以此为基础提出将UML目标模型转化为Z规格说明的形式化方法，并用Z-EVES工具形式化检测Z规格描述的正确性。通过实例分析验证了该方法的可行性。