The rhapsody UML verification environment

Abstract

Object-oriented modeling plays an increasing role in the design of embedded controllers. Formal verification can be applied in order to give evidence for meeting safety critical requirements. The "Rhapsody UML Verification Environment" supports verification of safety and liveness requirements for embedded controllers, developed within the Unified Modeling Language (UML). The verification environment is integrated in the design tool "Rhapsody in C+ +" offered by the company I-Logix. This paper discusses how UML models are transformed into a format usable for the VIS model checker, shows the specification and verification on a simple example and explains how the tool can be used to help determining the memory resources of a model.