Search

The design and implementation of vehicle suspension systems is complex and time-consuming process that usually leads to production delays. Although different Model Driven Engineering (MDE) technologies like EAST-ADL/AUTOSAR are frequently applied to expedite vehicle development process, a framework particularly dealing with design and analysis of vehicle suspension is hard to find in literature. This rises the need of a framework that not only supports the analysis of suspension system at higher abstraction level but also complements the existing standards like EAST-ADL. In this article, a Model driven framework for Vehicle Suspension System (MVSS) is proposed. Particularly, a meta-model containing major vehicle suspension aspects is introduced. Subsequently, a modeling editor is developed using Eclipse Sirius platform. This allows the modeling of both simple as well as complex vehicle suspension systems with simplicity. Moreover, Object Constraint Language (OCL) is utilized to perform early system analysis in modeling phase. Furthermore, the target MATLAB-Simulink models are generated from source models, using model-to-text transformations, to perform advanced system analysis. The application of proposed framework is demonstrated through real life Audi A6L Hydraulic active suspension use case. The initial results indicate that proposed framework is highly effective for the design and analysis of vehicle suspension systems. In addition to this, the analysis results could be propagated to EAST-ADL toolchains to support full vehicle development workflow.

En muchas asignaturas de Ingeniería Informática se pide a los alumnos que programen en papel. Entre sus ventajas, esto permite a los alumnos centrarse en la funcionalidad evitando las distracciones causadas por la sintaxis y sin limitar su pensamiento a un lenguaje o paradigma de programación concreto. Aún así, los estudiantes se quejan de no poder probar su código, lo que les impide descubrir errores. En contraposición al estado del arte que ha estudiado este problema para lenguajes de propósito general como Java con estudiantes de cursos iniciales, nosotros nos centramos en lenguajes estándares de la definición de reglas como OCL que se imparten en cursos avanzados. En este artículo presentamos nuestra experiencia tras introducir una herramienta de modelado para la definición de restricciones OCL en una asignatura de Ingeniería de Requisitos. Esta asignatura es optativa y se ofrece en el tercer y cuarto curso del grado de Ingeniería Informática. El estudio que hemos realizado abarca dos cursos académicos, 2019 y 2020, en los cuales hubo 136 y 161 estudiantes matriculados respectivamente. Presentamos los detalles de nuestro experimento, los resultados obtenidos del estudio empírico llevado a cabo y nuestras conclusiones, las cuales respaldan la idoneidad del uso de herramientas., In many Computer Engineering courses, students are asked to program on paper. Among its advantages, this allows students to focus on functionality avoiding the distractions caused by syntax and without limiting their thinking to a specific programming language or paradigm. Still, students complain about not being able to test their code, preventing them from discovering bugs. While the state of the art has studied this problem for general-purpose languages like Java and with students of initial courses, we focus on standard languages for contraint definition like OCL, which are taught in advanced courses. In this article, we present our experience after introducing a modeling tool for the definition of OCL constraints in the Requirements Engineering course. This course is optional and is offered in the third and fourth years of the Computer Engineering degree. The study we have carried out covers two academic years, 2019 and 2020, in which there were 136 and 161 students enrolled, respectively. We present the details of our study, the results obtained from the empirical study carried out and our conclusions, which support the suitability of the use of tools.

In artifact-centric business process models it is usually assumed that the specification of the activities requires stating all the effects of the activity execution over the information base (i.e. over the artifacts it handles). In particular, these effects have to deal with integrity constraint enforcement to ensure a proper treatment of integrity constraints during activity execution. Manually specifying this treatment is a difficult, expensive and error-prone task, because of the inherent difficulty of getting rid of all the implication entailed by the constraints and also of the way to properly handle it. In this paper, we advocate for separating constraint handling from the specification of activities in such a way that only the effects of the activity over the artifacts have to be defined (without needing to care about the constraints). Then, we propose an approach to automatically generate an extension to the original business process model that allows identifying at run-time the additional updates that have to be applied to the information base to repair all constraint violations caused by the activity execution., This work is partially supported by the REMEDiAL project,funded by Ministerio de Economia, Industria y Competitividad, Spain (TIN2017-87610-R); by the Generalitat de Catalunya, Spain (under 2017-SGR-1749); and by European Research Council under the European Unions Horizon 2020 Programme through the ERC Advanced Grant WhiteMech (No. 834228) and the ICT-48 2020 project TAILOR (No. 952215)., Peer Reviewed, Postprint (author's final draft)

The ability to generate test data is often a necessary prerequisite for automated software testing. For the generated data to be fit for its intended purpose, the data usually has to satisfy various logical constraints. When testing is performed at a system level, these constraints tend to be complex and are typically captured in expressive formalisms based on first-order logic. Motivated by improving the feasibility and scalability of data generation for system testing, we present a novel approach, whereby we employ a combination of metaheuristic search and Satisfiability Modulo Theories (SMT) for constraint solving. Our approach delegates constraint solving tasks to metaheuristic search and SMT in such a way as to take advantage of the complementary strengths of the two techniques. We ground our work on test data models specified in UML, with OCL used as the constraint language. We present tool support and an evaluation of our approach over three industrial case studies. The results indicate that, for complex system test data generation problems, our approach presents substantial benefits over the state of the art in terms of applicability and scalability.

UML models are standard artifacts used by software engineers for designing software. As software is designed, different UML diagram types (e.g., class diagrams and sequence diagrams) are produced by software designers. Since the various UML diagram types describe different aspects of a software system, they are not independent but strongly depend on each other, hence they must be consistent. Inconsistencies cause faults in the final software systems. It is, therefore, paramount that they get detected, analyzed, and fixed. Consistency rules are a useful tool proposed in the literature to detect inconsistencies. They categorize constraints that help in identifying inconsistencies when violated. This case study aims at collecting and analyzing UML models with OCL consistency rules proposed in the literature and at promoting the development of a reference benchmark that can be reused by the (FM-)research community. We collected 33 UML consistency rules and 206 different UML diagrams contained in 34 open-source UML models presented in the literature. We propose an FM-based encoding of the consistency rules in OCL. This encoding allows analyzing whether the consistency rules are satisfied or violated within the 34 UML models. To assess the proposed benchmark, we analyzed how the UML models, consistency rules, diagram types contained in the benchmark help in assessing the consistency of UML models, and the consistency of diagrams across the different software development phases. Our results show that the considered UML models and consistency rules allowed identifying 2731 inconsistencies and that those inconsistencies refer to different software development phases. We concluded that the considered UML models and consistency rules could be considered as an initial benchmark that can be further extended by the research community.

The Object Constraint Language (OCL) is a textual, declarative language typically used as part of the UML standard for specifying constraints and queries on models. Several attempts have been proposed in the past for translating OCL expressions into SQL queries in the context of Model Driven Engineering (MDE). To cope with OCL expressions that include iterators, previous attempts resorted to imperative features (loops, cursors) of SQL, with the consequent loss of efficiency. In this paper, we define (and implement) a novel mapping from OCL to SQL that covers (possibly nested) iterators, without resorting to imperative, non-declarative features of SQL. We show with a preliminary benchmark that our mapping generates SQL queries that can be efficiently executed on mid- and large-size SQL databases. 185-203

Model-driven engineering (MDE) enables the rise in abstraction during development in software and system design. In particular, meta-models become a central artifact in the process, and are supported by various other artifacts such as editors and transformation. In order to define constraints, invariants, and queries on model-driven artifacts, a generic language has been developed: the Object Constraint Language (OCL). In literature, many studies into OCL have been performed on small collections of data, mostly originating from a single source (e.g., OMG standards). As such, generalization of results beyond the data studied is often mentioned as a threat to validity. Creation of a benchmark dataset has already been identified as a key enabler to address the generalization threat. To facilitate further empirical studies in the field of OCL, we present the first large-scale dataset of 103262 OCL expression, systematically extracted from 671 GitHub repositories. In particular, our dataset has extracted these expressions from various types of files (a.o. metamodels and model-to-text transformations). In this work we showcase a variety of different studies performed using our dataset, and describe several other types that could be performed. We extend previous work with data and experiments regarding OCL in model-to-text (mtl) transformations.

The General Data Protection Regulation (GDPR) harmonizes data privacy laws and regulations across Europe. Through the GDPR, individuals are able to better control their personal data in the face of new technological developments. While the GDPR is highly advantageous to citizens, complying with it poses major challenges for organizations that control or process personal data. Since no automated solution with broad industrial applicability currently exists for GDPR compliance checking, organizations have no choice but to perform costly manual audits to ensure compliance. In this paper, we share our experience building a UML representation of the GDPR as a first step towards the development of future automated methods for assessing compliance with the GDPR. Given that a concrete implementation of the GDPR is affected by the national laws of the EU member states, GDPR’s expanding body of case laws and other contextual information, we propose a two-tiered representation of the GDPR: a generic tier and a specialized tier. The generic tier captures the concepts and principles of the GDPR that apply to all contexts, whereas the specialized tier describes a specific tailoring of the generic tier to a given context, including the contextual variations that may impact the interpretation and application of the GDPR. We further present the challenges we faced in our modeling endeavor, the lessons we learned from it, and future directions for research.

The verification of complex software systems often requires to check quantitative properties that rely on aggregation operators (e.g., the average response time of a service). One way to ease the specification of these properties is to use property specification patterns, such as the ones for “service provisioning”, previously proposed in the literature. In this paper we focus on the problem of performing offline trace checking of temporal properties containing aggregation operators. We first present TemPsy-AG, an extension of TemPsy—an existing pattern-based language for the specification of temporal properties—to support service provisioning patterns that use aggregation operators. We then extend an existing model-driven procedure for trace checking, to verify properties expressed in TemPsy-AG. The trace checking procedure relies on the efficient mapping of temporal properties written in TemPsy-AG into OCL constraints on a meta-model of execution traces. We have implemented this procedure in the TemPsy-Check-AG tool and evaluated its performance: our approach scales linearly with respect to the length of the input trace and can deal with much larger traces than a state-of-the-art tool.

In this paper, we discuss some of the challenges and opportunities that arise when mapping OCL into SQL. For the challenges, we review the past proposals, evaluating their key design decisions and limitations. For the opportunities, we highlight the key role that OCLto-SQL code-generators can play in model-driven software development. By no means we pretend to exhaust the subject: other challenges and opportunities can be identified and brought up. Our present goal is to stir up again the discussion on this subject among the OCL community.

OCL is the standard language for defining constraints in UML class diagrams. Unfortunately, as we show in this paper, full OCL is so expressive that it is not possible to check general OCL constraints efficiently. In particular, we show that checking general OCL constraints is not only not polynomial, but not even semidecidable. To overcome this situation, we identify OCLFO , a fragment of OCL which is expressively equivalent to relational algebra (RA). By equivalent we mean that any OCLFO constraint can be checked through a RA query (which guarantees that OCLFO checking is efficient, i.e., polynomial), and any RA query encoding some constraint can be written as an OCLFO constraint (which guarantees expressiveness of OCLFO ). In this paper we define the syntax of OCLFO , we concisely determine its semantics through set theory, and we prove its equivalence to RA. Additionally, we identify the core of this language, i.e., a minimal subset of OCLFO equivalent to RA., Peer Reviewed, Postprint (author's final draft)

Offline trace checking tools check whether a specification holds on a log of events recorded at run time; they yield a verification verdict (typically a boolean value) when the checking process ends. When the verdict is false, a software engineer needs to diagnose the property violations found in the trace in order to understand their cause and, if needed, decide for corrective actions to be performed on the system. However, a boolean verdict may not be informative enough to perform trace diagnostics, since it does not provide any useful information about the cause of the violation and because a property can be violated for multiple reasons. The goal of this paper is to provide a practical and scalable so- lution to solve the trace diagnostics problem, in the settings of model-driven trace checking of temporal properties expressed in TemPsy, a pattern-based specification language. The main contributions of the paper are: a model-driven approach for trace diagnostics of pattern-based temporal properties expressed in TemPsy, which relies on the evaluation of OCL queries on an instance of a trace meta-model; the implementation of this trace diagnostics procedure in the TemPsy-Report tool; the evaluation of the scalability of TemPsy-Report, when used for the diagnostics of violations of real properties derived from a case study of our industrial partner. The results show that TemPsy-Report is able to collect diagnostic information from large traces (with one million events) in less than ten seconds; TemPsy-Report scales linearly with respect to the length of the trace and keeps approximately constant performance as the number of violations increases.

In this thesis, we want to use conceptual modeling languages to define security protocols and to build an environment in which these protocols can be executed in an automated way., En aquesta tesi, volem utilitzar llenguatges de modalització conceptual per definir protocols de seguretat i també es pretén construir un entorn en què aquests protocols es puguin executar de forma automàtica.

De nos jours, de nombreux projets, ou de grands systèmes complexes sont développés, mais la conservation de la cohérence entre les différentes spécifications devint un problème majeur. En pratique, cette tâche est délicate dû aux manques d'outils CASE qui peuvent aider à faire face à ce problème. Les spécifications doivent généralement être cohérentes, au cours des différentes étapes de développement et même au sein d’une étape elle-même. Les développeurs ont souvent tendance à effectuer ces vérifications manuellement (contrôle statique des éléments d’un même modèle), ce qui entraîne beaucoup de temps consacré à un travail qui pourrait être automatiquement réalisé, en plus du fait que la méthode manuelle peut ne pas être également correcte en tant que routine de vérification comparée à celle basée sur un outil de vérification. La vérification comportementale des diagrammes UML 2.0 a fait l’objet de plusieurs recherches spécifiant deux grandes familles de traitement du phénomène, une utilisant les transformations de modèles vers un modèle formel et une autre consistant à utiliser directement le modèle. Le développement d’une approche de vérification basée sur les transformations passe obligatoirement par la compréhension profonde des sémantiques associées aux diagrammes manipulées. Une des façons de spécifier le comportement dynamique dans UML consiste à modéliser les interactions entre les objets avec des diagrammes de séquence et de modéliser le comportement de chaque objet avec des machines à états. Dans ce contexte, le problème d'assurer la cohérence entre les diagrammes de séquence et les machines à états peut apparaître. Pour vérifier la cohérence, nous proposons une approche basée sur des compositions d'automates de Büchi qui nous permettent de saisir l'évolution de chaque objet le long de sa ligne de vie. Notre thèse se concentre sur les méthodes de modélisation et de vérification UML et comble l'écart entre les études théoriques sur les sémantiques formelles, Nowadays, many projects, or large complex systems are developed, but suffer to keep their specifications consistent. In practice, this is not an easy task due to the lack of CASE tools that help to deal with this problem. The specifications must generally be consistent, during different stages of development and even within a development stage. Developers often tend to perform these checks manually (static control of the same model elements), which results in a lot of time spent on work that could be automatically associated, in addition to the fact that the manual method may not be also correct as a verification routine compared to that based on a verification tool. The behavioral verification of UML 2.0 diagrams has been the subject of several studies specifying two main families of treatment of the phenomenon, one using the transformations of models towards a formal model and another one consisting of using directly the model. The development of a transformation-based verification approach requires a deep understanding of the semantics associated with the manipulated diagrams. One of the ways to specify dynamic behavior in UML is to model interactions between objects with sequence diagrams, and model the behavior of each object with state machines. In this context, the problem of ensuring consistency between the sequence diagrams and state machines may arise. To verify consistency, we propose an approach based on compositions of Büchi automata which allow us to capture the evolution of each object among the lifeline. Our paper focuses on UML modeling and verification methods and bridges the gap between theoretical studies on formal semantics and practical studies to implement languages through model transformations. The transformations include basic interactions, state invariants, strict and weak sequencing, and alternative interaction fragments.

Usage-based statistical testing employs knowledge about the actual or anticipated usage profile of the system under test for estimating system reliability. For many systems, usage-based statistical testing involves generating synthetic test data. Such data must possess the same statistical characteristics as the actual data that the system will process during operation. Synthetic test data must further satisfy any logical validity constraints that the actual data is subject to. Targeting data-intensive systems, we propose an approach for generating synthetic test data that is both statistically representative and logically valid. The approach works by first generating a data sample that meets the desired statistical characteristics, without taking into account the logical constraints. Subsequently, the approach tweaks the generated sample to fix any logical constraint violations. The tweaking process is iterative and continuously guided toward achieving the desired statistical characteristics. We report on a realistic evaluation of the approach, where we generate a synthetic population of citizens' records for testing a public administration IT system. Results suggest that our approach is scalable and capable o

Full UML/OCL is so expressive that most reasoning tasks are known to be undecidable in schemas defined with these languages. To tackle this situation, literature has proposed mainly three decidable fragments of UML/OCL: UML with no OCL, UML with limited OCL and no maximum cardinality constraints (OCL-Lite), and UML with limited OCL with no minimum cardinality constraints (OCL UNIVUNIV ). Since most conceptual schemas make use of OCL together with min and max cardinalities, this poses a strong limitation to current proposals. In this paper, we go beyond these limits by showing that OCL UNIVUNIV with acyclic min cardinality constraints and path acyclicity constraints also preserves decidability. In this way, we establish a language that can deal with most of UML/OCL identified constraint patterns. We also empirically test the expressiveness of this language through different UML/OCL case studies., Peer Reviewed, Postprint (author's final draft)

Ensuring the correctness of a conceptual schema is an essential task in order to avoid the propagation of errors during software development. The kind of reasoning required to perform such task is known to be exponential for UML class diagrams alone and even harder when considering OCL constraints. Motivated by this issue, we propose an innovative method aimed at removing constraints and other UML elements of the schema to obtain a simplified one that preserve the same reasoning outcomes. In this way, we can reason about the correctness of the initial artifact by reasoning on a simplified version of it. Thus, the efficiency of the reasoning process is significantly improved. In addition, since our method is independent from the reasoning engine used, any reasoning method may benefit from it., Peer Reviewed, Postprint (author's final draft)

Context: Business Process Management (BPM) is becoming a strategic advantage for organizations tostreamline their operations. Most business experts are betting for OMG Business Process Model and No- tation (BPMN) as de-facto standard (ISO/IEC 19510:2013) and selected technology to model processes. Thetemporal dimension underlies in any kind of process however, technicians need to shape this perspectivethat must also coexist with task control flow aspects, as well as resource and case perspectives. BPMNpoorly gathers temporary rules. This is why there are contributions that extend the standard to coversuch dimension. BPMN is mainly an imperative language. There are research contributions showing timeconstraints in BPMN, such as (i) BPMN patterns to express each rule with a combination of artifacts, thusthese approaches increase the use of imperative BPMN style, and (ii) new decorators to capture timerules semantics giving clearer and simpler comprehensible specifications. Nevertheless, these extensionscannot yet be found in the present standard.Objective: To define a time rule taxonomy easily found in most business processes and look for an ap- proach that applies each rule with current BPMN 2.0 standard in a declarative way.Method: A model-driven approach is used to propose a BPMN metamodel extension to address time- perspective.Results: We look at a declarative approach where new time specifications may overlie the main controlflow of a BPMN process. This proposal is totally supported with current BPMN standard, giving a BPMNmetamodel extension with OCL constraints. We also use AQUA-WS as a software project case study whichis planned and managed with MS Project. We illustrate business process extraction from project plans.Conclusion: This paper suggests to handle business temporal rules with current BPMN standard, alongwith other business perspectives like resources and cases. This approach can be applied to reverse engi- neering processes from legacy databases.

Offline trace checking is a procedure for evaluating requirements over a log of events produced by a system. The goal of this thesis is to present a practical and scalable solution for the offline checking of the temporal requirements of a system, which can be used in contexts where model-driven engineering is already a practice, where temporal specifications should be written in a domain-specific language not requiring a strong mathematical background, and where relying on standards and industry-strength tools for property checking is a fundamental prerequisite. The main contributions of this thesis are: i) the TemPsy (Temporal Properties made easy) language, a pattern-based domain-specific language for the specification of temporal properties; ii) a model-driven trace checking procedure, which relies on an optimized mapping of temporal requirements written in TemPsy into Object Constraint Language (OCL) constraints on a conceptual model of execution traces; iii) a model-driven approach to violation information collection, which relies on the evaluation of OCL queries on an instance of the trace model; iv) three publicly-available tools: 1) TemPsy-Check and 2) TemPsy-Report, implementing, respectively, the trace checking and violation information collection procedures; 3) an interactive visualization tool for navigating and analyzing the violation information collected by TemPsy-Report; v) an evaluation of the scalability of TemPsy-Check and TemPsy-Report, when applied to the verification of real properties. The proposed approaches have been applied to and evaluated on a case study developed in collaboration with a public service organization, active in the domain of business process modeling for eGovernment. The experimental results show that TemPsy-Check is able to analyze traces with one million events in about two seconds, and TemPsy-Report can collect violation information from such large traces in less than ten seconds; both tools scale linearly with respect

Este proyecto consiste en dar a la herramienta Recover la capacidad de generar una documentación web automática y actualizada de un sistema software a partir de la información de la herramienta, una traducción de UML/OCL y la generación automática de diagramas de secuencia y actividad, This project consists into giving Recover tool the capacity of generating an automatic and up-to-date web documentation of a software system from the information provided by the tool, a translation of UML/OCL and an automatic generation of sequence and activity diagrams.

A common practice to specify constraints on the Unified Modeling Language (UML) models is using the Object Constraint Language (OCL). Such constraints serve various purposes, ranging from simply providing precise meaning to the models to supporting complex verification and validation activities. In many applications, these constraints have to be solved to obtain values satisfying the constraints, for example, in the case of modelbased testing (MBT) to generate test data for the purpose of generating executable test cases. In our previous work, we proposed novel heuristics for various OCL constructs to efficiently solve them using search algorithms. These heuristics are enhanced in this paper to further improve the performance of OCL constraint solving. We performed an empirical evaluation comprising of three case studies using three search algorithms: Alternating Variable Method (AVM), (1+1) Evolutionary Algorithm (EA), and a Genetic Algorithm (GA) and in addition Random Search (RS) was used as a comparison baseline. In the first case study, we evaluated each heuristics using carefully designed artificial problems. In the second case study, we evaluated the heuristics on various constraints of Cisco’s Video Conferencing Systems defined to support MBT. Finally, the third case study is about EURent Car Rental specification and is obtained from the literature. The results of the empirical evaluation showed that (1+1) EA and AVM with the improved heuristics significantly outperform the rest of the algorithms.

[CATALÀ] Disseny i desenvolupament d'un prototipus que implementa un dels passos necessaris per a l'execució d'esquemes conceptuals: la comprovació automàtica i eficient de les restriccions d'integritat del model amb una tècnica de comprovació incremental sobre una base de dades relacional., [ANGLÈS] Design and development of a prototype that implements one of the necessary steps to execute conceptual schemas: the automatic and efficient checking of the integrity constraints of the model, with a technique of incremental checking on a relational database.

Valid states of data are those satisfying a set of constraints. Therefore, efficiently checking whether some constraint has been violated after a data update is an important problem in data management. We tackle this problem by incrementally checking OCL constraint violations by means of SQL queries. Given an OCL constraint, we obtain a set of SQL queries that returns the data that violates the constraint. In this way, we can check the validity of the data by checking the emptiness of these queries. The queries that we obtain are incremental since they are only executed when some relevant data update may violate the constraint, and they only examine the data related to the update., Peer Reviewed, Postprint (author's final draft)

The validation and the verification of conceptual schemas have attracted a lot of interest during the last years, and several tools have been developed to automate this process as much as possible. This is achieved, in general, by assessing whether the schema satisfies different kinds of desirable properties which ensure that the schema is correct. In this paper we describe AuRUS, a tool we have developed to analyze UML/OCL conceptual schemas and to explain their (in)correctness. When a property is satisfied, AuRUS provides a sample instantiation of the schema showing a particular situation where the property holds. When it is not, AuRUS provides an explanation for such unsatisfiability, i.e., a set of integrity constraints which is in contradiction with the property., Peer Reviewed, Postprint (author’s final draft)

We propose a new method for efficiently checking OCL constraints by means of SQL queries. That is, an OCL constraint is satisfied if its corresponding SQL query returns the empty set. Such queries are computed in an incremental way since, whenever a change in the data occurs, only the constraints that may be violated because of such change are checked and only the relevant values given by the change are taken into account. Moreover, the queries we generate do not contain nested subqueries nor procedures. In this way, we take advantage of relational DBMS capabilities and we get an efficient check of OCL constraints., Postprint (published version)

This paper presents an integrated enterprise architecture framework for qualitative and quantitative modeling and assessment of enterprise IT service availability. While most previous work has either focused on formal availability methods such as fault trees or qualitative methods such as maturity models, this framework offers a combination. First, a modeling and assessment framework is described. In addition to metamodel classes, relationships and attributes suitable for availability modeling, the framework also features a formal computational model written in a probabilistic version of the object constraint language. The model is based on 14 systemic factors impacting service availability and also accounts for the structural features of the service architecture. Second, the framework is empirically tested in nine enterprise information system case studies. Based on an initial availability baseline and the annual evolution of the 14 factors of the model, annual availability predictions are made and compared with the actual outcomes as reported in SLA reports and system logs. The practical usefulness of the method is discussed based on the outcomes of a workshop conducted with the participating enterprises, and some directions for future research are offered., QC 20141027. Updated from e-pub ahead of print to published.

Offline trace checking is a procedure for evaluating requirements over a log of events produced by a system. The goal of this paper is to present a practical and scalable solution for the offline checking of the temporal requirements of a system, which can be used in contexts where model-driven engineering is already a practice, where temporal specifications should be written in a domain-specific language not requiring a strong mathematical background, and where relying on standards and industry-strength tools for property checking is a fundamental prerequisite. The main contributions are: the TemPsy language, a domain-specific specification language based on common property specification patterns, and extended with new constructs; a model-driven offline trace checking procedure based on the mapping of requirements written in TemPsy into OCL (Object Constraint Language) constraints on a conceptual model on execution traces, which can be evaluated using an OCL checker; the implementation of this trace checking procedure in the TemPsy-Check tool; the evaluation of the scalability of TemPsy-Check and its comparison to a state-of-the-art alternative technology. The proposed approach has been applied to a case study developed in collaboration with a public service organization, active in the domain of business process modeling for eGovernment.

Tobulėjant išmaniesiems telefonams ir jų techninėms galimybėms bei didėjant jų pardavimams Lietuvoje ir pasaulyje, kuriamos aplikacijos tampa sudėtingesnės ir funkcionalesnės, tačiau kokybės problema vis dar išlieka skaudžia programinės įrangos kūrimo dalimi. Šiuo metu iš visų parduodamų išmaniųjų telefonų apie 50% parduodami su Android operacine sistema. Matant Android OS programų vis didėjantį poreikį rinkoje ir jų populiarumą bei panagrinėjus esamą rinką ir pamačius, jog testavimo įrankių, skirtų testuoti Android aplikacijas, beveik nėra, buvo nuspręsta, jog reikalingas vienetų testų generavimo sprendimas pritaikytas testuoti Android aplikacijas. Šio darbo pagrindinis tikslas ir yra pateikti vienetų testų generavimo sprendimą skirtą Android OS aplikacijos testuoti, jį realizuoti bei pagrįsti eksperimentiškai. Darbe siūlomas vienetų testų generavimo metodas, kuris remiasi atsitiktiniu generavimu, naudoja OCL apribojimus bei regresinio testavimo principus. Taip pat yra suderinamas su Google kompanijos teikiamu ADT įskiepiu ir Android SDK priemonėmis. Įrankis sukurtas kaip Eclipse programavimo aplinkos įskiepis. Pasiūlyto vienetų testų generavimo sprendimo efektyvumas įrodomas eksperimentiniu tyrimu. Šio eksperimento metu buvo testuojamos 4 aplikacijos. Naudojantis įrankiu vidutiniškai sugautų mutantų skaičius yra 75%. Mažiausia reikšmė yra 69%, o didžiausia – 88%. Vidutiniškai pasiekiamas 85% kodo eilučių padengimas. Mažiausia reikšmė yra 72%, o didžiausia padengimo... [toliau žr. visą tekstą], With the development of smart phones and their technical capabilities and increase of their sales in Lithuania and the world applications become more complex and have more functionality, but the issue of quality remains a painful part of the development of software. Currently 50% out of all smart phones are sold with Android operating system. Having an increasing demand and popularity of Android OS applications in the market, as well as having researched the current market and seen that there is a lack of testing tools to test Android applications, it has been decided that a solution generating unit tests is needed to test Android applications. The main goal of this work is to provide unit test generation solution for the Android OS application testing, implementation and validate it experimentally. This work proposes a method generating unit tests based on random generation, using OCL constraints and regression testing principles. It is compatible with Google plug-in ADT and Android SDK tools. The tool is designed as a plugin in Eclipse development environment. Efficiency of the proposed decision of generating unit tests is proved by experimental study. During this study four applications were tested. Using the tool the average of catched mutants is 75%. The minimum value is 69%, while the highest - 88%. On average coverage of code lines is achieved by 85%. The minimum value is 72% and the maximum value of coverage - 97%.

Diplomová práce se věnuje využití jazyka Object Constraint Language (OCL) v objektově orientovaných modelech. Jako prostředí pro práci s OCL byl původně vybrán modelovací nástroj Enterprise Architect (EA). Vzhledem ke zjištění nedostatečné podpory jazyka OCL v EA se práce věnuje také nalezení vhodného OCL prostředí. Dále se zabývá vývojem OCL pluginu pro platformu Eclipse umožňujícího generovat validační kód pro kontrolu diagramů tříd vyvářených v rámci kurzů objektově orientovaného modelování., The main purpose of this master thesis is to describe how Object Constraint Language (OCL) can be used in object-oriented models. The modeling tool Enterprise Architect (EA) had been originally selected as an OCL environment but was evaluated insufficient. The thesis is therefore focused on finding a suitable OCL environment as well. The thesis is also devoted to the development of an OCL plugin for the Eclipse platform. The developed plugin functions as a validation code generator for checking class diagrams created in object-oriented modeling courses., Katedra softwarových technologií, Vydařená diplomová práce, která se skládá z několika částí. V první části DP v souladu se zadáním byl popsán jazyk OCL a jeho využití. V části druhé je podrobně zdokumentován stav implementace jazyka OCL v komerčním CASE nástroji Enterprise Architect. Dle oponenta se diplomantovi podařilo splnit cíle diplomové práce. Struktura textu je jasná, logická a přehledná. Student výborně prezentoval výsledky své práce a zodpověděl dotazy vedoucího práce i členů komise.

En aquest projecte es construeix una eina per l'anàlisi d'esquemes conceptuals amb operacions basat en la reducció del problema a un problema de lògica de 1r ordre. A través d'uns tests predefinits i l'opció de definir-ne de propis, un usuari pot provar la correcció d'un esquema.

Concerns such as compliance, auditing, activity monitoring or accounting need to be addressed in the early stages of modeling and not only at the implementation or execution levels. AO4BPMN is an aspect-oriented extension of BPMN that facilitates the modularization of crosscutting concerns.

Los sistemas clásicos permiten realizar consultas precisas sobre bases de datos. Sin embargo, durante la especificación de los requisitos, el usuario puede utilizar términos lingüísticos vagos, que son propios del lenguaje natural e involucran términos imprecisos o difusos. Contrariamente a lo necesitado, pocas son las metodologías de consulta de bases de datos que incluyen requisitos difusos provenientes del lenguaje natural. En este trabajo, se propone un método basado en el lenguaje formal OCL y lógica difusa para el desarrollo de sistemas orientados a datos que permite tratar la ambigüedad propia del lenguaje natural en la implementación de requisitos difusos. Finalmente, se presenta un caso de estudio real para ilustrar el uso del método propuesto.

Testavimo procesą galima gerinti jį optimizuojant. Vienas iš galimų gerinimo būdų yra vienetų testai. Vienetų testai padeda sumažinti klaidų kiekį nuo 20 % iki 90 %, tačiau tuo pačiu programų kūrimo išlaidos gali padidėti apie 30 %. Vienas iš galimų būdų išlaikyti pasiektą vienetų testų efektyvumą ir palaikyti mažą kainą yra automatinis jų generavimas. Vienetų testų generatorius, generuoja vienetų testus remdamasis OCL apribojimais. Generatorius JAVA programiniame kode įterptus apribojimus generuoja į Junit vienetų testus., The development of modern software is a difficult process, there is a high possibility to leave uncorrected mistakes in the software, it would be more precisely to say that it is impossible to make software without bugs. Software testing is maybe the biggest part of development process. The unit testing is very powerful testing. It prevents from defects 20% and more [1]. The quality increase came at a cost of approximately 30% more development time. The main goal is create generator for unit testing. Automated test generator can reduce development time. Unit test generation is based on the OCL (Object Constraint Language) and software static model. OCL eliminate a test oracle problem. Software static model can be UML a class diagrams, but it very complicated approach. We use a reflection technology, because it is more precise and better today. Also OCL constrains are inserted in code.

Projecte realitzat en el marc d'un programa de mobilitat amb la Norwegian University of Science and Technology, Department of Computer and Information Science., The purpose of this project is to showcase the work cycle and feasibility of Test- Driven Conceptual Modelling (TDCM) on a real-sized system. In particular, we focus on the development, by reverse engineering, of the conceptual schema of Remember the Milk (RTM).

Finalista del Premi Cercle Fiber al millor Projecte Final de Carrera (curs 2010-2011), Castellano: Los esquemas conceptuales que se pueden encontrar en el estándar de salud HL7 están descritos utilizando un lenguaje de modelización propio, hecho que dificulta el trabajo de todas aquellas personas que lo utilizan. En este proyecto, se ha construido una herramienta que permite transformar, de forma automática, esos esquemas en otros descritos utilizando el lenguaje UML. De esta manera, se pueden utilizar herramientas que trabajan con UML tales como generadores de código, editores gráficos, etc. directamente sobre los modelos del estándar HL7.

Multidimensional models are at the core of data warehouse systems, since they allow decision makers to early define the relevant information and queries that are required to satisfy their information needs. The use of aggregation functions is a cornerstone in the definition of these multidimensional queries. However, current proposals for multidimensional modeling lack the mechanisms to define aggregation functions at the conceptual level: multidimensional queries can only be defined once the rest of the system has already been implemented, which requires much effort and expertise. In this sense, the goal of this paper is to extend the Object Constraint Language (OCL) with a predefined set of aggregation functions. Our extension facilitates the definition of platform-independent queries as part of the specification of the conceptual multidimensional model of the data warehouse. These queries are automatically implemented with the rest of the data warehouse during the code-generation phase. The OCL extensions proposed in this paper have been validated by using the USE tool.

The specification of a software system must include all relevant static and dynamic aspects of the domain. Dynamic aspects are usually specified by means of a behavioral schema consisting of a set of system operations that the user may execute to update the system state. To be useful, such a set must be complete (i.e. through these operations, users should be able to modify the population of all elements in the class diagram) and executable (i.e. for each operation, there must exist a system state over which the operation can be successfully applied). A manual specification of these operations is an error-prone and time-consuming activity. Therefore, the aim of this paper is to present a strategy for the automatic generation of a basic behavior schema. Operations in the schema are drawn from the static aspects of the domain as defined in the UML class diagram and take into account possible dependencies among them to ensure the completeness and executability of the operations.We believe our approach is especially useful in a Model-Driven Development setting, where the full implementation of the system is derived from its specification. In this context, our approach facilitates the definition of the behavioral specification and ensures its quality obtaining, as a result, an improved code generation phase., Peer Reviewed, Postprint (published version)

After sketching how system development and the UML (Unified Modeling Language) and the OCL (Object Constraint Language) are related, validation and verification with the tool USE (UML-based Specification Environment) is demonstrated. As a more efficient alternative for verification tasks, two approaches using SAT-based techniques are put forward: First, a direct encoding of UML and OCL with Boolean variables and propositional formulas, and second, an encoding employing an intermediate, higher-level language (KODKOD, stongly connected to ALLOY). A number of further, presently not realized verification and validation tasks and the transformation of higher-level modeling concepts into simple UML/OCL models, which are checkable with SAT-based techniques, are shortly discussed. Finally, the potential of SAT-based techniques for model development is again emphasized.

Šiame dokumente aprašytas darbas susideda iš keturių pagrindinių dalių. Pirmojoje, analitinėje dalyje, atlikome UML ir susijusių modeliavimo standartų analizę. Apžvelgėme populiariausius rinkoje egzistuojančius UML redaktorius ir jų stipriąsias puses. Aptarėme verslo šioje rinkoje galimybes. Antrojoje darbo dalyje apžvelgėme sukurtos sistemos funkcionalumą, architektūrinius sprendimus ir architektūros kokybinius kriterijus. Trečioje dalyje aprašomi kodo ir bibliotekų generavimo iš UML modelių galimybių tyrimai. Pateiktas siūlymas taikyti OCL išraiškas elementų savybių validavimui. Paskutinėje dalyje aprašomas sistemos, skirtos elementų savybių validavimo OCL apribojimų pagalba, realizacijos pagrindimas, pateikia. Taip pat pateikiamas eksperimentas, palyginantis sukompiliuotų ir sugeneruotų dinaminių klasių bibliotekų spartos charakteristikas., This document describes the work that consists of four main parts. Analysis of UML and related modeling standards was performed in the first – analytical – part. UML editors that are popular in the present market and their advantages were reviewed. The possibilities of making business in this area were discussed. The functionality, architectural solutions and architecture quality criteria of the developed system were reviewed in the second part of the work. Researches of possibilities of code and library generating from UML models are described in the third part of the work. The proposal to apply OCL expressions for element property validation was offered. The substantiation of realization of the system for element property validation by OCL restrictions is described in the last part of the work. The experiment that compares characteristics of the compiled dynamic class libraries speed and the generated dynamic class libraries speed is presented.

Darbe nagrinėjamas verslo taisyklių panaudojimas ir transformacijos, kurių realizacijomis sprendžiamos problemos, susijusios su verslo taisyklių sistemos formavimu ir modeliavimu. Darbe buvo aprašyta, kaip verslo taisykles, formaliai aprašytas ontologijoje, galima transformuoti į informacijos apdorojimo ir modeliavimo taisykles. Išnagrinėjus transformacijas aprašančią literatūrą, buvo nustatytos transformacijų kalbos, stiliai, tipai, įvairūs būdai, kaip transformacija gali būti atlikta. Transformacijos metodo realizacijai buvo atlikta verslo taisyklių ir ontologijos analizė. Darbe aprašytas metodas, kaip ontologijoje aprašytos verslo taisyklės, išreikštos aksiomomis, gali būti panaudotos informacinei sistemai formuoti: jos transformuojamos į informacijos apdorojimo taisykles, ADB SQL trigerius ir OCL ribojimus. Buvo atlikta lyginamoji ontologijų kūrimo priemonių analizė, kurios metu pasirinktas Protégé įrankis, kuris panaudotas pademonstruoti metodo efektyvumą ir naudą. Transformacijoms įgyvendinti naudota įrankiu sukurta laikraščio ontologija. Metodo realizacijai buvo sukurti Protégé įrankio plėtiniai „Axiom2SQL“ ir „Axiom2OCL“, kuriais galima atlikti automatizuotą ribojimų aksiomų išgavimą ir transformavimą į SQL trigerių prototipus ar OCL ribojimus. Darbą sudaro 5 dalys: įvadas, analitinė ir projektinė, išvados, literatūros sąrašas (bei 3 priedai). Darbo apimtis – 95 p. teksto be priedų, 20 pav., 10 lent., 35 bibliografiniai šaltiniai Atskirai pridedami darbo priedai., This thesis describes usage and transformations to solve problems associated with business rules system development and modeling. The thesis describes how formally described business rules of the ontology can be transformed into information processing and modeling rules. A result of literature analysis are described transformation languages, styles, types, various ways of transformation how can be made. For described transformation method business rules and ontology were analyzed. Thesis describes method how ontology based business rules, represented as axioms, can be transformed and applied for development of information system: business rules transformed into processing rules, ADBMS SQL triggers, and OCL constraints. After ontology development tools analysis Protégé tool was chosen to demonstrate the efficiency and usefulness of the suggested method. For realization of transformations was used ontology of Newspaper domain. The method is implemented as Protégé plug-ins “Axiom2SQL” and “Axiom2OCL”, which automatically performs mining of axioms and transformation into SQL trigger prototypes and OCL constraints. Structure: 5 parts: introduction, analytic and project, conclusions and references (and 3 appendixes). Thesis consists of: 95 p. text without appendixes, 20 pictures, 10 tables, 35 bibliographical entries. Appendixes included.

Current proposals for designing information systems lack the mechanisms to define statistical functions at the conceptual level. Therefore, queries containing these kind of functions are defined once the rest of the system has already been implemented, which requires much effort and expertise. In this sense, the goal of this paper is to show the benefits of extending the Object Constraint Language (OCL) with a predefined set of statistical functions.

Modeling of application domains that include requirements with vague terms may be a complex process because existing modeling tools are not conceived for that. Nevertheless, many real life applications and systems information requirements might involve natural language vague terms for the expression of user preferences. Some previous works in the field of databases add fuzzy logic for preferences expression in querying. In this work, we define a UML profile that allows visual modeling of information requirements involving vague linguistics terms, i.e., fuzzy requirements. The proposed profile is based on stereotypes and fuzzy logic extended to OCL. This profile has a formal semantic to avoid ambiguity, moreover it provides diagram representation. We illustrate our profile by means of a real-world case study showing the potential and simplicity of this proposal., Modelar dominios de aplicación que involucren requisitos con términos vagos puede ser un proceso complejo, debido a que las herramientas de modelado disponibles en la actualidad no están concebidas para ello. Sin embargo, muchos requisitos de información en sistemas y aplicaciones actuales podrían involucrar términos vagos del lenguaje natural que expresan las preferencias del usuario. Algunos esfuerzos previos se han hecho en el área de consultas a bases de datos incorporando la lógica difusa para la expresión de tales preferencias. En este trabajo, se define un perfil bajo UML que permite el modelado visual de requisitos de información basados en términos lingüísticos, ejemplo de ellos son los llamados requerimientos fuzzy o difusos. El perfil propuesto se basa en estereotipos y lógica difusa extendida extendido OCL (Object Constraint Language). Dicho perfil posee una semántica formal que permite eliminar ambigüedades, que puede ser representado gráficamente. Se ejemplifica la aplicación del perfil a través de un caso de estudio de la vida real que muestra la sencillez y potencialidad de su uso.

Conceptual Schemas are one of the most important artifacts in the development cycle of information systems. To understand the conceptual schema is essential to get involved in the information system that is described within it. As the information system increases its size and complexity, the relative conceptual schema will grow in the same proportion making di cult to understand the main concepts of that schema/information system. The thesis comprises the investigation of the in uence of the whole schema in computing the relevance of schema elements. It will include research and implementation of algorithms for scoring elements in the literature, an study of the di erent results obtained once applied to a few example conceptual schemas, an extension of those algorithms including new components in the computation process like derivation rules, constraints and the behavioural subschema speci cation, and an in-depth comparison among the initial algorithms and the extended ones studying the results in order to choose those algorithms that give the most valuable output.