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 by semi-formal languages like UML. For verification of non-formal and semi-formal models, they should be first transformed into a formal language. The state chart is one of the well-known UML charts that describe the behavior of a system and used for modeling many systems such as resource managements and communications in networks or distributed systems. In this paper, we propose a method to automatically map a UML state chart to BIR language, which is designed for BOGOR model checking. The goal of the verification in this paper is to evaluate the deadlock property of this chart. The proposed method is evaluated by four case studies of ATM and Fax machine state charts and the model is verified regarding the existence of a deadlock. Results indicate that while the PAT verification tool cannot properly recognize deadlocks in a state chart, the proposed approach is capable of detecting such cases of a deadlock.