Equational reasoning about LOTOS specifications: a rewriting approach

摘要

An equational approach is given to the verification of concurrent systems specified in the ISO specification language LOTOS. The approach is based on term rewriting techniques. The kind of reasoning and verification strategies which can be performed are illustrated through two examples.