Validation of UML Models for Interactive Systems with CPN and SPIN

Abstract

Unified Modelling Language (UML) is considered to be the standard language for object-oriented modeling and analysis. However, UML cannot be used for automatic analysis and simulation. The system model developed on the basis of UML tool is not executable in nature. So, behavior of the model cannot be validated until it is implemented. In this thesis, an approach for transforming UML Interaction Overview Diagram (IOD) to Colored Petri Net (CPN) models is proposed. This transformation is used to bridge the gap between informal notation (UML diagrams) and more formal notation (CPN models) for analysis purpose. CPN model is validated by CPN tool. CPN tool is executable, and it is possible to inspect the behavior of the system by simulating CPN model. An interaction overview diagram has been designed for the different operation of an Automatic Teller Machine (ATM) using Magic Draw. Later, this diagram is transformed to CPN model. The specification of the proposed system has been analyzed by simulating the CPN model on CPN tool. Model checking is an important technique for ensuring the correctness of any system. This thesis presents a case study for model checking through an example of verifying ATM with Simple PROMELA Interpreter (SPIN). The ATM system was modeled in Process or Protocol Meta Language (PROMELA) for business flow of an ATM system. It is then checked for deadlock and unreachable code with SPIN model checker. Here the SPIN model checker is used to apply Linear Temporal Logic (LTL) formula on the ATM system and check for liveness and safety properties. The results showed that the ATM model did not have deadlock and unreachable code, and also satisfied the liveness and safety properties.