Automatic Verification of UML Statecharts by BOGOR Model Checking Tool

چکیده مقاله

Abstract—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 describes 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 study 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.