论文研究 基于时序逻辑的业务过程约束建模及验证.pdf

提出一种可视化的约束规则建模语言(visual constraint modeling language， VCML)，采用XYZ/E语言作为逻辑框架，统一定义约束规则和业务过程两种模型的形式化语义，为约束规则的自动验证提供形式化基础；然后基于模型检验(model checking)技术，简要讨论模型自动验证的实现方法；最后通过一个应用实例说明业务过程约束的建模。