Formal verification Unified Modeling Language Statechart using Enhancement Common Modeling Language

Modern systems are rapidly evolving and increasing in complexity to satisfy growing requirements. Such systems often incorporate multiple hierarchical statecharts within their behavior modeling diagram, which significantly complicates the verification process. To address this challenge, the Common Modeling Language (CML) was introduced as an intermediate modeling language for formal verification, serving as a bridge between Unified Modeling Language (UML) Statechart and the model checkers. However, CML supports modeling only a single hierarchical statechart, which limits its applicability to complex systems. This study introduces the Enhancement Common Modeling Language (E-CML), an extension of the CML, to support the verification of systems that incorporate multiple hierarchical statecharts. We introduce the group component in E-CML, comprising an initial state, a set of states, transitions, triggers, and a region, to formally differentiate the group components from superstates. We also propose new translation rules to map E-CML into Symbolic Model Verifier (SMV) syntax. E-CML operates through two main processes: transformation and translation. The transformation process transforms an XML Metadata Interchange (XMI) file into E-CML, while the translation process translates E-CML to an Input Symbolic Model Verifier (I-SMV) file. The system is verified using the SMV model checker, with formal properties specified in Computational Tree Logic (CTL) and represented in the I-SMV file. The results demonstrate that the behavior modeling diagram satisfies all formal properties, indicating that E-CML provides an effective framework for the verification of complex systems comprising multiple hierarchical statecharts.

Text 124679.pdf - Published Version Available under License Creative Commons Attribution. Download (480kB) Official URL or Download Paper: http://thesai.org/Publications/ViewPaper?Volume=16...

Actions (login required)

View Item