Journal Articles
Bagherzadeh, Mojtaba; Jahed, Karim; Dingel, Juergen; Combemale, Benoit
Live Modeling in the Context of State Machine Models and Code Generation Journal Article
In: Software and Systems Modeling (SoSyM), vol. 20, pp. 795-819, 2021.
@article{BJDC21,
title = {Live Modeling in the Context of State Machine Models and Code Generation},
author = {Mojtaba Bagherzadeh and Karim Jahed and Juergen Dingel and Benoit Combemale},
url = {https://link.springer.com/article/10.1007/s10270-020-00829-y},
doi = {10.1007/s10270-020-00829-y},
year = {2021},
date = {2021-06-01},
journal = {Software and Systems Modeling (SoSyM)},
volume = {20},
pages = {795-819},
publisher = {Springer},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Bagherzadeh, Mojtaba; Kahani, Nafiseh; Jahed, Karim; Dingel, Juergen
Execution of Partial State Machine Models Journal Article
In: IEEE Transactions on Software Engineering, 2020, (In print).
@article{BKJD20,
title = {Execution of Partial State Machine Models},
author = {Mojtaba Bagherzadeh and Nafiseh Kahani and Karim Jahed and Juergen Dingel},
url = {https://ieeexplore.ieee.org/document/9139402},
doi = {10.1109/TSE.2020.3008850},
year = {2020},
date = {2020-01-01},
journal = {IEEE Transactions on Software Engineering},
publisher = {IEEE},
note = {In print},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Jahed, Karim; Bagherzadeh, Mojtaba; Dingel, Juergen
On the Benefits of File-level Modularity in the Context of Model-driven Development Journal Article
In: Software and Systems Modeling (SoSyM), vol. 20, pp. 267-286, 2020.
@article{JDB20,
title = {On the Benefits of File-level Modularity in the Context of Model-driven Development},
author = {Karim Jahed and Mojtaba Bagherzadeh and Juergen Dingel},
url = {https://link.springer.com/article/10.1007/s10270-020-00804-7},
doi = {10.1007/s10270-020-00804-7},
year = {2020},
date = {2020-01-01},
journal = {Software and Systems Modeling (SoSyM)},
volume = {20},
pages = {267-286},
publisher = {Springer},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Hili, Nicolas; Bagherzadeh, Mojtaba; Jahed, Karim; Dingel, Juergen
A model-based architecture for interactive run-time monitoring Journal Article
In: Software and Systems Modeling (SoSyM) publisher = Springer, vol. 19, no. 4, pp. 959-981, 2020.
@article{HBJD20,
title = {A model-based architecture for interactive run-time monitoring},
author = {Nicolas Hili and Mojtaba Bagherzadeh and Karim Jahed and Juergen Dingel},
url = {http://link.springer.com/article/10.1007/s10270-020-00780-y},
doi = {10.1007/s10270-020-00780-y},
year = {2020},
date = {2020-01-01},
journal = {Software and Systems Modeling (SoSyM) publisher = Springer},
volume = {19},
number = {4},
pages = {959-981},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Atampore, Francis; Dingel, Juergen; Rudie, Karen
A Controller Synthesis Framework for Automated Service Composition Journal Article
In: Discrete Event Dynamic Systems (JDEDS), vol. 29, pp. 297-365, 2019.
@article{ADR19b,
title = {A Controller Synthesis Framework for Automated Service Composition},
author = {Francis Atampore and Juergen Dingel and Karen Rudie},
year = {2019},
date = {2019-01-01},
journal = {Discrete Event Dynamic Systems (JDEDS)},
volume = {29},
pages = {297-365},
publisher = {Springer},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Atampore, Francis; Dingel, Juergen; Rudie, Karen
A Controller Synthesis Framework for Automated Service Composition Journal Article
In: Discrete Event Dynamic Systems (JDEDS), 2019, (To appear).
@article{ADR19,
title = {A Controller Synthesis Framework for Automated Service Composition},
author = {Francis Atampore and Juergen Dingel and Karen Rudie},
year = {2019},
date = {2019-01-01},
journal = {Discrete Event Dynamic Systems (JDEDS)},
publisher = {Springer},
note = {To appear},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Das, Tuhin Kanti; Dingel, Juergen
Model Development Guidelines for UML-RT: Conventions, Patterns, and Antipatterns Journal Article
In: Software and Systems Modeling (SoSyM), vol. 17, no. 3, pp. 717-752, 2018.
@article{DD18b,
title = {Model Development Guidelines for UML-RT: Conventions, Patterns, and Antipatterns},
author = {Tuhin Kanti Das and Juergen Dingel},
url = {https://doi.org/10.1007/s10270-016-0549-6},
doi = {10.1007/s10270-016-0549-6},
year = {2018},
date = {2018-07-01},
journal = {Software and Systems Modeling (SoSyM)},
volume = {17},
number = {3},
pages = {717-752},
publisher = {Springer},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Das, Tuhin Kanti; Dingel, Juergen
Model Development Guidelines for UML-RT: Conventions, Patterns, and Antipatterns Journal Article
In: Software and Systems Modeling (SoSyM), vol. 17, no. 3, pp. 717-752, 2018.
@article{DD18,
title = {Model Development Guidelines for UML-RT: Conventions, Patterns, and Antipatterns},
author = {Tuhin Kanti Das and Juergen Dingel},
url = {https://doi.org/10.1007/s10270-016-0549-6},
doi = {10.1007/s10270-016-0549-6},
year = {2018},
date = {2018-07-01},
journal = {Software and Systems Modeling (SoSyM)},
volume = {17},
number = {3},
pages = {717-752},
publisher = {Springer},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Bagherzadeh, Mojtaba; Kahani, Nafiseh; Bezemer, Cor-Paul; Hassan, Ahmed E; Dingel, Juergen; Cordy, James R
Analyzing a Decade of Linux System Calls Journal Article
In: Empirical Software Engineering Journal, vol. 23, no. 3, pp. 1519-1551, 2018.
@article{BKBHDC18b,
title = {Analyzing a Decade of Linux System Calls},
author = {Mojtaba Bagherzadeh and Nafiseh Kahani and Cor-Paul Bezemer and Ahmed E Hassan and Juergen Dingel and James R Cordy},
url = {https://doi.org/10.1007/s10664-017-9551-z},
doi = {10.1007/s10664-017-9551-z},
year = {2018},
date = {2018-06-01},
journal = {Empirical Software Engineering Journal},
volume = {23},
number = {3},
pages = {1519-1551},
publisher = {Springer},
abstract = {Over the past 25 years, thousands of developers have contributed more than 18 million lines of code (LOC) to the Linux kernel. As the Linux kernel forms the central part of various operating systems that are used by millions of users, the kernel must be continuously adapted to the changing demands and expectations of these users.
The Linux kernel provides its services to an application through system calls. The combined set of all system calls forms the essential Application Programming Interface (API) through which an application interacts with the kernel. In this paper, we conduct an empirical study of 8,770 changes that were made to Linux system calls during the last decade (i.e., from April 2005 to December 2014). In particular, we study the size of the changes, and we manually identify the type of changes and bug fixes that were made. Our analysis provides an overview of the evolution of the Linux system calls over the last decade. We find that there was a considerable amount of technical debt in the kernel, that was addressed by adding a number of sibling calls(i.e., 26% of all system calls). In addition, we find that by far, the ptrace() and signal handling system calls are the most challenging to maintain. Our study can be used by developers who want to improve the design and ensure the successful evolution of their own kernel APIs.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
The Linux kernel provides its services to an application through system calls. The combined set of all system calls forms the essential Application Programming Interface (API) through which an application interacts with the kernel. In this paper, we conduct an empirical study of 8,770 changes that were made to Linux system calls during the last decade (i.e., from April 2005 to December 2014). In particular, we study the size of the changes, and we manually identify the type of changes and bug fixes that were made. Our analysis provides an overview of the evolution of the Linux system calls over the last decade. We find that there was a considerable amount of technical debt in the kernel, that was addressed by adding a number of sibling calls(i.e., 26% of all system calls). In addition, we find that by far, the ptrace() and signal handling system calls are the most challenging to maintain. Our study can be used by developers who want to improve the design and ensure the successful evolution of their own kernel APIs.
Bagherzadeh, Mojtaba; Kahani, Nafiseh; Bezemer, Cor-Paul; Hassan, Ahmed E; Dingel, Juergen; Cordy, James R
Analyzing a Decade of Linux System Calls Journal Article
In: Empirical Software Engineering Journal, vol. 23, no. 3, pp. 1519-1551, 2018.
@article{BKBHDC18,
title = {Analyzing a Decade of Linux System Calls},
author = {Mojtaba Bagherzadeh and Nafiseh Kahani and Cor-Paul Bezemer and Ahmed E Hassan and Juergen Dingel and James R Cordy},
url = {https://doi.org/10.1007/s10664-017-9551-z},
doi = {10.1007/s10664-017-9551-z},
year = {2018},
date = {2018-06-01},
journal = {Empirical Software Engineering Journal},
volume = {23},
number = {3},
pages = {1519-1551},
publisher = {Springer},
abstract = {Over the past 25 years, thousands of developers have contributed more than 18 million lines of code (LOC) to the Linux kernel. As the Linux kernel forms the central part of various operating systems that are used by millions of users, the kernel must be continuously adapted to the changing demands and expectations of these users.
The Linux kernel provides its services to an application through system calls. The combined set of all system calls forms the essential Application Programming Interface (API) through which an application interacts with the kernel. In this paper, we conduct an empirical study of 8,770 changes that were made to Linux system calls during the last decade (i.e., from April 2005 to December 2014). In particular, we study the size of the changes, and we manually identify the type of changes and bug fixes that were made. Our analysis provides an overview of the evolution of the Linux system calls over the last decade. We find that there was a considerable amount of technical debt in the kernel, that was addressed by adding a number of sibling calls(i.e., 26% of all system calls). In addition, we find that by far, the ptrace() and signal handling system calls are the most challenging to maintain. Our study can be used by developers who want to improve the design and ensure the successful evolution of their own kernel APIs.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
The Linux kernel provides its services to an application through system calls. The combined set of all system calls forms the essential Application Programming Interface (API) through which an application interacts with the kernel. In this paper, we conduct an empirical study of 8,770 changes that were made to Linux system calls during the last decade (i.e., from April 2005 to December 2014). In particular, we study the size of the changes, and we manually identify the type of changes and bug fixes that were made. Our analysis provides an overview of the evolution of the Linux system calls over the last decade. We find that there was a considerable amount of technical debt in the kernel, that was addressed by adding a number of sibling calls(i.e., 26% of all system calls). In addition, we find that by far, the ptrace() and signal handling system calls are the most challenging to maintain. Our study can be used by developers who want to improve the design and ensure the successful evolution of their own kernel APIs.
Dingel, Juergen; Schulte, Wolfram
Guest editorial for the special section on MODELS 2014 Journal Article
In: Software and Systems Modeling (SoSyM), vol. 17, no. 1, pp. 9-10, 2018.
@article{DS18b,
title = {Guest editorial for the special section on MODELS 2014},
author = {Juergen Dingel and Wolfram Schulte},
url = {https://doi.org/10.1007/s10270-016-0561-x},
doi = {10.1007/s10270-016-0561-x},
year = {2018},
date = {2018-02-01},
journal = {Software and Systems Modeling (SoSyM)},
volume = {17},
number = {1},
pages = {9-10},
publisher = {Springer},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Kahani, Nafiseh; Bagherzadeh, Mojtaba; Cordy, Jim; Dingel, Juergen; Varro, Daniel
Survey and Classification of Model Transformation Tools Journal Article
In: Software and Systems Modeling (SoSyM), pp. 37, 2018.
@article{KBCDV18b,
title = {Survey and Classification of Model Transformation Tools},
author = {Nafiseh Kahani and Mojtaba Bagherzadeh and Jim Cordy and Juergen Dingel and Daniel Varro},
url = {https://link.springer.com/article/10.1007/s10270-018-0665-6},
doi = {https://doi.org/10.1007/s10270-018-0665-6},
year = {2018},
date = {2018-02-01},
journal = {Software and Systems Modeling (SoSyM)},
pages = {37},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Dingel, Juergen; Schulte, Wolfram
Guest editorial for the special section on MODELS 2014 Journal Article
In: Software and Systems Modeling (SoSyM), vol. 17, no. 1, pp. 9-10, 2018.
@article{DS18,
title = {Guest editorial for the special section on MODELS 2014},
author = {Juergen Dingel and Wolfram Schulte},
url = {https://doi.org/10.1007/s10270-016-0561-x},
doi = {10.1007/s10270-016-0561-x},
year = {2018},
date = {2018-02-01},
journal = {Software and Systems Modeling (SoSyM)},
volume = {17},
number = {1},
pages = {9-10},
publisher = {Springer},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Kahani, Nafiseh; Bagherzadeh, Mojtaba; Cordy, Jim; Dingel, Juergen; Varro, Daniel
Survey and Classification of Model Transformation Tools Journal Article
In: Software and Systems Modeling (SoSyM), pp. 37, 2018.
@article{KBCDV18,
title = {Survey and Classification of Model Transformation Tools},
author = {Nafiseh Kahani and Mojtaba Bagherzadeh and Jim Cordy and Juergen Dingel and Daniel Varro},
url = {https://link.springer.com/article/10.1007/s10270-018-0665-6},
doi = {https://doi.org/10.1007/s10270-018-0665-6},
year = {2018},
date = {2018-02-01},
journal = {Software and Systems Modeling (SoSyM)},
pages = {37},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Waez, Md. Tawhid Bin; WÄ…sowski, Andrzej; Dingel, Juergen; Rudie, Karen
Controller Synthesis for Dynamic Hierarchical Real-Time Plants Using Timed Automata Journal Article
In: Journal Discrete Event Dynamic Systems, Special Issue on Formal Methods in Control, vol. 27, pp. 407-441, 2017.
@article{WWD+17b,
title = {Controller Synthesis for Dynamic Hierarchical Real-Time Plants Using Timed Automata},
author = {Md. Tawhid Bin Waez and Andrzej WÄ…sowski and Juergen Dingel and Karen Rudie},
url = {http://dx.doi.org/10.1007/s10626-017-0240-2},
doi = {10.1007/s10626-017-0240-2},
year = {2017},
date = {2017-06-01},
journal = {Journal Discrete Event Dynamic Systems, Special Issue on Formal Methods in Control},
volume = {27},
pages = {407-441},
publisher = {Springer},
abstract = {We use timed I/O automata based timed games to synthesize task-level reconfiguration services for cost-effective fault tolerance in a case study. The case study shows that state-space explosion is a severe problem for timed games. By applying suitable abstractions, we dramatically improve the scalability. However, timed I/O automata do not facilitate algorithmic abstraction generation techniques. The case study motivates the development of timed process automata to improve modeling and analysis for controller synthesis of time-critical plants which can be hierarchical and dynamic. The model offers two essential features for industrial systems: (i) compositional modeling with reusable designs for different contexts, and (ii) state-space reduction technique. Timed process automata model dynamic networks of continuous-time communicating plant processes which can activate other plant processes. We show how to establish safety and reachability properties of timed process automata by reduction to solving timed games. To mitigate the state-space explosion problem, an algorithmic state-space reduction technique using compositional reasoning and aggressive abstractions is also proposed. In this article, we demonstrate the theoretical framework of timed process automata and the effectiveness of the proposed state-space reduction technique by extending the case study.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Waez, Md. Tawhid Bin; WÄ…sowski, Andrzej; Dingel, Juergen; Rudie, Karen
Controller Synthesis for Dynamic Hierarchical Real-Time Plants Using Timed Automata Journal Article
In: Journal Discrete Event Dynamic Systems, Special Issue on Formal Methods in Control, vol. 27, pp. 407-441, 2017.
@article{WWD+17,
title = {Controller Synthesis for Dynamic Hierarchical Real-Time Plants Using Timed Automata},
author = {Md. Tawhid Bin Waez and Andrzej WÄ…sowski and Juergen Dingel and Karen Rudie},
url = {http://dx.doi.org/10.1007/s10626-017-0240-2},
doi = {10.1007/s10626-017-0240-2},
year = {2017},
date = {2017-06-01},
journal = {Journal Discrete Event Dynamic Systems, Special Issue on Formal Methods in Control},
volume = {27},
pages = {407-441},
publisher = {Springer},
abstract = {We use timed I/O automata based timed games to synthesize task-level reconfiguration services for cost-effective fault tolerance in a case study. The case study shows that state-space explosion is a severe problem for timed games. By applying suitable abstractions, we dramatically improve the scalability. However, timed I/O automata do not facilitate algorithmic abstraction generation techniques. The case study motivates the development of timed process automata to improve modeling and analysis for controller synthesis of time-critical plants which can be hierarchical and dynamic. The model offers two essential features for industrial systems: (i) compositional modeling with reusable designs for different contexts, and (ii) state-space reduction technique. Timed process automata model dynamic networks of continuous-time communicating plant processes which can activate other plant processes. We show how to establish safety and reachability properties of timed process automata by reduction to solving timed games. To mitigate the state-space explosion problem, an algorithmic state-space reduction technique using compositional reasoning and aggressive abstractions is also proposed. In this article, we demonstrate the theoretical framework of timed process automata and the effectiveness of the proposed state-space reduction technique by extending the case study.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Bagherzadeh, Mojtaba; Kahani, Nafiseh; Bezemer, Cor-Paul; Hassan, Ahmed E; Dingel, Juergen; Cordy, James R
Analyzing a Decade of Linux System Calls Journal Article
In: Empirical Software Engineering Journal, 2017.
@article{BKB+17b,
title = {Analyzing a Decade of Linux System Calls},
author = {Mojtaba Bagherzadeh and Nafiseh Kahani and Cor-Paul Bezemer and Ahmed E Hassan and Juergen Dingel and James R Cordy},
url = {https://doi.org/10.1007/s10664-017-9551-z},
doi = {10.1007/s10664-017-9551-z},
year = {2017},
date = {2017-01-01},
journal = {Empirical Software Engineering Journal},
publisher = {Springer},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Bagherzadeh, Mojtaba; Kahani, Nafiseh; Bezemer, Cor-Paul; Hassan, Ahmed E; Dingel, Juergen; Cordy, James R
Analyzing a Decade of Linux System Calls Journal Article
In: Empirical Software Engineering Journal, 2017.
@article{BKB+17,
title = {Analyzing a Decade of Linux System Calls},
author = {Mojtaba Bagherzadeh and Nafiseh Kahani and Cor-Paul Bezemer and Ahmed E Hassan and Juergen Dingel and James R Cordy},
url = {https://doi.org/10.1007/s10664-017-9551-z},
doi = {10.1007/s10664-017-9551-z},
year = {2017},
date = {2017-01-01},
journal = {Empirical Software Engineering Journal},
publisher = {Springer},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Das, Tuhin Kanti; Dingel, Juergen
Model development guidelines for UML-RT: conventions, patterns and antipatterns Journal Article
In: Software and Systems Modeling, 2016.
@article{Das2016b,
title = {Model development guidelines for UML-RT: conventions, patterns and antipatterns},
author = {Tuhin Kanti Das and Juergen Dingel},
url = {http://dx.doi.org/10.1007/s10270-016-0549-6},
doi = {10.1007/s10270-016-0549-6},
year = {2016},
date = {2016-07-23},
journal = {Software and Systems Modeling},
abstract = {Software development guidelines are a set of rules which can help improve the quality of software. These rules are defined on the basis of experience gained by the software development community over time. This paper discusses a set of design guidelines for model-based development of complex real-time embedded software systems. To be precise, we propose nine design conventions, three design patterns and thirteen antipatterns for developing UML-RT models. These guidelines have been identified based on our analysis of around 100 UML-RT models from industry and academia. Most of the guidelines are explained with the help of examples, and standard templates from the current state of the art are used for documenting the design rules.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Das, Tuhin Kanti; Dingel, Juergen
Model development guidelines for UML-RT: conventions, patterns and antipatterns Journal Article
In: Software and Systems Modeling, 2016.
@article{Das2016,
title = {Model development guidelines for UML-RT: conventions, patterns and antipatterns},
author = {Tuhin Kanti Das and Juergen Dingel},
url = {http://dx.doi.org/10.1007/s10270-016-0549-6},
doi = {10.1007/s10270-016-0549-6},
year = {2016},
date = {2016-07-23},
journal = {Software and Systems Modeling},
abstract = {Software development guidelines are a set of rules which can help improve the quality of software. These rules are defined on the basis of experience gained by the software development community over time. This paper discusses a set of design guidelines for model-based development of complex real-time embedded software systems. To be precise, we propose nine design conventions, three design patterns and thirteen antipatterns for developing UML-RT models. These guidelines have been identified based on our analysis of around 100 UML-RT models from industry and academia. Most of the guidelines are explained with the help of examples, and standard templates from the current state of the art are used for documenting the design rules.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Lúcio, Levi; Amrani, Moussa; Dingel, Juergen; Lambers, Leen; Salay, Rick; Selim, Gehan M K; Syriani, Eugene; Wimmer, Manuel
Model transformation intents and their properties Journal Article
In: Software and Systems Modeling, vol. 15, no. 3, pp. 647-684, 2016.
@article{Lucio2016b,
title = {Model transformation intents and their properties},
author = {Levi Lúcio and Moussa Amrani and Juergen Dingel and Leen Lambers and Rick Salay and Gehan M K Selim and Eugene Syriani and Manuel Wimmer},
url = {http://dx.doi.org/10.1007/s10270-014-0429-x},
doi = {10.1007/s10270-014-0429-x},
year = {2016},
date = {2016-07-01},
journal = {Software and Systems Modeling},
volume = {15},
number = {3},
pages = {647-684},
abstract = {The notion of model transformation intent is proposed to capture the purpose of a transformation. In this paper, a framework for the description of model transformation intents is defined, which includes, for instance, a description of properties a model transformation has to satisfy to qualify as a suitable realization of an intent. Several common model transformation intents are identified, and the framework is used to describe six of them in detail. A case study from the automotive industry is used to demonstrate the usefulness of the proposed framework for identifying crucial properties of model transformations with different intents and to illustrate the wide variety of model transformation intents that an industrial model-driven software development process typically encompasses.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Lúcio, Levi; Amrani, Moussa; Dingel, Juergen; Lambers, Leen; Salay, Rick; Selim, Gehan M K; Syriani, Eugene; Wimmer, Manuel
Model transformation intents and their properties Journal Article
In: Software and Systems Modeling, vol. 15, no. 3, pp. 647-684, 2016.
@article{Lucio2016,
title = {Model transformation intents and their properties},
author = {Levi Lúcio and Moussa Amrani and Juergen Dingel and Leen Lambers and Rick Salay and Gehan M K Selim and Eugene Syriani and Manuel Wimmer},
url = {http://dx.doi.org/10.1007/s10270-014-0429-x},
doi = {10.1007/s10270-014-0429-x},
year = {2016},
date = {2016-07-01},
journal = {Software and Systems Modeling},
volume = {15},
number = {3},
pages = {647-684},
abstract = {The notion of model transformation intent is proposed to capture the purpose of a transformation. In this paper, a framework for the description of model transformation intents is defined, which includes, for instance, a description of properties a model transformation has to satisfy to qualify as a suitable realization of an intent. Several common model transformation intents are identified, and the framework is used to describe six of them in detail. A case study from the automotive industry is used to demonstrate the usefulness of the proposed framework for identifying crucial properties of model transformations with different intents and to illustrate the wide variety of model transformation intents that an industrial model-driven software development process typically encompasses.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Dingel, Juergen; Schulte, Wolfram
Guest editorial for the special section on MODELS 2014 Journal Article
In: Software and Systems Modeling, 2016, (To appear).
@article{DS16b,
title = {Guest editorial for the special section on MODELS 2014},
author = {Juergen Dingel and Wolfram Schulte},
doi = {10.1007/s10270-016-0561-x},
year = {2016},
date = {2016-01-01},
journal = {Software and Systems Modeling},
publisher = {Springer},
note = {To appear},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Posse, Ernesto; Dingel, Juergen
An executable formal semantics for UML-RT Journal Article
In: Software and Systems Modeling, vol. 15, no. 1, pp. 179-217, 2016.
@article{Posse2016b,
title = {An executable formal semantics for UML-RT},
author = {Ernesto Posse and Juergen Dingel},
url = {http://dx.doi.org/10.1007/s10270-014-0399-z},
doi = {10.1007/s10270-014-0399-z},
year = {2016},
date = {2016-01-01},
journal = {Software and Systems Modeling},
volume = {15},
number = {1},
pages = {179-217},
abstract = {We propose a formal semantics for UML-RT, a UML profile for real-time and embedded systems. The formal semantics is given by mapping UML-RT models into a language called kiltera, a real-time extension of the Pi-calculus. Previous attempts to formalize the semantics of UML-RT have fallen short by considering only a very small subset of the language and providing fundamentally incomplete semantics based on incorrect assumptions, such as a one-to-one correspondence between 'capsules' and threads. Our semantics is novel in several ways: (1) it deals with both state machine diagrams and capsule diagrams; (2) it deals with aspects of UML-RT that have not been formalized before, such as thread allocation, service provision points, and service access points; (3) it supports an action language; and (4) the translation has been implemented in the form of a transformation from UML-RT models created with IBM's RSA-RTE tool, into kiltera code. To our knowledge, this is the most comprehensive formal semantics for UML-RT to date.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Dingel, Juergen; Schulte, Wolfram
Guest editorial for the special section on MODELS 2014 Journal Article
In: Software and Systems Modeling, 2016, (To appear).
@article{DS16,
title = {Guest editorial for the special section on MODELS 2014},
author = {Juergen Dingel and Wolfram Schulte},
doi = {10.1007/s10270-016-0561-x},
year = {2016},
date = {2016-01-01},
journal = {Software and Systems Modeling},
publisher = {Springer},
note = {To appear},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Posse, Ernesto; Dingel, Juergen
An executable formal semantics for UML-RT Journal Article
In: Software and Systems Modeling, vol. 15, no. 1, pp. 179-217, 2016.
@article{Posse2016,
title = {An executable formal semantics for UML-RT},
author = {Ernesto Posse and Juergen Dingel},
url = {http://dx.doi.org/10.1007/s10270-014-0399-z},
doi = {10.1007/s10270-014-0399-z},
year = {2016},
date = {2016-01-01},
journal = {Software and Systems Modeling},
volume = {15},
number = {1},
pages = {179-217},
abstract = {We propose a formal semantics for UML-RT, a UML profile for real-time and embedded systems. The formal semantics is given by mapping UML-RT models into a language called kiltera, a real-time extension of the Pi-calculus. Previous attempts to formalize the semantics of UML-RT have fallen short by considering only a very small subset of the language and providing fundamentally incomplete semantics based on incorrect assumptions, such as a one-to-one correspondence between 'capsules' and threads. Our semantics is novel in several ways: (1) it deals with both state machine diagrams and capsule diagrams; (2) it deals with aspects of UML-RT that have not been formalized before, such as thread allocation, service provision points, and service access points; (3) it supports an action language; and (4) the translation has been implemented in the form of a transformation from UML-RT models created with IBM's RSA-RTE tool, into kiltera code. To our knowledge, this is the most comprehensive formal semantics for UML-RT to date.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Amrani, Moussa; Combemale, Benoit; Lúcio, Levi; Selim, Gehan M K; Dingel, Juergen; Traon, Yves Le; Vangheluwe, Hans; Cordy, James R
Formal Verification Techniques for Model Transformations: A Tridimensional Classification Journal Article
In: Journal of Object Technology, vol. 14, no. 3, pp. 1-43, 2015, ISSN: 1660-1769.
@article{JOT:issue_2015_03/article1b,
title = {Formal Verification Techniques for Model Transformations: A Tridimensional Classification},
author = {Moussa Amrani and Benoit Combemale and Levi Lúcio and Gehan M K Selim and Juergen Dingel and Yves Le Traon and Hans Vangheluwe and James R Cordy},
url = {http://www.jot.fm/contents/issue_2015_03/article1.html},
doi = {10.5381/jot.2015.14.3.a1},
issn = {1660-1769},
year = {2015},
date = {2015-08-01},
journal = {Journal of Object Technology},
volume = {14},
number = {3},
pages = {1-43},
publisher = {Association Internationale pour les Technologies Objets (AITO)},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Amrani, Moussa; Combemale, Benoit; Lúcio, Levi; Selim, Gehan M K; Dingel, Juergen; Traon, Yves Le; Vangheluwe, Hans; Cordy, James R
Formal Verification Techniques for Model Transformations: A Tridimensional Classification Journal Article
In: Journal of Object Technology, vol. 14, no. 3, pp. 1-43, 2015, ISSN: 1660-1769.
@article{JOT:issue_2015_03/article1,
title = {Formal Verification Techniques for Model Transformations: A Tridimensional Classification},
author = {Moussa Amrani and Benoit Combemale and Levi Lúcio and Gehan M K Selim and Juergen Dingel and Yves Le Traon and Hans Vangheluwe and James R Cordy},
url = {http://www.jot.fm/contents/issue_2015_03/article1.html},
doi = {10.5381/jot.2015.14.3.a1},
issn = {1660-1769},
year = {2015},
date = {2015-08-01},
journal = {Journal of Object Technology},
volume = {14},
number = {3},
pages = {1-43},
publisher = {Association Internationale pour les Technologies Objets (AITO)},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Selim, Gehan M K; Wang, Shige; Cordy, James R; Dingel, Juergen
Model transformations for migrating legacy deployment models in the automotive industry Journal Article
In: Software and Systems Modeling, vol. 14, no. 1, pp. 365-381, 2015.
@article{Selim2015c,
title = {Model transformations for migrating legacy deployment models in the automotive industry},
author = {Gehan M K Selim and Shige Wang and James R Cordy and Juergen Dingel},
url = {http://dx.doi.org/10.1007/s10270-013-0365-1},
doi = {10.1007/s10270-013-0365-1},
year = {2015},
date = {2015-02-01},
journal = {Software and Systems Modeling},
volume = {14},
number = {1},
pages = {365-381},
abstract = {Many companies in the automotive industry have adopted model-driven development in their vehicle software development. As a major automotive company, General Motors (GM) has been using a custom-built, domain-specific modeling language, implemented as an internal proprietary metamodel, to meet the modeling needs in its control software development. Since AUTomotive Open System ARchitecture (AUTOSAR) has been developed as a standard to ease the process of integrating components provided by different suppliers and manufacturers, there has been a growing demand to migrate these GM-specific, legacy models to AUTOSAR models. Given that AUTOSAR defines its own metamodel for various system artifacts in automotive software development, we explore applying model transformations to address the challenges in migrating GM-specific, legacy models to their AUTOSAR equivalents. As a case study, we have built and validated a model transformation using the MDWorkbench tool, the Atlas Transformation Language, and the Metamodel Coverage Checker tool. This paper reports on the case study, makes observations based on our experience to assist in the development of similar types of transformations, and provides recommendations for further research.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Selim, Gehan M K; Wang, Shige; Cordy, James R; Dingel, Juergen
Model transformations for migrating legacy deployment models in the automotive industry Journal Article
In: Software and Systems Modeling, vol. 14, no. 1, pp. 365-381, 2015.
@article{Selim2015,
title = {Model transformations for migrating legacy deployment models in the automotive industry},
author = {Gehan M K Selim and Shige Wang and James R Cordy and Juergen Dingel},
url = {http://dx.doi.org/10.1007/s10270-013-0365-1},
doi = {10.1007/s10270-013-0365-1},
year = {2015},
date = {2015-02-01},
journal = {Software and Systems Modeling},
volume = {14},
number = {1},
pages = {365-381},
abstract = {Many companies in the automotive industry have adopted model-driven development in their vehicle software development. As a major automotive company, General Motors (GM) has been using a custom-built, domain-specific modeling language, implemented as an internal proprietary metamodel, to meet the modeling needs in its control software development. Since AUTomotive Open System ARchitecture (AUTOSAR) has been developed as a standard to ease the process of integrating components provided by different suppliers and manufacturers, there has been a growing demand to migrate these GM-specific, legacy models to AUTOSAR models. Given that AUTOSAR defines its own metamodel for various system artifacts in automotive software development, we explore applying model transformations to address the challenges in migrating GM-specific, legacy models to their AUTOSAR equivalents. As a case study, we have built and validated a model transformation using the MDWorkbench tool, the Atlas Transformation Language, and the Metamodel Coverage Checker tool. This paper reports on the case study, makes observations based on our experience to assist in the development of similar types of transformations, and provides recommendations for further research.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Zurowska, Karolina; Dingel, Juergen
A Customizable Execution Engine for Models of Embedded Systems Journal Article
In: pp. 82-110, 2015, ISBN: 978-3-319-21911-0.
@article{Zurowska:2015:CEE:2977726.2977732b,
title = {A Customizable Execution Engine for Models of Embedded Systems},
author = {Karolina Zurowska and Juergen Dingel},
url = {http://dx.doi.org/10.1007/978-3-319-21912-7_4},
doi = {10.1007/978-3-319-21912-7_4},
isbn = {978-3-319-21911-0},
year = {2015},
date = {2015-01-01},
booktitle = {Revised Selected Papers of the International Workshops on Behavior Modeling - Foundations and Applications},
pages = {82-110},
publisher = {Springer},
address = {New York, NY, USA},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Zurowska, Karolina; Dingel, Juergen
A Customizable Execution Engine for Models of Embedded Systems Journal Article
In: pp. 82-110, 2015, ISBN: 978-3-319-21911-0.
@article{Zurowska:2015:CEE:2977726.2977732,
title = {A Customizable Execution Engine for Models of Embedded Systems},
author = {Karolina Zurowska and Juergen Dingel},
url = {http://dx.doi.org/10.1007/978-3-319-21912-7_4},
doi = {10.1007/978-3-319-21912-7_4},
isbn = {978-3-319-21911-0},
year = {2015},
date = {2015-01-01},
booktitle = {Revised Selected Papers of the International Workshops on Behavior Modeling - Foundations and Applications},
pages = {82-110},
publisher = {Springer},
address = {New York, NY, USA},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Auer, Anthony; Dingel, Juergen; Rudie, Karen
Concurrency control generation for dynamic threads using discrete-event systems Journal Article
In: Science of Computer Programming, vol. 82, pp. 22 - 43, 2014, ISSN: 0167-6423, (Special Issue on Automated Verification of Critical Systems (AVoCS'11)).
@article{AUER201422b,
title = {Concurrency control generation for dynamic threads using discrete-event systems},
author = {Anthony Auer and Juergen Dingel and Karen Rudie},
url = {http://www.sciencedirect.com/science/article/pii/S0167642313000208},
doi = {http://dx.doi.org/10.1016/j.scico.2013.01.007},
issn = {0167-6423},
year = {2014},
date = {2014-01-01},
journal = {Science of Computer Programming},
volume = {82},
pages = {22 - 43},
note = {Special Issue on Automated Verification of Critical Systems (AVoCS'11)},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Auer, Anthony; Dingel, Juergen; Rudie, Karen
Concurrency control generation for dynamic threads using discrete-event systems Journal Article
In: Science of Computer Programming, vol. 82, pp. 22 - 43, 2014, ISSN: 0167-6423, (Special Issue on Automated Verification of Critical Systems (AVoCS'11)).
@article{AUER201422,
title = {Concurrency control generation for dynamic threads using discrete-event systems},
author = {Anthony Auer and Juergen Dingel and Karen Rudie},
url = {http://www.sciencedirect.com/science/article/pii/S0167642313000208},
doi = {http://dx.doi.org/10.1016/j.scico.2013.01.007},
issn = {0167-6423},
year = {2014},
date = {2014-01-01},
journal = {Science of Computer Programming},
volume = {82},
pages = {22 - 43},
note = {Special Issue on Automated Verification of Critical Systems (AVoCS'11)},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Moffett, Yann; Dingel, Juergen; Beaulieu, Alain
Verifying Protocol Conformance Using Software Model Checking for the Model-Driven Development of Embedded Systems Journal Article
In: IEEE Transactions on Software Engineering, vol. 39, no. 9, pp. 1307-13256, 2013, ISSN: 0098-5589.
@article{6482140b,
title = {Verifying Protocol Conformance Using Software Model Checking for the Model-Driven Development of Embedded Systems},
author = {Yann Moffett and Juergen Dingel and Alain Beaulieu},
url = {http://ieeexplore.ieee.org/document/6482140},
doi = {10.1109/TSE.2013.14},
issn = {0098-5589},
year = {2013},
date = {2013-09-01},
journal = {IEEE Transactions on Software Engineering},
volume = {39},
number = {9},
pages = {1307-13256},
publisher = {IEEE},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Moffett, Yann; Dingel, Juergen; Beaulieu, Alain
Verifying Protocol Conformance Using Software Model Checking for the Model-Driven Development of Embedded Systems Journal Article
In: IEEE Transactions on Software Engineering, vol. 39, no. 9, pp. 1307-13256, 2013, ISSN: 0098-5589.
@article{6482140,
title = {Verifying Protocol Conformance Using Software Model Checking for the Model-Driven Development of Embedded Systems},
author = {Yann Moffett and Juergen Dingel and Alain Beaulieu},
url = {http://ieeexplore.ieee.org/document/6482140},
doi = {10.1109/TSE.2013.14},
issn = {0098-5589},
year = {2013},
date = {2013-09-01},
journal = {IEEE Transactions on Software Engineering},
volume = {39},
number = {9},
pages = {1307-13256},
publisher = {IEEE},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Waez, Md Tawhid Bin; Dingel, Juergen; Rudie, Karen
A survey of timed automata for the development of real-time systems Journal Article
In: Computer Science Review, vol. 9, pp. 1 - 26, 2013, ISSN: 1574-0137.
@article{WAEZ20131b,
title = {A survey of timed automata for the development of real-time systems},
author = {Md Tawhid Bin Waez and Juergen Dingel and Karen Rudie},
url = {http://www.sciencedirect.com/science/article/pii/S1574013713000178},
doi = {http://dx.doi.org/10.1016/j.cosrev.2013.05.001},
issn = {1574-0137},
year = {2013},
date = {2013-01-01},
journal = {Computer Science Review},
volume = {9},
pages = {1 - 26},
publisher = {Elsevier},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Waez, Md Tawhid Bin; Dingel, Juergen; Rudie, Karen
A survey of timed automata for the development of real-time systems Journal Article
In: Computer Science Review, vol. 9, pp. 1 - 26, 2013, ISSN: 1574-0137.
@article{WAEZ20131,
title = {A survey of timed automata for the development of real-time systems},
author = {Md Tawhid Bin Waez and Juergen Dingel and Karen Rudie},
url = {http://www.sciencedirect.com/science/article/pii/S1574013713000178},
doi = {http://dx.doi.org/10.1016/j.cosrev.2013.05.001},
issn = {1574-0137},
year = {2013},
date = {2013-01-01},
journal = {Computer Science Review},
volume = {9},
pages = {1 - 26},
publisher = {Elsevier},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Dingel, Juergen; Diskin, Zinovy; Zito, Alanna
Understanding and improving UML package merge Journal Article
In: Software and Systems Modeling, vol. 7, no. 4, pp. 443-467, 2008.
@article{Dingel2008b,
title = {Understanding and improving UML package merge},
author = {Juergen Dingel and Zinovy Diskin and Alanna Zito},
url = {http://dx.doi.org/10.1007/s10270-007-0073-9},
doi = {10.1007/s10270-007-0073-9},
year = {2008},
date = {2008-10-01},
journal = {Software and Systems Modeling},
volume = {7},
number = {4},
pages = {443-467},
abstract = {Package merge allows the content of one package to be combined with that of another package. Package merge is used extensively in the UML 2 specification to modularize the definition of the UML 2 meta model and to define the four compliance levels of UML 2. Package merge is a novel construct in UML and currently not well understood. This paper summarizes our work to understand and improve package merge. First, we identify ambiguous and missing rules in the package merge definition and suggest corrections. Then, we formalize package merge and analyze it with respect to some desirable properties. Our analyses employs Alloy, a first-order modelling language with tool support, and concepts from mathematical logic which allow us to develop a general taxonomy of package extension mechanisms. The analyses reveal the unexpected failure of important properties.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Dingel, Juergen; Diskin, Zinovy; Zito, Alanna
Understanding and improving UML package merge Journal Article
In: Software and Systems Modeling, vol. 7, no. 4, pp. 443-467, 2008.
@article{Dingel2008,
title = {Understanding and improving UML package merge},
author = {Juergen Dingel and Zinovy Diskin and Alanna Zito},
url = {http://dx.doi.org/10.1007/s10270-007-0073-9},
doi = {10.1007/s10270-007-0073-9},
year = {2008},
date = {2008-10-01},
journal = {Software and Systems Modeling},
volume = {7},
number = {4},
pages = {443-467},
abstract = {Package merge allows the content of one package to be combined with that of another package. Package merge is used extensively in the UML 2 specification to modularize the definition of the UML 2 meta model and to define the four compliance levels of UML 2. Package merge is a novel construct in UML and currently not well understood. This paper summarizes our work to understand and improve package merge. First, we identify ambiguous and missing rules in the package merge definition and suggest corrections. Then, we formalize package merge and analyze it with respect to some desirable properties. Our analyses employs Alloy, a first-order modelling language with tool support, and concepts from mathematical logic which allow us to develop a general taxonomy of package extension mechanisms. The analyses reveal the unexpected failure of important properties.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Crane, Michelle L; Dingel, Juergen
UML vs. Classical vs. Rhapsody statecharts: not all models are created equal Journal Article
In: Software and Systems Modeling, vol. 6, no. 4, pp. 415-435, 2007.
@article{DBLP:journals/sosym/CraneD07b,
title = {UML vs. Classical vs. Rhapsody statecharts: not all models are created equal},
author = {Michelle L Crane and Juergen Dingel},
url = {https://doi.org/10.1007/s10270-006-0042-8},
doi = {10.1007/s10270-006-0042-8},
year = {2007},
date = {2007-01-01},
journal = {Software and Systems Modeling},
volume = {6},
number = {4},
pages = {415-435},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Crane, Michelle L; Dingel, Juergen
UML vs. Classical vs. Rhapsody statecharts: not all models are created equal Journal Article
In: Software and Systems Modeling, vol. 6, no. 4, pp. 415-435, 2007.
@article{DBLP:journals/sosym/CraneD07,
title = {UML vs. Classical vs. Rhapsody statecharts: not all models are created equal},
author = {Michelle L Crane and Juergen Dingel},
url = {https://doi.org/10.1007/s10270-006-0042-8},
doi = {10.1007/s10270-006-0042-8},
year = {2007},
date = {2007-01-01},
journal = {Software and Systems Modeling},
volume = {6},
number = {4},
pages = {415-435},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Zhang, Hongyu; Bradbury, Jeremy S; Cordy, James R; Dingel, Juergen
Using source transformation to test and model check implicit-invocation systems Journal Article
In: Science of Computer Programming, vol. 62, no. 3, pp. 209 - 227, 2006, ISSN: 0167-6423, (Special issue on Source code analysis and manipulation (SCAM 2005)).
@article{ZHANG2006209,
title = {Using source transformation to test and model check implicit-invocation systems},
author = {Hongyu Zhang and Jeremy S Bradbury and James R Cordy and Juergen Dingel},
url = {http://www.sciencedirect.com/science/article/pii/S0167642306000955},
doi = {http://dx.doi.org/10.1016/j.scico.2006.04.008},
issn = {0167-6423},
year = {2006},
date = {2006-01-01},
journal = {Science of Computer Programming},
volume = {62},
number = {3},
pages = {209 - 227},
note = {Special issue on Source code analysis and manipulation (SCAM 2005)},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Dingel, Juergen
Compositional Analysis of C/C++ Programs with VeriSoft Journal Article
In: Acta Informatica, vol. 43, no. 1, pp. 45-71, 2006, ISSN: 0001-5903.
@article{Dingel:2006:CAC:1148011.1148013,
title = {Compositional Analysis of C/C++ Programs with VeriSoft},
author = {Juergen Dingel},
url = {http://dx.doi.org/10.1007/s00236-006-0016-x},
doi = {10.1007/s00236-006-0016-x},
issn = {0001-5903},
year = {2006},
date = {2006-01-01},
journal = {Acta Informatica},
volume = {43},
number = {1},
pages = {45-71},
publisher = {Springer},
address = {Secaucus, NJ, USA},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Zhang, Hongyu; Bradbury, Jeremy S; Cordy, James R; Dingel, Juergen
Using source transformation to test and model check implicit-invocation systems Journal Article
In: Science of Computer Programming, vol. 62, no. 3, pp. 209 - 227, 2006, ISSN: 0167-6423, (Special issue on Source code analysis and manipulation (SCAM 2005)).
@article{ZHANG2006209b,
title = {Using source transformation to test and model check implicit-invocation systems},
author = {Hongyu Zhang and Jeremy S Bradbury and James R Cordy and Juergen Dingel},
url = {http://www.sciencedirect.com/science/article/pii/S0167642306000955},
doi = {http://dx.doi.org/10.1016/j.scico.2006.04.008},
issn = {0167-6423},
year = {2006},
date = {2006-01-01},
journal = {Science of Computer Programming},
volume = {62},
number = {3},
pages = {209 - 227},
note = {Special issue on Source code analysis and manipulation (SCAM 2005)},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Dingel, Juergen
Compositional Analysis of C/C++ Programs with VeriSoft Journal Article
In: Acta Informatica, vol. 43, no. 1, pp. 45-71, 2006, ISSN: 0001-5903.
@article{Dingel:2006:CAC:1148011.1148013b,
title = {Compositional Analysis of C/C++ Programs with VeriSoft},
author = {Juergen Dingel},
url = {http://dx.doi.org/10.1007/s00236-006-0016-x},
doi = {10.1007/s00236-006-0016-x},
issn = {0001-5903},
year = {2006},
date = {2006-01-01},
journal = {Acta Informatica},
volume = {43},
number = {1},
pages = {45-71},
publisher = {Springer},
address = {Secaucus, NJ, USA},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Cassidy, Timothy; Cordy, James R; Dean, Thomas R; Dingel, Juergen
Source Transformation for Concurrency Analysis Journal Article
In: Electron. Notes Theor. Comput. Sci., vol. 141, no. 4, pp. 57-75, 2005, ISSN: 1571-0661.
@article{Cassidy:2005:STC:1705513.1705661,
title = {Source Transformation for Concurrency Analysis},
author = {Timothy Cassidy and James R Cordy and Thomas R Dean and Juergen Dingel},
url = {http://dx.doi.org/10.1016/j.entcs.2005.05.012},
doi = {10.1016/j.entcs.2005.05.012},
issn = {1571-0661},
year = {2005},
date = {2005-01-01},
journal = {Electron. Notes Theor. Comput. Sci.},
volume = {141},
number = {4},
pages = {57-75},
publisher = {Elsevier},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Cassidy, Timothy; Cordy, James R; Dean, Thomas R; Dingel, Juergen
Source Transformation for Concurrency Analysis Journal Article
In: Electron. Notes Theor. Comput. Sci., vol. 141, no. 4, pp. 57-75, 2005, ISSN: 1571-0661.
@article{Cassidy:2005:STC:1705513.1705661b,
title = {Source Transformation for Concurrency Analysis},
author = {Timothy Cassidy and James R Cordy and Thomas R Dean and Juergen Dingel},
url = {http://dx.doi.org/10.1016/j.entcs.2005.05.012},
doi = {10.1016/j.entcs.2005.05.012},
issn = {1571-0661},
year = {2005},
date = {2005-01-01},
journal = {Electron. Notes Theor. Comput. Sci.},
volume = {141},
number = {4},
pages = {57-75},
publisher = {Elsevier},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Dingel, Juergen
A Refinement Calculus for Shared-Variable Parallel and Distributed Programming Journal Article
In: Formal Aspects of Computing, vol. 14, no. 2, pp. 123-197, 2002, ISSN: 1433-299X.
@article{Dingel2002,
title = {A Refinement Calculus for Shared-Variable Parallel and Distributed Programming},
author = {Juergen Dingel},
url = {http://dx.doi.org/10.1007/s001650200032},
doi = {10.1007/s001650200032},
issn = {1433-299X},
year = {2002},
date = {2002-12-01},
journal = {Formal Aspects of Computing},
volume = {14},
number = {2},
pages = {123-197},
abstract = {Parallel computers have not yet had the expected impact on mainstream computing. Parallelism adds a level of complexity to the programming task that makes it very error-prone. Moreover, a large variety of very different parallel architectures exists. Porting an implementation from one machine to another may require substantial changes. This paper addresses some of these problems by developing a formal basis for the design of parallel programs in the form of a refinement calculus. The calculus allows the stepwise formal derivation of an abstract, low-level implementation from a trusted, high-level specification. The calculus thus helps structuring and documenting the development process. Portability is increased, because the introduction of a machine-dependent feature can be located in the refinement tree. Development efforts above this point in the tree are independent of that feature and are thus reusable. Moreover, the discovery of new, possibly more efficient solutions is facilitated. Last but not least, programs are correct by construction, which obviates the need for difficult debugging. Our programming/specification notation supports fair parallelism, shared-variable and message-passing concurrency, local variables and channels. The calculus rests on a compositional trace semantics that treats shared-variable and message-passing concurrency uniformly. The refinement relation combines a context-sensitive notion of trace inclusion and assumption-commitment reasoning to achieve compositionality. The calculus straddles both concurrency paradigms, that is, a shared-variable program can be refined into a distributed, message-passing program and vice versa.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Dingel, Juergen
A Refinement Calculus for Shared-Variable Parallel and Distributed Programming Journal Article
In: Formal Aspects of Computing, vol. 14, no. 2, pp. 123-197, 2002, ISSN: 1433-299X.
@article{Dingel2002b,
title = {A Refinement Calculus for Shared-Variable Parallel and Distributed Programming},
author = {Juergen Dingel},
url = {http://dx.doi.org/10.1007/s001650200032},
doi = {10.1007/s001650200032},
issn = {1433-299X},
year = {2002},
date = {2002-12-01},
journal = {Formal Aspects of Computing},
volume = {14},
number = {2},
pages = {123-197},
abstract = {Parallel computers have not yet had the expected impact on mainstream computing. Parallelism adds a level of complexity to the programming task that makes it very error-prone. Moreover, a large variety of very different parallel architectures exists. Porting an implementation from one machine to another may require substantial changes. This paper addresses some of these problems by developing a formal basis for the design of parallel programs in the form of a refinement calculus. The calculus allows the stepwise formal derivation of an abstract, low-level implementation from a trusted, high-level specification. The calculus thus helps structuring and documenting the development process. Portability is increased, because the introduction of a machine-dependent feature can be located in the refinement tree. Development efforts above this point in the tree are independent of that feature and are thus reusable. Moreover, the discovery of new, possibly more efficient solutions is facilitated. Last but not least, programs are correct by construction, which obviates the need for difficult debugging. Our programming/specification notation supports fair parallelism, shared-variable and message-passing concurrency, local variables and channels. The calculus rests on a compositional trace semantics that treats shared-variable and message-passing concurrency uniformly. The refinement relation combines a context-sensitive notion of trace inclusion and assumption-commitment reasoning to achieve compositionality. The calculus straddles both concurrency paradigms, that is, a shared-variable program can be refined into a distributed, message-passing program and vice versa.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}