Abstract Logical puzzles can be important factors for the development of rational analysis and application capabilities for pupils and students. Therefore, logical puzzles can also take a prominent supporting role in computer science education. This contribution proposes a UML class model with accompanying OCL constraints for developing logical puzzles. The class model acts as a metamodel for the description of the basic puzzle organization and the logical clues presented to the learners. The constraints express, for example, statements about uniqueness of solutions, and the degree of puzzle complexity may be tuned by appropriate model elements. Given a puzzle specification which simply comprises the domain elements of the puzzle plus constraints, our implementation uses a UML and OCL solver to construct a puzzle instance (i.e., a set of clues and solutions) automatically. The puzzle is made playable by a graphical user interface. We have validated this approach for developing puzzles by building several puzzles from the literature of increasing complexity and performed a student survey.

Abstract At its core, OCL as currently defined is a first-order functional language: its expressions evaluate to single values, with collections accounting for multitudes of values, and special values and for partiality. By contrast, the data model providing the context of OCL expressions is inherently relational: the associations of UML class diagrams are essentially relations, with uniqueness and order designators extending expressiveness to ordered multirelations. As a result, OCL suffers from a functional/relational impedance mismatch, which is only superficially addressed by its navigation shorthands. At the same time, OCL is inherently unsafe: expressions containing subexpressions evaluating to may be invalid, translating to a runtime error in programming languages. We address this situation by turning OCL into a relational language that retains most of OCL’s original syntax and semantics, yet revises its fundamental design decisions that lead up to the noted problems. In particular, our version of OCL, which we call OCL $${^\sharp }$$ ♯ , is type-safe.

In order to achieve effective support for software development, the transition between an informal and provisional mode of tool operation, which is conducive to design exploration, and a formal mechanistic mode required for computer-based design capture is crucial. This contribution proposes a smooth transition for designing class models starting from informal, sketchy object models. We propose a lenient development approach and discuss the possibilities and problems of a transformation from object diagrams to class diagrams. While classes describe abstract concepts, objects are representations of what can be seen in the real world, so it might be easier to start modeling with objects instead of classes. An object diagram can however not describe a whole system, it is only used as the first step of an iterative process to create a complete model. During this process, our object and class diagrams provide a notation for highlighting missing or conflicting parts. Based on these imperfect object diagrams, educated guesses can be made for resulting, imperfect class diagrams, which can then be refined to a complete, formal description of the modeled system.

Testing system behavior in real world applications often requires analyzing properties over multiple system states to ensure that operations do not interfere with each other in ways that are not desired. In UML class diagrams, behavior is specified using operations with pre-and postconditions, which alone are not sufficient to formulate temporal properties spanning multiple system states and, thus, require additional description means. For this purpose, multiple extensions of OCL with linear temporal logic (LTL) exist, which provide a formalism to describe temporal properties. Using so-called filmstrip models, this paper provides formal semantics for OCL enhanced by LTL through a translation into standard OCL on the basis of class diagrams and enables verifying these temporal properties using existing model checking tools.

Since its release in 2004, Ruby on Rails has evolved into a widely used full stack model-view-controller (MVC) framework. But despite the fact, that Rails (short for Ruby on Rails) is also used for developing enterprise-scale applications like Github or scientific tools like QTREDS, there is no official support for graphical modelling. This paper introduces a proposal to fill this gap by suggesting a model driven approach using the free yEd diagram editor as well as a specifically developed transformation tool and ER dialect. The implementation is based on the Rails data abstraction layer ActiveRecord and its provided domain specific languages.

This contribution proposes a new technique for developing test cases for UML and OCL models. The technique is based on an approach that automatically constructs object models for class models enriched by OCL constraints. By guiding the construction process through so-called classifying terms, the built test cases in form of object models are classified into equivalence classes. A classifying term can be an arbitrary OCL term on the class model that calculates for an object model a characteristic value. From each equivalence class of object models with identical characteristic values one representative is chosen. The constructed test cases behave significantly different with regard to the selected classifying term. By building few diverse object models, properties of the UML and OCL model can be explored effectively. The technique is applied for automatically constructing relevant source model test cases for model transformations between a source and target metamodel.

In behavioral modeling, operation contracts defined by pre- and postconditions describe the effects on model properties (i.e., model elements such as attributes, links, etc.) that are enforced by an operation. However, it is usually omitted which model properties should not be modified. Defining so-called frame conditions can fill this gap. But, thus far, these have to be defined manually - a time-consuming task. In this work, we propose a methodology which aims to support the modeler in the definition of the frame conditions by extracting suggestions based on an automatic analysis of operation contracts provided in OCL. More precisely, the proposed approach performs a structural analysis of pre- and postconditions together with invariants in order to categorize which class and object properties are clearly “variable” or “unaffected” - and which are “ambiguous”, i.e. indeed require a more thorough inspection. The developed concepts are implemented as a prototype and evaluated by means of several example models known from the literature.

The paper introduces a new, comprehensive integrated conceptual data model in a precise way. Central language features cover core modeling concepts as classification, membership, inheritance, interfaces, structured types, aliasing, aggregation, composition, constraints, clustering and relationships. Schema states are thought of as being realized as graphs with appropriate navigation options. A prototypical graph database implementation and accompanying examples are discussed.

The use of modeling languages such as UML or SysML enables to formally specify and verify the behavior of digital systems already in the absence of a specific implementation. However, for each modeling method and verification task usually a separate verification solution has to be applied today. In this paper, a methodology is envisioned that aims at stopping this “inflation” of different verification approaches and instead employs a generic methodology. For this purpose, a given specification as well as the verification shall be transformed into a basic model which itself is specified by means of a generic modeling language. Then, a range of automatic reasoning engines shall uniformly be applied to perform the actual verification. A feasibility study demonstrates the applicability of the envisioned approach.

The stringent security requirements of organisations like banks or hospitals frequently adopt role-based access control (RBAC) principles to represent and simplify their internal permission management. While representing a fundamental advanced RBAC concept enabling precise restrictions on access rights, authorisation constraints increase the complexity of the resulting security policies so that tool support for convenient creation and adequate validation is required. A particular contribution of our work is a new approach to developing and analysing RBAC policies using a UML-based domain-specific language (DSL), which allows the hiding of the mathematical structures of the underlying authorisation constraints implemented in OCL. The DSL we present is highly configurable and extensible with respect to new concepts and classes of authorisation constraints, and allows the developer to validate RBAC policies in an effective way. The handling of dynamic (that is, time-dependent) constraints, their visual representation through the RBAC DSL and their analysis all form another part of our contribution. The approach is supported by a UML and OCL validation tool.

In this paper, we present a UML metamodel-based approach for creating and executing workflow models. The workflow modeling language is introduced through its abstract syntax, and an evaluation shows how this language supports known workflow patterns. Some patterns can be expressed easier compared to established languages like EPCs or BPMN. Organizational and data aspects in workflow models can be described on the basis of the presented metamodel. The workflow models can be instantiated and executed with a tool realizing parts of the UML action semantics. At an early stage of design, our workflow models can be evaluated by testing scenarios with the used tool in combination with the developed workflow plug in. Employing the tool, dynamic aspects of the workflow process models together with data and organizational aspects can be evaluated. During execution of the workflow scenarios, the workflow models can be adaptively changed, and data can be captured and evaluated by formulating process mining queries with UML's OCL (Object Constraint Language).

Nowadays, modeling languages like UML are essential in the design of complex software systems and also start to enter the domain of hardware and hardware/software codesign. Due to shortening time-to-market demands, ¿first time right¿ requirements have thereby to be satisfied. In this paper, we propose an approach that makes use of Boolean satisfiability for verifying UML/OCL models. We describe how the respective components of a verification problem, namely system states of a UML model, OCL constraints, and the actual verification task, can be encoded and afterwards automatically solved using an off-the-shelf SAT solver. Experiments show that our approach can solve verification tasks significantly faster than previous methods while still supporting a large variety of UML/OCL constructs.

Presenting precisely models and supporting automatic manipulation of models are at the heart of model-centric software development. A formal foundation for these tasks is a necessity as well as a challenge. We present a model-driven approach based on the integration of two light-weight formal methods, the object constraint language (OCL) and triple graph grammars (TGGs). OCL together with metamodeling allows us to present precisely models. With TGGs we can carry out model manipulations, especially model transformations. We focus on explaining the tool which realizes our approach. This tool is developed as an extension of the UML-based specification environment (USE), which offers full OCL support. A case study showing the transformation between statecharts and extended hierarchical automata explains our approach.

Abstract This paper describes the Mondex case study with UML class diagrams and restricting OCL constraints. The constraints have been formulated either as OCL class invariants or as OCL pre- and postconditions. The proposed two models include UML class diagrams and OCL constraints which have been checked by the UML and OCL tool USE (UML-based Specification Environment). USE allows validation of a model by testing it with scenarios. The Mondex case study has been validated by positive and negative test cases. The test cases allow the validity of the various constraints to be traced and checked. Validation results are presented as textual protocols or as UML sequence diagrams where starting, intermediate, and resulting system states are represented by UML object diagrams. UML sequence diagrams, UML object diagrams, and textual protocols are shown with varying degrees of detail for the attributes, constraints, and executed commands.

Today more and more security-relevant data is stored on computer systems; security-critical business processes are mapped to their digital counterparts. This situation applies to various domains such as health care industry, digital government, and financial service institutes requiring that different security requirements must be fulfilled. Authorisation constraints can help the policy architect design and express higher-level organisational rules. Although the importance of authorisation constraints has been addressed in the literature, there does not exist a systematic way to verify and validate authorisation constraints. In this paper, we specify both non-temporal and history-based authorisation constraints in the Object Constraint Language (OCL) and first-order linear temporal logic (LTL). Based upon these specifications, we attempt to formally verify role-based access control policies with the help of a theorem prover and to validate policies with the USE system, a validation tool for OCL constraints. We also describe an authorisation engine, which supports the enforcement of authorisation constraints.

Different approaches support the construction of software by representing certain aspects of a system graphically. Recently, the UML has become common to provide software designers with tools, in which they can create visual representations of software interactively. But the UML is intended to be drawn on two-dimensional surfaces. Our approach extends UML into a third and fourth dimension in a way that we can place both static and dynamic aspects in one single view. By this, we can show behavior in the context of structural aspects, instead of drawing different diagrams for each aspect with only loose relation to each other. We also use the third dimension to emphasize important things and to place less interesting things in the background. Thereby, we direct the viewer's attention to the important things in the foreground. Currently, UML shows dynamic behavior by diagrams which do not change and are therefore static in nature. In sequence diagrams, for example, time elapses from the top of the diagram to the bottom. We point out that behavior is better visualized by animated diagrams where message symbols move from the sender object to the receiver object. Our approach supports the creation of a system as well as the communication of its dynamic processes especially to customers.

One of the central tasks in developing information systems is the specification of desired system properties. We use the object specification language TROLL light to formalize the conceptual model of a system. A TROLL light specification describes structural as well as dynamic characteristics of objects representing real world entities. For validating specifications, we have developed an animation tool, allowing us to reflect structural properties and dynamic behaviour. The main concepts of the animator are illustrated by a working example. We present a simple specification of a car rental company and describe some of the steps performed during a typical animation session. The animation allows us to check whether desired properties are fulfilled by the given object descriptions. Finally, some design and implementation issues regarding the utilized persistent programming environment and the Web based user interface are discussed.

A single pushout approach to the transformation of attributed partial graphs based on categories of partial algebras and partial morphisms is introduced. A sufficient condition for pushouts in these categories is presented. As the synchronization mec

Techniques for the development of reliable information systems on the basis of their formal specification are the main concern in the project. Our work focuses on the specification language TROLL light which allows one to describe the part of the world to be modeled as a community of concurrently existing and communicating objects. Our specification language comes with an integrated, open development environment. The task of this environment is to give support for the creation of correct information systems. Two important ingredients of the environment are the animator and the proof support system.>

Within the compound project KorSo our team is concerned with the research on techniques and methods for the development of reliable information systems on the basis of formal specifications. Our work focuses on the specification language TROLL light which allows to describe the part of the world which is to be modeled as a community of concurrently existing and communicating objects by determining their structure as well as their behavior. Moreover we develop and implement a computer aided specification environment for TROLL light which permits a prototyping animation as well as the proof of properties of specifications. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Nearly all query languages discussed recently for the Entity-Relationship (ER) model do not possess a formal semantics. Languages are often defined by means of examples only. The reason for this phenomenon is the essential gap between features of query languages and theoretical foundations like algebras and calculi. Known languages offer arithmetic capabilities and allow for aggregates, but algebras and calculi defined for ER models do not. This paper introduces an extended ER model concentrating nearly all concepts of known so-called semantic data models in a few syntactical constructs. Moreover, we provide our extended ER model with a formal mathematical semantics. On this basis a well-founded calculus is developed taking into account data operations on arbitrary user-defined data types and aggregate functions. We pay special attention to arithmetic operations, as well as multivalued terms allowing nested queries, in a uniform and consistent manner. We prove our calculus only allows the formulation of safe terms and queries yielding a finite result, and to be (at least) as expressive as the relational calculi.