A dynamic assertion-based verification platform for UML statecharts over rhapsody

For quite some time, the Unified Modeling Language (UML) has been adopted by designers of safety critical control systems such as automotive and aviation control. This has led to an increased emphasis on setting up a validation flow over UML that can be used to guarantee the correctness of UML models. In this paper, we propose a dynamic Assertion-based verification (ABV) framework for validation of UML Statecharts over the Rhapsody platform of I-logix. We present an extension of Linear Temporal Logic (LTL), named Action-LTL that allows assertions to be specified over data attributes and events of UML models. We present a methodology for automatic generation of Rhapsody Statecharts from Action-LTL specifications. These generated Statecharts are added as simulation observers to an existing UML model to detect specification violations during simulation. In view of the capacity limitations of existing formal assertion-based verification tools, we believe that our methods are of immediate practical value to the UML-based design community.