Automatic verification of uml state chart by bogor model checking tool Automatic formal verification of network and distributed systems

Validation and verification of software or system specifications are crucial in reducing costs and proper software development. Software specifications are usually represented bysemi-formal languages like UML. For verification of non-formal and semi-formal models, they should be first transformed into aformal language. The state chart is one of the well-known UML charts that describe the behavior of a system and used formodeling many systems such as resource managements andcommunications in networks or distributed systems. In this paper, we propose a method to automatically map a UML statechart to BIR language, which is designed for BOGOR model checking. The goal of the verification in this paper is to evaluatethe deadlock property of this chart. The proposed method is evaluated by four case studies of ATM and Fax machine statecharts and the model is verified regarding the existence of adeadlock. Results indicate that while the PAT verification tool cannot properly recognize deadlocks in a state chart, theproposed approach is capable of detecting such cases of a deadlock.

Keywords:

Automation Model Checking , UML State Machine , BOGOR , PAT , Dead Lock