Generic Methodology for Formal Verification of UML Models

This paper discusses a Unified Modelling Language (UML) based formal verification methodology for early error detection in the model-based software development cycle. Our approach proposes a UML-based formal verification process utilising functional and behavioural modelling artifacts of UML. It reinforces these artifacts with formal model transition and property verification. The main contribution is a UML to Labelled Transition System (LTS) Translator application that automatically converts UML Statecharts to formal models. Property specifications are derived from system requirements and corresponding Computational Tree Logic (CTL)/Linear Temporal Logic (LTL) model checking procedure verifies property entailment in LTS. With its ability to verify CTL and LTL specifications, the methodology becomes generic for verifying all types of embedded system behaviours. The steep learning curve associated with formal methods is avoided through the automatic formal model generation and thus reduces the reluctance of using formal methods in software development projects. A case study of an embedded controller used in military applications validates the methodology. It establishes how the methodology finds its use in verifying the correctness and consistency of UML models before implementation.

An efficient and scalable search engine for models

Search engines extract data from relevant sources and make them available to users via queries. A search engine typically crawls the web to gather data, analyses and indexes it and provides some query mechanism to obtain ranked results. There exist search engines for websites, images, code, etc., but the specific properties required to build a search engine for models have not been explored much. In the previous work, we presented MAR, a search engine for models which has been designed to support a query-by-example mechanism with fast response times and improved precision over simple text search engines. The goal of MAR is to assist developers in the task of finding relevant models. In this paper, we report new developments of MAR which are aimed at making it a useful and stable resource for the community. We present the crawling and analysis architecture with which we have processed about 600,000 models. The indexing process is now incremental and a new index for keyword-based search has been added. We have also added a web user interface intended to facilitate writing queries and exploring the results. Finally, we have evaluated the indexing times, the response time and search precision using different configurations. MAR has currently indexed over 500,000 valid models of different kinds, including Ecore meta-models, BPMN diagrams, UML models and Petri nets. MAR is available at http://mar-search.org.

Detecting the Most Important Classes from Software Systems with Self Organizing Maps

Self Organizing Maps (SOM) are unsupervised neural networks suited for visualisation purposes and clustering analysis. This study uses SOM to solve a software engineering problem: detecting the most important (key) classes from software projects. Key classes are meant to link the most valuable concepts of a software system and in general these are found in the solution documentation. UML models created in the design phase become deprecated in time and tend to be a source of confusion for large legacy software. Therefore, developers try to reconstruct class diagrams from the source code using reverse engineering. However, the resulting diagram is often very cluttered and difficult to understand. There is an interest for automatic tools for building concise class diagrams, but the machine learning possibilities are not fully explored at the moment. This paper proposes two possible algorithms to transform SOM in a classification algorithm to solve this task, which involves separating the important classes - that should be on the diagrams - from the others, less important ones. Moreover, SOM is a reliable visualization tool which able to provide an insight about the structure of the analysed projects.

Ontology-Based Transformation and Verification of UML Qualified Association

UML class model is an essential element of today's software development process. In modern software development methodologies, it is considered a key contributor in every phase of software development. It may be automatically converted into other UML models and even in programming code. However, the erroneous model generates other erroneous models. The model verification technique checks the presence of error in the UML class model. This paper's main objective is to introduce a technique for the completely automatic and expressive transformation of the UML class model's qualified association into ontology. Because the current verification method does not support the transformation and verification of qualified associations. Later on, the ontology-based reasoning method is presented to verify qualified associations and their constraints.

Validation Automation of UML Diagrams Created by Students

Unified Modeling Language (UML) is widely used standard for models visualization in software industry. Hence, a preparation of IT professionals involves the learning modeling process. Studies of student perception of UML modeling indicate that this process is perceived as quite complex. This paper presents software for validation activity, class and use-case diagrams by XMI representation. To achieve this goal, we researched existing methods and systems. Besides, we analyzed mistake catalogues and Perm State University’s student models to propose a mistake classification and checklist that presents a list of validation to be done. This paper focuses on validation each type of diagram separately, without maintaining consistency between different UML models. However, all these validation modules are combined in one system, which allows to check any of the described types of diagrams.

Model Transformation Approach According Model-Driven Architecture From BPMN to UML Up to IFML

The main key in MDA is the model's transformation. There are two transformation kinds into MDA: CIM to PIM and PIM to PSM. Most researchers focused on transformation from PIM to PSM because there are several points in common between these two levels. But transforming CIM to PIM is rarely discussed in research subjects because they are two different levels. This chapter presents a methodology to master model transformation from CIM to PIM up to PSM respecting MDA. The methodology is founded on creating a good CIM level, through well-chosen rules, to facilitate transformation to the PIM level. However, the authors establish a rich PIM level, respecting the three classic modeling views: functional, dynamic, and static. The method conforms to MDA by considering the business dimension in the CIM level, through BPMN which is the OMG standard for modeling business process. Nevertheless, they used UML models into the PIM level because UML is recommended by MDA in this level. Then, they use IFML the OMG standard for representing web interface model in PSM level.