In this paper, a formal method for specifying and verifying concurrent and distributed systems is presented. The formal method has adapted and extended the recent research results in integrating Petri nets with algebraic specifications, and offers new techniques for specification construction and analysis. The new results are illustrated through the specification and verification of a simplified lift system.
