UML2Alloy: Analysis of UML model via SAT-solvers

 

The goal of this research is to achieve automated analysis of UML Class Diagrams enriched with OCL or constraints written in Natural Languages. The transformation from UML (Class diagram and OCL is explained [3] and [4]. The proposed method has been implemented in in a prototype tool called UML2Alloy. The implementation of transformations is via SiTra which is extended to support MDA Tracing as specified in QVT [5]. UML2Alloy has been applied to the analysis of UML models in various applications domains such as Manufacturing [1], security [6,7] and proving correctness of Model Transformations [2], among others.

We have experimented with other UML diagrams such as Sequence Diagrams. We can transform simple Sequence Diagrams to Alloy. In [8,9,10] we present a method of using Petri nets to analyse Sequence Diagrams. Recently, we have extended UML2Alloy to use Natural Languages for describing Constraints, see NL2OCLviaSBVR.

Selected publications

  1. UML2Alloy: A tool for lightweight modelling of Discrete Event Systems, B. Bordbar, K. Anastasakis In: Proc. IADIS International Conference in Applied Computing 2005, Algarve, Portugal, (2005) 209-216

  2. Analysis of Model Transformations via Alloy, K. Anastasakis, B. Bordbar and J. M. Kuster, Model-Driven Engineering, Verification and Validation (MoDeVVa'07) Associated with MoDELS’07

  3. UML2Alloy: A Challenging Model Transformation, K. Anastasakis, B. Bordbar, G. Georg, and I Ray, ACM/IEEE 10TH International Conference on Model Driven Engineering Languages and Systems, LNCS, Vol. 4735, pages 436-450, 2007

  4. On challenges of Model Transformation from UML to Alloy, K. Anastasakis, B. Bordbar, G. Georg, and I Ray, Journal of System and Software Modelling, 2008

  5. From UML to Alloy and Back, S.M.A. Shah, K.Anastasakis, B. Bordbar, 6th Workshop on Model Design, Verification and Validation (MODEVVA 09) published in ACM International Conference Proceeding Series; Vol. 413, pages 1-10, 2009 (won the best paper award)

  6. Ensuring Spatio-Temporal Access Control for Real-World Applications, M. Toahchoodee, I. Ray, K. Anastasakis, G. Georg and B. Bordbar, Proceedings of the 14th ACM Symposium on Access Control Models and Technologies, Stresa, Italy, June 2009.

  7. Verification and Trade-off Analysis of Security Properties in UML System Models, G. Georg, K. Anastasakis, B. Bordbar, S. H. Houmb, I. Ray, M. Toahchoodee, accepted for publication in IEEE Transactions on Software Engineering, Volume 36 no. 3, Pages 338 - 356, 2010

  8. A Model Driven Approach to the Analysis of Timeliness Properties, M. A. Ameedeen, B. Bordbar and R. Anane, European Conference on Model Driven Architecture Foundations and Applications (ECMDA-FA 09), LNCS, Vol. 5562, pages 221-236, 2009

  9. A Model Driven Approach to Represent Sequence Diagrams as Free Choice Petri Nets, M. A.Ameedeen, B.Bordbar, Proceeding of 12th IEEE International conference on Enterprise Distributed Object Computing(EDOC) pages 213-221, 2008

  10. Model Interoperability via Model Driven Development M. A. Ameedeen, B. Bordbar, R. Anane, accepted for publication in Journal of Computer and System Sciences, 2010