DROPS

Document

DOI: 10.4230/LIPIcs.CSL.2026.23

A Logic for Fresh Labelled Transition Systems

Authors: Mohamed H. Bandukara and Nikos Tzevelekos

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract

We introduce a Hennessy-Milner logic with recursion for Fresh Labelled Transition Systems (FLTSs). These are nominal labelled transition systems which keep track of the history, i.e. of data values seen so far, and can model fresh data generation. In particular, FLTSs generalise the computations of Fresh-Register Automata, which in turn can be seen as a "regular" class of history-tracking automata operating on infinite input alphabets. The logic we introduce is a modal mu-calculus equipped with infinite disjunctions over arbitrary and fresh data values respectively, while its recursion is parameterised on vectors of data values. It can express a variety of properties, such as the existence of an infinite path of distinct data values, the absence of paths where values are repeated, or the existence of a finite path where some taint property is violated. We study the model-checking problem and its complexity via a reduction to parity games and, using nominal sets techniques, provide an exponential upper bound for it.

Cite as

Mohamed H. Bandukara and Nikos Tzevelekos. A Logic for Fresh Labelled Transition Systems. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 23:1-23:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{bandukara_et_al:LIPIcs.CSL.2026.23,
  author =	{Bandukara, Mohamed H. and Tzevelekos, Nikos},
  title =	{{A Logic for Fresh Labelled Transition Systems}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{23:1--23:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.23},
  URN =		{urn:nbn:de:0030-drops-254478},
  doi =		{10.4230/LIPIcs.CSL.2026.23},
  annote =	{Keywords: Nominal Transition Systems, Hennessy-Milner Logic, Modal Mu-Calculus, Register Automata, Nominal Sets, Parity Games}
}

Document

DOI: 10.4230/LITES.8.2.4

A Hybrid Programming Language for Formal Modeling and Verification of Hybrid Systems

Authors: Eduard Kamburjan, Stefan Mitsch, and Reiner Hähnle

Published in: LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2

Abstract

Designing and modeling complex cyber-physical systems (CPS) faces the double challenge of combined discrete-continuous dynamics and concurrent behavior. Existing formal modeling and verification languages for CPS expose the underlying proof search technology. They lack high-level structuring elements and are not efficiently executable. The ensuing modeling gap renders formal CPS models hard to understand and to validate. We propose a high-level programming-based approach to formal modeling and verification of hybrid systems as a hybrid extension of an Active Objects language. Well-structured hybrid active programs and requirements allow automatic, reachability-preserving translation into differential dynamic logic, a logic for hybrid (discrete-continuous) programs. Verification is achieved by discharging the resulting formulas with the theorem prover KeYmaera X. We demonstrate the usability of our approach with case studies.

Cite as

Eduard Kamburjan, Stefan Mitsch, and Reiner Hähnle. A Hybrid Programming Language for Formal Modeling and Verification of Hybrid Systems. In LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2, pp. 04:1-04:34, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{kamburjan_et_al:LITES.8.2.4,
  author =	{Kamburjan, Eduard and Mitsch, Stefan and H\"{a}hnle, Reiner},
  title =	{{A Hybrid Programming Language for Formal Modeling and Verification of Hybrid Systems}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{04:1--04:34},
  ISSN =	{2199-2002},
  year =	{2022},
  volume =	{8},
  number =	{2},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES.8.2.4},
  URN =		{urn:nbn:de:0030-drops-192965},
  doi =		{10.4230/LITES.8.2.4},
  annote =	{Keywords: Active Objects, Differential Dynamic Logic, Hybrid Systems}
}

Document

DOI: 10.4230/DagRep.8.12.1

Multidirectional Transformations and Synchronisations (Dagstuhl Seminar 18491)

Authors: Anthony Cleve, Ekkart Kindler, Perdita Stevens, and Vadim Zaytsev

Published in: Dagstuhl Reports, Volume 8, Issue 12 (2019)

Abstract

Bidirectional transformations (bx) are a mechanism for maintaining the consistency of two (or more) related sources of information, such as models in model-driven development, database schemas, or programs. Bx technologies have been developed for practical engineering purposes in many diverse fields. Different disciplines such as programming languages, graph transformations, software engineering, and databases have contributed to the concepts and theory of bx. However, so far, most efforts have been focused on the case where exactly two information sources must be kept consistent; the case of more than two has usually been considered as an afterthought. In many practical scenarios, it is essential to work with more than two information sources, but the community has hardly started to identify and address the research challenges that this brings. Driven by the practical needs and usage scenarios from industry, this Dagstuhl Seminar aimed to identify the challenges, issues and open research problems for multidirectional model transformations and synchronisations and sketch a road map for developing relevant concepts, theories and tools. The report contains an executive summary of the seminar, reports from its working groups, as well as descriptions of industrial and academic case studies that motivated the discussions.

Cite as

Anthony Cleve, Ekkart Kindler, Perdita Stevens, and Vadim Zaytsev. Multidirectional Transformations and Synchronisations (Dagstuhl Seminar 18491). In Dagstuhl Reports, Volume 8, Issue 12, pp. 1-48, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@Article{cleve_et_al:DagRep.8.12.1,
  author =	{Cleve, Anthony and Kindler, Ekkart and Stevens, Perdita and Zaytsev, Vadim},
  title =	{{Multidirectional Transformations and Synchronisations (Dagstuhl Seminar 18491)}},
  pages =	{1--48},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2019},
  volume =	{8},
  number =	{12},
  editor =	{Cleve, Anthony and Kindler, Ekkart and Stevens, Perdita and Zaytsev, Vadim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.8.12.1},
  URN =		{urn:nbn:de:0030-drops-103606},
  doi =		{10.4230/DagRep.8.12.1},
  annote =	{Keywords: bidirectional transformation, synchronisation}
}

Document

DOI: 10.4230/DagRep.1.1.42

Bidirectional Transformation "bx" (Dagstuhl Seminar 11031)

Authors: Zhenjiang Hu, Andy Schürr, Perdita Stevens, and James Terwilliger

Published in: Dagstuhl Reports, Volume 1, Issue 1 (2011)

Abstract

Bidirectional transformations bx are a mechanism for maintaining the consistency of two (or more) related sources of information. Researchers from many different areas of computer science including databases (DB), graph transformations (GT), software engineering (SE), and programming languages (PL) are actively investigating the use of bx to solve a diverse set of problems. Although researchers have been actively working on bidirectional transformations in the above mentioned communities for many years already, there has been very little cross-discipline interaction and cooperation so far. The purpose of a first International Meeting on Bidirectional Transformations (GRACE-BX), held in December 2008 near Tokyo, was therefore to bring together international elites, promising young researchers, and leading practitioners to share problems, discuss solutions, and open a dialogue towards understanding the common underpinnings of bx in all these areas. While the GRACE-BX meeting provided a starting point for exchanging ideas in different communities and confirmed our believe that there is a considerable overlap of studied problems and developed solutions in the identified communities, the Dagstuhl Seminar 11031 on ``Bidirectional Transformations'' also aimed at providing a place for working together to define a common vocabulary of terms and desirable properties of bidirectional transformations, develop a suite of benchmarks, solve some challenging problems, and launch joint efforts to form a living bx community of cooperating experts across the identified subdisciplines. This report documents the program and the outcomes of Dagstuhl Seminar 11031 with abstracts of tutorials, working groups, and presentations on specific research topics.

Cite as

Zhenjiang Hu, Andy Schürr, Perdita Stevens, and James Terwilliger. Bidirectional Transformation "bx" (Dagstuhl Seminar 11031). In Dagstuhl Reports, Volume 1, Issue 1, pp. 42-67, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@Article{hu_et_al:DagRep.1.1.42,
  author =	{Hu, Zhenjiang and Sch\"{u}rr, Andy and Stevens, Perdita and Terwilliger, James},
  title =	{{Bidirectional Transformation "bx" (Dagstuhl Seminar 11031)}},
  pages =	{42--67},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2011},
  volume =	{1},
  number =	{1},
  editor =	{Hu, Zhenjiang and Sch\"{u}rr, Andy and Stevens, Perdita and Terwilliger, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.1.1.42},
  URN =		{urn:nbn:de:0030-drops-31442},
  doi =		{10.4230/DagRep.1.1.42},
  annote =	{Keywords: Bidirectional Languages, Transformation, Model/Data Synchronisation}
}

Document

DOI: 10.4230/DagSemProc.06351.1

06351 Abstracts Collection – Methods for Modelling Software Systems (MMOSS)

Authors: Ed Brinksma, David Harel, Angelika Mader, Perdita Stevens, and Roel Wieringa

Published in: Dagstuhl Seminar Proceedings, Volume 6351, Methods for Modelling Software Systems (MMOSS) (2007)

Abstract

From 27.08.06 to 01.09.06, the Dagstuhl Seminar 06351 ``Methods for Modelling Software Systems (MMOSS)'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.

Cite as

Ed Brinksma, David Harel, Angelika Mader, Perdita Stevens, and Roel Wieringa. 06351 Abstracts Collection – Methods for Modelling Software Systems (MMOSS). In Methods for Modelling Software Systems (MMOSS). Dagstuhl Seminar Proceedings, Volume 6351, pp. 1-17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{brinksma_et_al:DagSemProc.06351.1,
  author =	{Brinksma, Ed and Harel, David and Mader, Angelika and Stevens, Perdita and Wieringa, Roel},
  title =	{{06351 Abstracts Collection – Methods for Modelling Software Systems (MMOSS)}},
  booktitle =	{Methods for Modelling Software Systems (MMOSS)},
  pages =	{1--17},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{6351},
  editor =	{Ed Brinksma and David Harel and Angelika Mader and Perdita Stevens and Roel Wieringa},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06351.1},
  URN =		{urn:nbn:de:0030-drops-9586},
  doi =		{10.4230/DagSemProc.06351.1},
  annote =	{Keywords: Modelling Methods, Design Models, Verification Models, Problem-solution co-refinement}
}

Document

DOI: 10.4230/DagSemProc.06351.2

06351 Summary – Methods for Modelling Software Systems (MMOSS)

Authors: Ed Brinksma, David Harel, Angelika Mader, Perdita Stevens, and Roel Wieringa

Published in: Dagstuhl Seminar Proceedings, Volume 6351, Methods for Modelling Software Systems (MMOSS) (2007)

Abstract

We survey the key objectives and the structure of this Dagstuhl seminar, and discuss common themes that emerged.

Cite as

Ed Brinksma, David Harel, Angelika Mader, Perdita Stevens, and Roel Wieringa. 06351 Summary – Methods for Modelling Software Systems (MMOSS). In Methods for Modelling Software Systems (MMOSS). Dagstuhl Seminar Proceedings, Volume 6351, pp. 1-4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{brinksma_et_al:DagSemProc.06351.2,
  author =	{Brinksma, Ed and Harel, David and Mader, Angelika and Stevens, Perdita and Wieringa, Roel},
  title =	{{06351 Summary – Methods for Modelling Software Systems (MMOSS)}},
  booktitle =	{Methods for Modelling Software Systems (MMOSS)},
  pages =	{1--4},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{6351},
  editor =	{Ed Brinksma and David Harel and Angelika Mader and Perdita Stevens and Roel Wieringa},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06351.2},
  URN =		{urn:nbn:de:0030-drops-9574},
  doi =		{10.4230/DagSemProc.06351.2},
  annote =	{Keywords: Modelling Methods, Design Models, Verification Models, Problem-solution co-refinement}
}

Document

DOI: 10.4230/DagSemProc.06351.3

A Framework for Analyzing Composition of Security Aspects

Authors: Jorge Fox and Jan Juerjens

Published in: Dagstuhl Seminar Proceedings, Volume 6351, Methods for Modelling Software Systems (MMOSS) (2007)

Abstract

The methodology of aspect-oriented software engineering has been proposed to factor out concerns that are orthogonal to the core functionality of a system. In particular, this is a useful approach to handling the difficulties of integrating non-functional requirements such as security into complex software systems. Doing so correctly and securely, however, still remains a non-trivial task. For example, one has to make sure that the "weaving" process actually enforces the aspects needed. This is highly non-obvious especially in the case of security, since different security aspects may actually contradict each other, in which case they cannot be woven in a sequential way without destroying each other. To address these problems, this paper introduces a framework for the aspect-oriented development of secure software using composition filters at the model level. Using an underlying foundation based on streamprocessing functions, we explore under which conditions security properties are preserved when composed as filters. Thanks to this foundation we may also rely on model level verification tools and on code and model weaving to remedy security failures. Our approach is explained using as case-studies a web banking application developed by a major German bank and a webstore design.

Cite as

Jorge Fox and Jan Juerjens. A Framework for Analyzing Composition of Security Aspects. In Methods for Modelling Software Systems (MMOSS). Dagstuhl Seminar Proceedings, Volume 6351, pp. 1-25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{fox_et_al:DagSemProc.06351.3,
  author =	{Fox, Jorge and Juerjens, Jan},
  title =	{{A Framework for Analyzing Composition of Security Aspects}},
  booktitle =	{Methods for Modelling Software Systems (MMOSS)},
  pages =	{1--25},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{6351},
  editor =	{Ed Brinksma and David Harel and Angelika Mader and Perdita Stevens and Roel Wieringa},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06351.3},
  URN =		{urn:nbn:de:0030-drops-8594},
  doi =		{10.4230/DagSemProc.06351.3},
  annote =	{Keywords: Aspects in software engineering, aspect interference, verification, semantics, formal methods}
}

Document

DOI: 10.4230/DagSemProc.06351.4

A Model-Based Approach To Requirements Analysis

Authors: Bernhard Schätz, Eva Geisberger, and Johannes Grünbauer

Published in: Dagstuhl Seminar Proceedings, Volume 6351, Methods for Modelling Software Systems (MMOSS) (2007)

Abstract

A major task in designing embedded systems is the systematic elaboration of functional system requirements and their integration into the environment of the complete technical system. The main challenge is to handle the versatile tasks of coordinating a definition of behavior, which is appropriate to the problem. The problem- and design-specifications of the customer related product definition have to be adjusted with and integrated into the manifold requirements of the technical system design. Accordingly, the model-based requirements analysis and system-definition presented here defines a well-structured modeling approach, which systematically aids the goal-oriented formulation and adjustment of the different stakeholder-requirements with the aid of views onto the system and descriptive specification techniques. Thus it allows a clear specification of a consistent and complete system design. The central steps of this approach are implemented in a requirements management (RM) tool prototype called AutoRAID

Cite as

Bernhard Schätz, Eva Geisberger, and Johannes Grünbauer. A Model-Based Approach To Requirements Analysis. In Methods for Modelling Software Systems (MMOSS). Dagstuhl Seminar Proceedings, Volume 6351, pp. 1-9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{schatz_et_al:DagSemProc.06351.4,
  author =	{Sch\"{a}tz, Bernhard and Geisberger, Eva and Gr\"{u}nbauer, Johannes},
  title =	{{A Model-Based Approach To Requirements Analysis}},
  booktitle =	{Methods for Modelling Software Systems (MMOSS)},
  pages =	{1--9},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{6351},
  editor =	{Ed Brinksma and David Harel and Angelika Mader and Perdita Stevens and Roel Wieringa},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06351.4},
  URN =		{urn:nbn:de:0030-drops-8663},
  doi =		{10.4230/DagSemProc.06351.4},
  annote =	{Keywords: Requirements, model-based, tool support}
}

Document

DOI: 10.4230/DagSemProc.06351.5

A Taxonomy of Aspects in Terms of Crosscutting Concerns

Authors: Jorge Fox

Published in: Dagstuhl Seminar Proceedings, Volume 6351, Methods for Modelling Software Systems (MMOSS) (2007)

Abstract

Aspect-orientation provides support for " Separation of Concerns" by means of techniques that first isolate and then weave concerns. Most work in aspect-orientation has achieved such goals at the programming level, even also at the modeling level. Though, in some cases the application of these techniques is independent of the problem itself. In other words, the techniques for weaving either code or models are in principle applicable to a number of problems without a clear criterion to answer questions like: in what software processes we may actually discuss aspect-orientation? This also brings other questions: what do we consider an aspect?, how do we deal with it?, are aspects crosscutting concerns? The first notions of aspect-orientation relate to crosscutting in code. We consider this a bottom-up approach. We believe though, that aspect-orientation can be better understood from an architectural perspective. We call this a top-down approach. We explore the question of ''what makes an aspect an aspect" and '' when do aspects arise" from a top-down perspective. This work relates to a definition of aspects in terms of requirements traceability, proposes a classification, and altogether a taxonomy.

Cite as

Jorge Fox. A Taxonomy of Aspects in Terms of Crosscutting Concerns. In Methods for Modelling Software Systems (MMOSS). Dagstuhl Seminar Proceedings, Volume 6351, pp. 1-27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{fox:DagSemProc.06351.5,
  author =	{Fox, Jorge},
  title =	{{A Taxonomy of Aspects in Terms of Crosscutting Concerns}},
  booktitle =	{Methods for Modelling Software Systems (MMOSS)},
  pages =	{1--27},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{6351},
  editor =	{Ed Brinksma and David Harel and Angelika Mader and Perdita Stevens and Roel Wieringa},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06351.5},
  URN =		{urn:nbn:de:0030-drops-8603},
  doi =		{10.4230/DagSemProc.06351.5},
  annote =	{Keywords: Aspect-orientation, Software Engineering, Taxonomy}
}

Document

DOI: 10.4230/DagSemProc.06351.6

Model Development in the UML-based Specification Environment (USE)

Authors: Martin Gogolla

Published in: Dagstuhl Seminar Proceedings, Volume 6351, Methods for Modelling Software Systems (MMOSS) (2007)

Abstract

The tool USE (UML-based Specification Environment) supports analysts, designers and developers in executing UML models and checking OCL constraints and thus enables them to employ model-driven techniques for software production. USE has been developed since 1998 at the University of Bremen. This paper will discuss to what extent and how USE relates to the questions and topics (Model quality, Modelling method, Model Effectiveness, Model Maintainability) raised for this seminar.

Cite as

Martin Gogolla. Model Development in the UML-based Specification Environment (USE). In Methods for Modelling Software Systems (MMOSS). Dagstuhl Seminar Proceedings, Volume 6351, pp. 1-3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{gogolla:DagSemProc.06351.6,
  author =	{Gogolla, Martin},
  title =	{{Model Development in the  UML-based Specification Environment (USE)}},
  booktitle =	{Methods for Modelling Software Systems (MMOSS)},
  pages =	{1--3},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{6351},
  editor =	{Ed Brinksma and David Harel and Angelika Mader and Perdita Stevens and Roel Wieringa},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06351.6},
  URN =		{urn:nbn:de:0030-drops-8613},
  doi =		{10.4230/DagSemProc.06351.6},
  annote =	{Keywords: UML, OCL, Model-Driven Development, Validation, Animation, Model Execution,}
}

Document

DOI: 10.4230/DagSemProc.06351.7

Model Transformation Technologies in the Context of Modelling Software Systems

Authors: Óscar Pastor

Published in: Dagstuhl Seminar Proceedings, Volume 6351, Methods for Modelling Software Systems (MMOSS) (2007)

Abstract

Programming technologies have improved continuously during the last decades, but from an Information Systems perspective, some well-known problems associated to the design and implementation of an Information Systems persists. Object-Oriented Methods, Formal Specification Languages, Component-Based Software Production... This is just a very short list of technologies proposed to solve a very old and, at the same time, very well-known problem: how to produce software of quality. Programming has been the key task during the last 40 years, and the results have not been successful yet. This work will explore the need of facing a sound software production process from a different perspective: the non-programming perspective, where by non-programming we mainly mean modeling. Instead of talking about Extreme Programming, we will introduce a Extreme Non-Programming (Extreme Modeling-Oriented) approach. We will base our ideas on the intensive work done during the last years, oriented to the objective of generating code from a higher-level system specification, normally represented as a Conceptual Schema. Nowadays, though, the hip around MDA has given a new push to these strategies. New methods propose sound model transformations which cover all the different steps of a sound software production process from an Information Systems Engineering point of view. This must include Organizational Modeling, Requirements Engineering, Conceptual Modeling and Model-Based Code Generation techniques. In this context, it seems that the time of Model Transformation Technologies is finally here...

Cite as

Óscar Pastor. Model Transformation Technologies in the Context of Modelling Software Systems. In Methods for Modelling Software Systems (MMOSS). Dagstuhl Seminar Proceedings, Volume 6351, pp. 1-15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{pastor:DagSemProc.06351.7,
  author =	{Pastor, \'{O}scar},
  title =	{{Model Transformation Technologies in the Context of Modelling Software Systems}},
  booktitle =	{Methods for Modelling Software Systems (MMOSS)},
  pages =	{1--15},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{6351},
  editor =	{Ed Brinksma and David Harel and Angelika Mader and Perdita Stevens and Roel Wieringa},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06351.7},
  URN =		{urn:nbn:de:0030-drops-8659},
  doi =		{10.4230/DagSemProc.06351.7},
  annote =	{Keywords: Information Systems Design, Software Engineering, Model-Based Code Generation}
}

Document

DOI: 10.4230/DagSemProc.06351.8

Modeling and Aspect Weaving

Authors: Jean-Marc Jezequel

Published in: Dagstuhl Seminar Proceedings, Volume 6351, Methods for Modelling Software Systems (MMOSS) (2007)

Abstract

A model is a simplified representation of an aspect of the world for a specific purpose. Complex systems typically give rise to more than one model because many aspects are to be handled. For software systems, the design process can be characterized as a (partially automated) weaving of these aspects into a detailed design model. While verification is usually feasible on each of the aspects, it is seldom possible on the resulting detailed design because of the size explosion. Hence we need weaving processes that exhibit good composition properties from the point of view of verification. We present an example of such a weaving process for behavioral models represented as scenarios.

Cite as

Jean-Marc Jezequel. Modeling and Aspect Weaving. In Methods for Modelling Software Systems (MMOSS). Dagstuhl Seminar Proceedings, Volume 6351, pp. 1-15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{jezequel:DagSemProc.06351.8,
  author =	{Jezequel, Jean-Marc},
  title =	{{Modeling and Aspect Weaving}},
  booktitle =	{Methods for Modelling Software Systems (MMOSS)},
  pages =	{1--15},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{6351},
  editor =	{Ed Brinksma and David Harel and Angelika Mader and Perdita Stevens and Roel Wieringa},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06351.8},
  URN =		{urn:nbn:de:0030-drops-8641},
  doi =		{10.4230/DagSemProc.06351.8},
  annote =	{Keywords: Model Aspect Weaving MDE Kermeta}
}

Document

DOI: 10.4230/DagSemProc.06351.9

Partial Behavioural Models for Requirements and Early Design

Authors: Marsha Chechik, Greg Brunet, Dario Fischbein, and Sebastian Uchitel

Published in: Dagstuhl Seminar Proceedings, Volume 6351, Methods for Modelling Software Systems (MMOSS) (2007)

Abstract

The talk will discuss the problem of creation, management, and specifically merging of partial behavioural models, expressed as model transition systems. We argue why this formalism is essential in the early stages of the software cycle and then discuss why and how to merge information coming from different sources using this formalism. The talk is based on papers presented in FSE'04 and FME'06 and will also include emerging results on synthesizing partial behavioural models from temporal properties and scenarios.

Cite as

Marsha Chechik, Greg Brunet, Dario Fischbein, and Sebastian Uchitel. Partial Behavioural Models for Requirements and Early Design. In Methods for Modelling Software Systems (MMOSS). Dagstuhl Seminar Proceedings, Volume 6351, pp. 1-10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{chechik_et_al:DagSemProc.06351.9,
  author =	{Chechik, Marsha and Brunet, Greg and Fischbein, Dario and Uchitel, Sebastian},
  title =	{{Partial Behavioural Models for Requirements and Early Design}},
  booktitle =	{Methods for Modelling Software Systems (MMOSS)},
  pages =	{1--10},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{6351},
  editor =	{Ed Brinksma and David Harel and Angelika Mader and Perdita Stevens and Roel Wieringa},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06351.9},
  URN =		{urn:nbn:de:0030-drops-8582},
  doi =		{10.4230/DagSemProc.06351.9},
  annote =	{Keywords: Requirements behavioural models}
}

Document

DOI: 10.4230/DagSemProc.06351.10

Structural Relationships among Models

Authors: Michael Jackson

Published in: Dagstuhl Seminar Proceedings, Volume 6351, Methods for Modelling Software Systems (MMOSS) (2007)

Abstract

The basis of a problem-oriented view of software-intensive systems is the recognition of three fundamental roles to be played by models in a development: R, the requirement; W, the given properties of the problem world; and S, the specification of the machine's behaviour at its interface with the problem world. These are (ideally) related by the entailment S,W |= R. Decomposition of a problem into subproblems is analogous (but not identical) to decomposition of a system into components. A subproblem has R, W and S, its machine interacting with a subset of the problem world. Conceptually, subproblems are initially considered in isolation, composition concerns being deferred. Composition of subproblems involves relationships among all three of their models R, W and S; in general different subproblems use different models, even of the same parts of the problem world. Problem world properties are not in general compositional. Relationships among subproblems, and hence among their models, may be complex.

Cite as

Michael Jackson. Structural Relationships among Models. In Methods for Modelling Software Systems (MMOSS). Dagstuhl Seminar Proceedings, Volume 6351, pp. 1-6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{jackson:DagSemProc.06351.10,
  author =	{Jackson, Michael},
  title =	{{Structural Relationships among Models}},
  booktitle =	{Methods for Modelling Software Systems (MMOSS)},
  pages =	{1--6},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{6351},
  editor =	{Ed Brinksma and David Harel and Angelika Mader and Perdita Stevens and Roel Wieringa},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06351.10},
  URN =		{urn:nbn:de:0030-drops-8633},
  doi =		{10.4230/DagSemProc.06351.10},
  annote =	{Keywords: Composition, model, problem, requirement, specificaiton, structure, subproblem}
}

Document

DOI: 10.4230/DagSemProc.06351.11

System model for UML – The interactions case

Authors: María Victoria Cengarle

Published in: Dagstuhl Seminar Proceedings, Volume 6351, Methods for Modelling Software Systems (MMOSS) (2007)

Abstract

A system model for an OO specification language is any timed state transition system whose states are composed of a data store, a control store, and a message pool. To define a semantics for any OO specification language (as e.g. UML) is the art of defining the transition function $Delta$ depending on the current state and on the input sofar that moreover observes certain rules. Having defined what a system model is, the challenge now is to establish when such a system model satisfies a message interchange specification (expressed by means of UML interactions).

Cite as

María Victoria Cengarle. System model for UML – The interactions case. In Methods for Modelling Software Systems (MMOSS). Dagstuhl Seminar Proceedings, Volume 6351, pp. 1-19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{cengarle:DagSemProc.06351.11,
  author =	{Cengarle, Mar{\'\i}a Victoria},
  title =	{{System model for UML – The interactions case}},
  booktitle =	{Methods for Modelling Software Systems (MMOSS)},
  pages =	{1--19},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{6351},
  editor =	{Ed Brinksma and David Harel and Angelika Mader and Perdita Stevens and Roel Wieringa},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06351.11},
  URN =		{urn:nbn:de:0030-drops-8572},
  doi =		{10.4230/DagSemProc.06351.11},
  annote =	{Keywords: System model, UML, interaction}
}

16 Search Results for "Stevens, Perdita"

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Thanks for your feedback!

Could not send message