Ontology-Based Transformation and Verification of UML/OCL Constraints

In Software Engineering (SE), the graphical models specify the system's architecture, connection, and characteristics. New SE methods such as MDA utilize graphical models as a nucleus of all development activities. This paper presents the transformation and verification of class diagram and Object Constraint Language (OCL) and transformation algorithm from Class model to ontology in the continuity of our research on UML and ontology integration. The class diagram is transformed into ontology, and constraints specified through OCL are transformed into SPARQL.

A formal approach to finding inconsistencies in a metamodel

Checking the consistency of a metamodel involves finding a valid metamodel instance that provably meets the set of constraints that are defined over the metamodel. These constraints are often specified in Object Constraint Language. Often, a metamodel is inconsistent due to conflicts among the constraints. Existing approaches and tools are typically incapable of pinpointing the conflicting constraints, and this makes it difficult for users to debug and fix their metamodels. In this paper, we present a formal approach for locating conflicting constraints in inconsistent metamodels. Our approach has four distinct features: (1) users can rank individual metamodel features using their own domain-specific knowledge, (2) we transform these ranked features to a weighted maximum satisfiability modulo theories problem and solve it to compute the set of maximum achievable features, (3) we pinpoint the conflicting constraints by solving the set cover problem using a novel algorithm, and (4) we have implemented our approach into a fully automated tool called MaxUSE. Our evaluation results, using our assembled set of benchmarks, demonstrate the scalability of our work and that it is capable of efficiently finding conflicting constraints.

Modeling and Solving a Latin American University Course Timetabling Problem Instance

Timetabling problem is a complex task that is performed by a number of institutions worldwide, which has been usually addressed as an optimization problem where every approach considers the particular constraints of each institution under consideration. In this paper, we describe, model, and propose a solution to the timetabling problem at the División Académica de Ciencias y Tecnologías de la Información of the Universidad Juárez Autónoma de Tabasco (UJAT), México. We modeled the specific constraints of this problem instance using the Object Constraint Language (OCL) of the Unified Modeling Language (UML), and we validated the model while using the state-of-the-art tool USE: UML-based Specification Environment. The solution strategy tackles the problem in two stages: (1) ACA: academic assignments, i.e., assign lectures to professors and (2) TTP: the timetabling process. We developed a Tabu Search customization named Tabu Search with Probabilistic Aspiration Criterion (TS-PAC) in order to solve the timetabling problem, and we developed a software prototype to test our proposal. Two feasible timetables for two different semesters were obtained according to the modeled constraints.

A Comparative Study on Transformation of UML/OCL to Other Specifications

Background: Static verification is a sound programming methodology that permits automated reasoning about the correctness of an implementation with respect to its formal specification before its execution. Unified Modelling Language is most commonly used modelling language which describes the client’s requirement. Object Constraint Language is a formal language which allows users to express textual constraints regarding the UML model. Therefore, UML/OCL express formal specification and helps the developers to implement the code according to the client’s requirement through software design. Objective: This paper aims to compare the existing approaches generating Java, C++, C# code or JML, Spec# specifications from UML/OCL. Methods: Nowadays, software system is developed via automatic code generation from software design to implementation when using formal specification and static analysis. In this paper, the study considers transformation from design to implementation and vice versa using model transformation, code generation or other techniques. Results: The related tools, which generate codes, do not support verification at the implementation phase. On the other hand, the specification generation tools do not generate all the required properties which are needed for verification at the implementation phase. Conclusion: If the generated system supports the verification with all required properties, code developer needs less efforts to produce correct software system. Therefore, this study recommends introducing a new framework which can act as an interface between design and implementation to generate verified software systems.

Configurable DDS as Uniform Middleware for Data Communication in Smart Grids

Data Distribution Service (DDS) has emerged as a potential solution for data communication challenges in smart grids. DDS is designed to support quality communication for large scale real-time systems through a wide range of QoS policies. However, a smart grid involves various types of communication applications running on different computing environments. Some environments have limited computing resources such as small memory and low performance, which makes it difficult to accommodate DDS. In this paper, we present a feature-based approach for tailoring DDS to configure lightweight DDS by selecting only the necessary features for the application in consideration of the resource constraints of its running environment. This allows DDS to serve as a uniform communication middleware across the smart grid, which is critical for interoperability. We analyze DDS in terms of features and design them using Unified Modeling Language (UML) and Object Constraint Language (OCL) based on inheritance and overriding. We define a formal notion of feature composition to build DDS configurations. We implemented the approach in OpenDDS and demonstrate its application to different application environments. We also experimented the approach for the efficiency of configured DDS in terms of resource utilization. The results show that configured DDS is viable for efficient and quality data communication for applications that run on an environment with limited computing capability.