11 Search Results for "Wehrheim, Heike"

Document
DOI: 10.4230/LIPIcs.OPODIS.2025.17
Recoverable Lock-Free Locks

Authors: Hagit Attiya, Panagiota Fatourou, Eleftherios Kosmas, and Yuanhao Wei

Published in: LIPIcs, Volume 361, 29th International Conference on Principles of Distributed Systems (OPODIS 2025)

Abstract
This paper presents the first transformation that introduces both lock-freedom and recoverability. Our transformation starts with a lock-based implementation, and provides a recoverable, lock-free substitution to lock acquire and lock release operations. The transformation supports nested locks for generality and ensures recoverability without jeopardising the correctness of the lock-based implementation it is applied on.
Cite as

Hagit Attiya, Panagiota Fatourou, Eleftherios Kosmas, and Yuanhao Wei. Recoverable Lock-Free Locks. In 29th International Conference on Principles of Distributed Systems (OPODIS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 361, pp. 17:1-17:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{attiya_et_al:LIPIcs.OPODIS.2025.17,
  author =	{Attiya, Hagit and Fatourou, Panagiota and Kosmas, Eleftherios and Wei, Yuanhao},
  title =	{{Recoverable Lock-Free Locks}},
  booktitle =	{29th International Conference on Principles of Distributed Systems (OPODIS 2025)},
  pages =	{17:1--17:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-409-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{361},
  editor =	{Arusoaie, Andrei and Onica, Emanuel and Spear, Michael and Tucci-Piergiovanni, Sara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2025.17},
  URN =		{urn:nbn:de:0030-drops-251905},
  doi =		{10.4230/LIPIcs.OPODIS.2025.17},
  annote =	{Keywords: recoverable computing, NVM, lock, lock-freedom}
}
Document
DOI: 10.4230/DagRep.15.4.92
Information Exchange in Software Verification (Dagstuhl Seminar 25172)

Authors: Dirk Beyer, Marieke Huisman, Jan Strejček, and Heike Wehrheim

Published in: Dagstuhl Reports, Volume 15, Issue 4 (2025)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 25172 Information Exchange in Software Verification. The term "software verification" refers to the procedure of deciding the correctness of software with respect to (user-supplied or predefined) specifications. In general, software verification is an undecidable problem. Despite this undecidability, software verification is a very active research field with contributions of researchers from several areas such as theorem proving, deductive verification, static analysis, and automatic verification. The analysis techniques developed in these subareas are often complementary with respect to the type of software and specifications they can efficiently handle. The objective of this Dagstuhl Seminar was to bring together people working in these different subareas to discuss and advance ways of having tools and techniques cooperate on the task of software verification.
Cite as

Dirk Beyer, Marieke Huisman, Jan Strejček, and Heike Wehrheim. Information Exchange in Software Verification (Dagstuhl Seminar 25172). In Dagstuhl Reports, Volume 15, Issue 4, pp. 92-111, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@Article{beyer_et_al:DagRep.15.4.92,
  author =	{Beyer, Dirk and Huisman, Marieke and Strej\v{c}ek, Jan and Wehrheim, Heike},
  title =	{{Information Exchange in Software Verification (Dagstuhl Seminar 25172)}},
  pages =	{92--111},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2025},
  volume =	{15},
  number =	{4},
  editor =	{Beyer, Dirk and Huisman, Marieke and Strej\v{c}ek, Jan and Wehrheim, Heike},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.15.4.92},
  URN =		{urn:nbn:de:0030-drops-252559},
  doi =		{10.4230/DagRep.15.4.92},
  annote =	{Keywords: Competitions and Benchmarks, Data-Flow Analysis, Deductive Verification, Formal Verification, Model Checking}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.26
Optimal Concolic Dynamic Partial Order Reduction

Authors: Mohammad Hossein Khoshechin Jorshari, Michalis Kokologiannakis, Rupak Majumdar, and Srinidhi Nagendra

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
Stateless model checking (SMC) software implementations requires exploring both concurrency- and data nondeterminism. Unfortunately, most SMC algorithms focus on efficient exploration of concurrency nondeterminism, thereby neglecting an important source of bugs. We present ConDpor, an SMC algorithm for unmodified Java programs that combines optimal dynamic partial order reduction (DPOR) for concurrency nondeterminism, with concolic execution for data nondeterminism. ConDpor is sound, complete, optimal, and parametric w.r.t. the memory consistency model. Our experiments confirm that ConDpor is exponentially faster than DPOR with small-domain enumeration. Overall, ConDpor opens the door for efficient exploration of concurrent programs with data nondeterminism.
Cite as

Mohammad Hossein Khoshechin Jorshari, Michalis Kokologiannakis, Rupak Majumdar, and Srinidhi Nagendra. Optimal Concolic Dynamic Partial Order Reduction. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 26:1-26:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{khoshechinjorshari_et_al:LIPIcs.CONCUR.2025.26,
  author =	{Khoshechin Jorshari, Mohammad Hossein and Kokologiannakis, Michalis and Majumdar, Rupak and Nagendra, Srinidhi},
  title =	{{Optimal Concolic Dynamic Partial Order Reduction}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{26:1--26:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.26},
  URN =		{urn:nbn:de:0030-drops-239765},
  doi =		{10.4230/LIPIcs.CONCUR.2025.26},
  annote =	{Keywords: Stateless model checking, dynamic symbolic execution}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2022.31
Weak Progressive Forward Simulation Is Necessary and Sufficient for Strong Observational Refinement

Authors: Brijesh Dongol, Gerhard Schellhorn, and Heike Wehrheim

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract
Hyperproperties are correctness conditions for labelled transition systems that are more expressive than traditional trace properties, with particular relevance to security. Recently, Attiya and Enea studied a notion of strong observational refinement that preserves all hyperproperties. They analyse the correspondence between forward simulation and strong observational refinement in a setting with only finite traces. We study this correspondence in a setting with both finite and infinite traces. In particular, we show that forward simulation does not preserve hyperliveness properties in this setting. We extend the forward simulation proof obligation with a (weak) progress condition, and prove that this weak progressive forward simulation is equivalent to strong observational refinement.
Cite as

Brijesh Dongol, Gerhard Schellhorn, and Heike Wehrheim. Weak Progressive Forward Simulation Is Necessary and Sufficient for Strong Observational Refinement. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 31:1-31:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{dongol_et_al:LIPIcs.CONCUR.2022.31,
  author =	{Dongol, Brijesh and Schellhorn, Gerhard and Wehrheim, Heike},
  title =	{{Weak Progressive Forward Simulation Is Necessary and Sufficient for Strong Observational Refinement}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{31:1--31:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.31},
  URN =		{urn:nbn:de:0030-drops-170947},
  doi =		{10.4230/LIPIcs.CONCUR.2022.31},
  annote =	{Keywords: Strong Observational Refinement, Hyperproperties, Forward Simulation, Weak Progressiveness}
}
Document
Brief Announcement
DOI: 10.4230/LIPIcs.DISC.2021.55
Brief Announcement: On Strong Observational Refinement and Forward Simulation

Authors: John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, and Heike Wehrheim

Published in: LIPIcs, Volume 209, 35th International Symposium on Distributed Computing (DISC 2021)

Abstract
Hyperproperties are correctness conditions for labelled transition systems that are more expressive than traditional trace properties, with particular relevance to security. Recently, Attiya and Enea studied a notion of strong observational refinement that preserves all hyperproperties. They analyse the correspondence between forward simulation and strong observational refinement in a setting with finite traces only. We study this correspondence in a setting with both finite and infinite traces. In particular, we show that forward simulation does not preserve hyperliveness properties in this setting. We extend the forward simulation proof obligation with a progress condition, and prove that this progressive forward simulation does imply strong observational refinement.
Cite as

John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, and Heike Wehrheim. Brief Announcement: On Strong Observational Refinement and Forward Simulation. In 35th International Symposium on Distributed Computing (DISC 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 209, pp. 55:1-55:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{derrick_et_al:LIPIcs.DISC.2021.55,
  author =	{Derrick, John and Doherty, Simon and Dongol, Brijesh and Schellhorn, Gerhard and Wehrheim, Heike},
  title =	{{Brief Announcement: On Strong Observational Refinement and Forward Simulation}},
  booktitle =	{35th International Symposium on Distributed Computing (DISC 2021)},
  pages =	{55:1--55:4},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-210-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{209},
  editor =	{Gilbert, Seth},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2021.55},
  URN =		{urn:nbn:de:0030-drops-148575},
  doi =		{10.4230/LIPIcs.DISC.2021.55},
  annote =	{Keywords: Strong Observational Refinement, Hyperproperties, Forward Simulation}
}
Document
DOI: 10.4230/OASIcs.Gabbrielli.10
Inseguendo Fagiani Selvatici: Partial Order Reduction for Guarded Command Languages

Authors: Frank S. de Boer, Einar Broch Johnsen, Rudolf Schlatte, Silvia Lizeth Tapia Tarifa, and Lars Tveito

Published in: OASIcs, Volume 86, Recent Developments in the Design and Implementation of Programming Languages (2020)

Abstract
This paper presents a method for testing whether objects in actor languages and active object languages exhibit locally deterministic behavior. We investigate such a method for a class of guarded command programs, abstracting from object-oriented features like method calls but focusing on cooperative scheduling of dynamically spawned processes executing in parallel. The proposed method can answer questions such as whether all permutations of an execution trace are equivalent, by generating candidate traces for testing which may lead to different final states. To prune the set of candidate traces, we employ partial order reduction. To further reduce the set, we introduce an analysis technique to decide whether a generated trace is schedulable. Schedulability cannot be decided for guarded commands using standard dependence and interference relations because guard enabledness is non-monotonic. To solve this problem, we use concolic execution to produce linearized symbolic traces of the executed program, which allows a weakest precondition computation to decide on the satisfiability of guards.
Cite as

Frank S. de Boer, Einar Broch Johnsen, Rudolf Schlatte, Silvia Lizeth Tapia Tarifa, and Lars Tveito. Inseguendo Fagiani Selvatici: Partial Order Reduction for Guarded Command Languages. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{deboer_et_al:OASIcs.Gabbrielli.10,
  author =	{de Boer, Frank S. and Johnsen, Einar Broch and Schlatte, Rudolf and Tapia Tarifa, Silvia Lizeth and Tveito, Lars},
  title =	{{Inseguendo Fagiani Selvatici: Partial Order Reduction for Guarded Command Languages}},
  booktitle =	{Recent Developments in the Design and Implementation of Programming Languages},
  pages =	{10:1--10:18},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-171-9},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{86},
  editor =	{de Boer, Frank S. and Mauro, Jacopo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Gabbrielli.10},
  URN =		{urn:nbn:de:0030-drops-132322},
  doi =		{10.4230/OASIcs.Gabbrielli.10},
  annote =	{Keywords: Testing, Symbolic Traces, Guarded Commands, Partial Order Reduction}
}
Document
Artifact
DOI: 10.4230/DARTS.6.2.15
Owicki-Gries Reasoning for C11 RAR (Artifact)

Authors: Sadegh Dalvandi, Simon Doherty, Brijesh Dongol, and Heike Wehrheim

Published in: DARTS, Volume 6, Issue 2, Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020)

Abstract
The paper "Owicki-Gries Reasoning for C11 RAR" introduces a new proof calculus for the C11 RAR memory model that allows Owicki-Gries proof rules for compound statements, including non-interference, to remain unchanged. The proof method features novel assertions specifying thread-specific views on the state of programs. This is combined with a set of Hoare logic rules that describe how these assertions are affected by atomic program steps. The artifact includes the Isabelle formalisation of the proof method introduced in the paper. It also contains the formalisation and proof of all case studies presented in the paper. All of the theorems are accompanied with their respective proofs.
Cite as

Sadegh Dalvandi, Simon Doherty, Brijesh Dongol, and Heike Wehrheim. Owicki-Gries Reasoning for C11 RAR (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 15:1-15:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@Article{dalvandi_et_al:DARTS.6.2.15,
  author =	{Dalvandi, Sadegh and Doherty, Simon and Dongol, Brijesh and Wehrheim, Heike},
  title =	{{Owicki-Gries Reasoning for C11 RAR (Artifact)}},
  pages =	{15:1--15:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2020},
  volume =	{6},
  number =	{2},
  editor =	{Dalvandi, Sadegh and Doherty, Simon and Dongol, Brijesh and Wehrheim, Heike},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.6.2.15},
  URN =		{urn:nbn:de:0030-drops-132123},
  doi =		{10.4230/DARTS.6.2.15},
  annote =	{Keywords: C11, Verification, Hoare logic, Owicki-Gries, Isabelle}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2020.11
Owicki-Gries Reasoning for C11 RAR

Authors: Sadegh Dalvandi, Simon Doherty, Brijesh Dongol, and Heike Wehrheim

Published in: LIPIcs, Volume 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020)

Abstract
Owicki-Gries reasoning for concurrent programs uses Hoare logic together with an interference freedom rule for concurrency. In this paper, we develop a new proof calculus for the C11 RAR memory model (a fragment of C11 with both relaxed and release-acquire accesses) that allows all Owicki-Gries proof rules for compound statements, including non-interference, to remain unchanged. Our proof method features novel assertions specifying thread-specific views on the state of programs. This is combined with a set of Hoare logic rules that describe how these assertions are affected by atomic program steps. We demonstrate the utility of our proof calculus by verifying a number of standard C11 litmus tests and Peterson’s algorithm adapted for C11. Our proof calculus and its application to program verification have been fully mechanised in the theorem prover Isabelle.
Cite as

Sadegh Dalvandi, Simon Doherty, Brijesh Dongol, and Heike Wehrheim. Owicki-Gries Reasoning for C11 RAR. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 11:1-11:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{dalvandi_et_al:LIPIcs.ECOOP.2020.11,
  author =	{Dalvandi, Sadegh and Doherty, Simon and Dongol, Brijesh and Wehrheim, Heike},
  title =	{{Owicki-Gries Reasoning for C11 RAR}},
  booktitle =	{34th European Conference on Object-Oriented Programming (ECOOP 2020)},
  pages =	{11:1--11:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-154-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{166},
  editor =	{Hirschfeld, Robert and Pape, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2020.11},
  URN =		{urn:nbn:de:0030-drops-131687},
  doi =		{10.4230/LIPIcs.ECOOP.2020.11},
  annote =	{Keywords: C11, Verification, Hoare logic, Owicki-Gries, Isabelle}
}
Document
Brief Announcement
DOI: 10.4230/LIPIcs.DISC.2018.45
Brief Announcement: Generalising Concurrent Correctness to Weak Memory

Authors: Simon Doherty, Brijesh Dongol, Heike Wehrheim, and John Derrick

Published in: LIPIcs, Volume 121, 32nd International Symposium on Distributed Computing (DISC 2018)

Abstract
Correctness conditions like linearizability and opacity describe some form of atomicity imposed on concurrent objects. In this paper, we propose a correctness condition (called causal atomicity) for concurrent objects executing in a weak memory model, where the histories of the objects in question are partially ordered. We establish compositionality and abstraction results for causal atomicity and develop an associated refinement-based proof technique.
Cite as

Simon Doherty, Brijesh Dongol, Heike Wehrheim, and John Derrick. Brief Announcement: Generalising Concurrent Correctness to Weak Memory. In 32nd International Symposium on Distributed Computing (DISC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 121, pp. 45:1-45:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{doherty_et_al:LIPIcs.DISC.2018.45,
  author =	{Doherty, Simon and Dongol, Brijesh and Wehrheim, Heike and Derrick, John},
  title =	{{Brief Announcement: Generalising Concurrent Correctness to Weak Memory}},
  booktitle =	{32nd International Symposium on Distributed Computing (DISC 2018)},
  pages =	{45:1--45:3},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-092-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{121},
  editor =	{Schmid, Ulrich and Widder, Josef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2018.45},
  URN =		{urn:nbn:de:0030-drops-98344},
  doi =		{10.4230/LIPIcs.DISC.2018.45},
  annote =	{Keywords: Weak Memory, Concurrent Object, Execution Structure}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2016.35
Proving Opacity of a Pessimistic STM

Authors: Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, and Heike Wehrheim

Published in: LIPIcs, Volume 70, 20th International Conference on Principles of Distributed Systems (OPODIS 2016)

Abstract
Transactional Memory (TM) is a high-level programming abstraction for concurrency control that provides programmers with the illusion of atomically executing blocks of code, called transactions. TMs come in two categories, optimistic and pessimistic, where in the latter transactions never abort. While this simplifies the programming model, high-performing pessimistic TMs can be complex. In this paper, we present the first formal verification of a pessimistic software TM algorithm, namely, an algorithm proposed by Matveev and Shavit. The correctness criterion used is opacity, formalising the transactional atomicity guarantees. We prove that this pessimistic TM is a refinement of an intermediate opaque I/O-automaton, known as TMS2. To this end, we develop a rely-guarantee approach for reducing the complexity of the proof. Proofs are mechanised in the interactive prover Isabelle.
Cite as

Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, and Heike Wehrheim. Proving Opacity of a Pessimistic STM. In 20th International Conference on Principles of Distributed Systems (OPODIS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 70, pp. 35:1-35:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{doherty_et_al:LIPIcs.OPODIS.2016.35,
  author =	{Doherty, Simon and Dongol, Brijesh and Derrick, John and Schellhorn, Gerhard and Wehrheim, Heike},
  title =	{{Proving Opacity of a Pessimistic STM}},
  booktitle =	{20th International Conference on Principles of Distributed Systems (OPODIS 2016)},
  pages =	{35:1--35:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-031-6},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{70},
  editor =	{Fatourou, Panagiota and Jim\'{e}nez, Ernesto and Pedone, Fernando},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2016.35},
  URN =		{urn:nbn:de:0030-drops-71040},
  doi =		{10.4230/LIPIcs.OPODIS.2016.35},
  annote =	{Keywords: Pessimistic STMs, Opacity, Verification, Isabelle, Simulation, TMS2}
}
Document
DOI: 10.4230/DagSemProc.04101.13
Refinement and Consistency in Multiview Models

Authors: Heike Wehrheim

Published in: Dagstuhl Seminar Proceedings, Volume 4101, Language Engineering for Model-Driven Software Development (2005)

Abstract
Model transformations are an integral part of OMG's standard for Model Driven Architecture (MDA). Model transformations should at the best allow for a seamless transition from high-level models to actual implementations. They are therefore required to be behaviour preserving: models (or the final implementation) at lower levels should adhere to the descriptions given in higher level models. Moreover, for complex systems models usually consists of descriptions of different views on the system. Consequently, different kinds of model transformations take place on different views, and together they should guarantee behaviourpreservation. In this paper we discuss the applicability of formal methods to model transformations. Formal methods come with build-in notions of transformations between models, or more precisely, with refinement and subtyping concepts which provide means for comparing models on different levels with respect to their behaviour. Such notions can be applied as correctness criteria for evaluating model transformations. Moreover, refinement and subtyping concepts for different views can be shown to neatly fit together. This is achieved by giving a common semantics to all views which furthermore opens the possibility of checking consistency between them.
Cite as

Heike Wehrheim. Refinement and Consistency in Multiview Models. In Language Engineering for Model-Driven Software Development. Dagstuhl Seminar Proceedings, Volume 4101, pp. 1-11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2005)

Copy BibTex To Clipboard

@InProceedings{wehrheim:DagSemProc.04101.13,
  author =	{Wehrheim, Heike},
  title =	{{Refinement and Consistency in Multiview Models}},
  booktitle =	{Language Engineering for Model-Driven Software Development},
  pages =	{1--11},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2005},
  volume =	{4101},
  editor =	{Jean Bezivin and Reiko Heckel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.04101.13},
  URN =		{urn:nbn:de:0030-drops-190},
  doi =		{10.4230/DagSemProc.04101.13},
  annote =	{Keywords: no keywords}
}
  • Refine by Type
  • 11 Document/PDF
  • 3 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 2 2025
  • 1 2022
  • 1 2021
  • 3 2020
  • Show More...

  • Refine by Author
  • 8 Wehrheim, Heike
  • 6 Dongol, Brijesh
  • 5 Doherty, Simon
  • 3 Derrick, John
  • 3 Schellhorn, Gerhard
  • Show More...

  • Refine by Series/Journal
  • 7 LIPIcs
  • 1 OASIcs
  • 1 DARTS
  • 1 DagRep
  • 1 DagSemProc

  • Refine by Classification
  • 5 Theory of computation → Concurrency
  • 3 Theory of computation → Logic and verification
  • 2 Security and privacy → Formal methods and theory of security
  • 2 Theory of computation → Hoare logic
  • 2 Theory of computation → Operational semantics
  • Show More...

  • Refine by Keyword
  • 3 Isabelle
  • 3 Verification
  • 2 C11
  • 2 Forward Simulation
  • 2 Hoare logic
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact