Electronic Communications of the EASST (European Association of Software Science and Technology)
Not a member yet
887 research outputs found
Sort by
Rule-Based Integration of Domain-Specific Modelling Languages
Get PDFDomain-specific modelling languages (DSMLs) can increase the acceptance of (semi-)formal modelling techniques. They allow all stakeholders in an application domain to participate in the modelling process using notations that are close to their understanding of the domain. When several groups of stakeholders are concerned with a certain aspect of the modelled system, the question arises how different DSMLs can be integrated with respect to this aspect. In this paper, we
propose rule-based transformations as a means to integrate heterogeneous DSMLs overlapping on dedicated aspects. We illustrate the approach by a running example of a small visual DSML for IT landscapes and a textual DSML for firewall configurations
Checking Consistency Between Message Choreographies And Their Implementation Models
Get PDFApplying the concepts of Service-Oriented Architectures (SOA) has already become a mainstream in industry. The development of business applications according to these principles implies a layered design and implementation. This paper describes an industrial approach to the verification of a consistency relation between such layers. In our case service choreographies defined by Message Choreography
Models (MCM) and their corresponding implementation models
represented as Business Objects are examined. By translating both into Event-B specifications we are able to prove the consistency relation between them. A number of case studies with realistic industrial software models were carried out which showed the solidness of our verification technique. Apart from giving details about our concrete realization, this paper also discusses general challenges that have to be faced when developing a verification approach applicable for the real-world systems
Construction of Pushout Complements in the Category of Hypergraphs
Get PDFWe describe a concrete construction of all pushout complements for two given morphisms f : A -> B, m: B -> D in the category of hypergraphs, valid also for the case where f, m are non-injective. It is based on the generation of suitable equivalence relations. We also give a combinatorial interpretation and show how well-known coefficients from combinatorics, such as the Bell numbers, can be recovered. Furthermore we present a formula that can be used to compute the number of pushout complements for two given morphisms
Preface (OCL 2011 Proceedings)
No full textThis preface reports on the 11th workshop on OCL and Textual Modelling held at the TOOLS Federated Conferences in 2011. The workshop focused on the current state of OCL (standard, tool support, adoption, ...) and the application of textual modelling to different domains. The workshop included presentations
together with a discussion session. All the workshop materials are available at http://gres.uoc.edu/OCL2011
Patterns of Federated Identity Management Systems as Architectural Reconfigurations
Get PDFThis paper proposes a formal model of Federated Identity Management systems (FIMs) in terms of architectural design rewriting. FIMs allow cross-domain user authentication to enable access control across the organisations under the concept known as Circle of Trust (CoT). Patterns of FIMs emerged as recurring CoT scenarios due to the fact that each of the pattern has different security and trust requirements. This paper proposes a formal model for FIMs to characterise their patterns as architectural styles. More precisely, an architectural style is given to precisely pinpoint all possible legal configurations of the CoT in terms of the patterns. The proposed model is specified through style-consistent (graphical) designs in terms of architectural design rewriting (ADR)
Dynamic Validation of OCL Constraints with mOdCL
Get PDFThis paper presents mOdCL, a Maude based evaluator of OCL
expressions and validator of OCL constraints. Given its OCL
expression evaluator, the use of execution strategies allows mOdCL, not only validating invariant constraints on concrete system states, but also dynamically validating invariants and pre- and post-conditions on the successive states obtained during system
execution