Comparison of Software Specification Methods Using a Case Study

Numerous formal specification methods have been proposed in the literature, such as the Z language, the Unified Modeling Language (UML), the B method, Petri nets, and action systems. Comparing the different specification methods is not an easy task but it is meaningful in many aspects. In this paper, we discuss the properties of five formal specification methods theoretically and address their differences by designing a particular part of the ABM system using each method, and further compare these methods by analyzing their strengths and weaknesses.