Formal Verification of UML Statecharts using the LOTOS Formal Language

UML is a standard modeling language in software engineering. Although this language is capable of describing and modeling different aspects of a problem, it cannot be used for verification of the obtained model. Formal languages can be utilized for this purpose to verify the model. In a previous study by the authors of this paper, Statecharts diagram has been mapped to the LOTOS formal language. However, not all possible structures and necessary relations like the condition and loop structures were mapped. In this paper, an improvement of the previous method is presented. Moreover, for verification of the presented mapping, the CADP toolbox has been used. To apply the proposed method in practice, a case study is presented, where the properties deadlock, live lock, unreachable states, and non-deterministic states are formally verified. The results of the model verification show that the evaluated statecharts diagram has had deadlocks, but there have not been live locks, unreachable states, or non-deterministic states in it.

Keywords:

UML Statecharts diagram , model verification , CADP , LOTOS ,