论文部分内容阅读
本文以LOTOS为基础，简介了LOTOS进程代数的概念和算子。同时，以事件结构作为进程代数的语义模型，充分展示了形式化方法是如何对一个复杂系统进行静态或动态刻画。本文最后以上述理论为基础．开发出一款辅助软件工具。该软件具有两方面的用途：一是能对给定的一个LOTOS语言层次上的系统刻画，自动生成结构层次上的系统模型；二是进行等价性模型检测。此工具将形式化方法的推理过程可视化、实用化。