Software

Tracing Properties of UML and OCL Models With Maude

Date Added: Jul 2011
Format: PDF

The starting point of this paper is a system described in form of a UML class diagram where system states are characterized by OCL invariants and system transitions are defined by OCL pre- and post-conditions. The aim of the approach is to assist the developer in learning about the consequences of the described system states and transitions and about the formal implications of the properties that are explicitly given. The authors propose to draw conclusions about the stated constraints by translating the UML and OCL model into the algebraic specification language and system Maude, which is based on rewrite logic.