Comparative study of formal specifications through a case study

Numerous formal specification methods have been proposed in the literature, i.e., the Z language, the unified modeling language (UML), the B method, Petri nets, action systems, the language of temporal ordering specification (LOTOS), and the specification and description language (SDL). Comparing the different specification methods is not an easy task but it is meaningful in many aspects. In [1], we discussed and compared the properties of five formal specification methods by designing a particular part of the ABM system for each method. Continuing our work, in this paper, we discuss another two formal specification methods, SDL and LOTOS, by emphasizing some similarities among them and address their differences based on a particular part of the ABM system, and further compare these methods by analyzing their strengths and weaknesses.