Alloy is a textual language developed by Daniel Jackson and his team at MIT. It is a formal language, which has a succinct syntax and allows specification and automatic analysis of a wide variety of systems. On the other hand, the Unified Modelling Language (UML) is a semi-formal language, which is accepted by the software engineering community as the defacto standard for modelling, specification and implementation of Object based systems. This paper studies the integration of the UML and Alloy into a single CASE tool, which aims to take advantage of the positive aspect of both the UML and Alloy. Alloy and UML specification provide two views of the system. In order to synchronise the two views, we make use of the MDA style transformation. In particular, we shall present a Meta Object Facility (MOF) compliant metamodel for Alloy and define a model transformation from the UML metamodel to the Alloy metamodel. Based on the approach presented in the paper, we have implemented a tool called UML2Alloy for the modelling and analysis of Discrete Event Systems. To evaluate the tool, the paper presents a case study involving the modelling and analysis of a prototype manufacturing system.
Keywords: UML, OCL, Alloy, Verification, MDA, Metamodel, Transformation
|
