EAFM-Projects

Projects

QMaxUSE

QMaxUSE is an automatic tool that allows users to issue a set of queries over UML class diagrams and OCL constraints. The new algorithms used by QMaxUSE break large and complex models into multiple queries that can be verified concurrently. Currently, QMaxUSE has its own query langauges, is under development and will be released for testing.

MaxUSE
MaxUSE is an automatic tool that finds the set of achievable features and constraint conflicts for inconsistent metamodels (UML class diagrams). MaxUSE allows users to freely rank individual model features or use automatic ranking. MaxUSE integrates USE modelling tool with Z3 SMT Solver. It currently uses Uran as its solving engine to interact with Z3.

Uran
Uran provides Java APIs for generating standard SMT2 formulas. Though Z3 Java API does the same thing, Uran differs by giving full control of generated SMT formulas. Thus, it is very well suited for debugging purpose. Currently, uran supports generating different kinds of formulas including: boolean-circuit gate (CNF), quantifiers, arithmetic (linear inequalities.). It now uses Z3 as its back-end solver. Uran can be considered as an engine that you could place in between solvers and your own specification language, and seperate your code from underlying solvers.

Smart Cities
This project focuses on applying and modelling Enterprise Architecture (EA) in Smart Cities. Smart Citites are complex systems where offered city services must respond to multiple goals and involve multi-domain systems and heterogeneous data sources. This requires a coherent EA Modelling Langauge to provide the techniques and tools for using models. We propose a Smart City ALignment Metamodel (SCALM), following the Design Science Research Methodology. The metamodel was developed by extending the ArchiMate language and applying multiple case studies within real-world cities.