The Rhapsody UML Verification Environment
I. Schinz, Tobe Toben, C. Mrugalla, Bernd Westphal · 2004
Abstract Object-oriented modeling plays an increasing role inthe design of embedded controllers. Formal verification can be applied in order to give evidence for meeting safetycritical requirements. The "Rhapsody UML Verification Environment " supports verification of safety and livenessrequirements for embedded controllers, developed within the Unified Modeling Language (UML). The verificationenvironment is integrated in the design tool "Rhapsody in C++ " offered by the company I-Logix. This paper discusses how UML models are trans-formed into a format usable for the VIS model checker, shows the specification and verification on a simple ex-ample and explains how the tool can be used to help determining the memory resources of a model. 1.