Modeling and Verification of Manufacturing Systems: A Domain-Specific Formalization of UML

S. Flake (Germany)

Keywords

Object Constraint Language (OCL) UML Statecharts Formal semantics

Abstract

This article presents a formalization of parts of the Unified Modeling Language (UML) w.r.t. the domain of modeling time-dependant manufacturing systems. The formalization approach is based upon a set of identified general formal ization steps. We investigate the applicability of UML class diagrams, Statecharts, and UML's textual Object Con straint Language (OCL) to model manufacturing systems and specify required time-dependent system properties. We then define a formal semantics for the utilized UML mod eling elements and the extensions we have to make due to the considered domain. Corresponding mappings to formal languages allow to verify whether a domain-specific UML model satisfies required temporal properties.

Important Links:



Go Back