Publications Search Tool

@inproceedings{PD14b,

title = {Contract-based Specification and Analysis of AADL models},

author = {Ernesto Posse and Juergen Dingel},

url = {ceur-ws.org/Vol-1233},

year  = {2014},

date = {2014-01-01},

booktitle = {Architecture Centric Virtual Integration Workshop (ACVI'14)},

volume = {CEUR},

number = {1233},

address = {Valencia, Spain. September 29, 2014},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{Selim2014b,

title = {Specification and Verification of Graph-Based Model Transformation Properties},

author = {Gehan M K Selim and Levi Lúcio and James R Cordy and Juergen Dingel and Bentley J Oakes},

url = {http://dx.doi.org/10.1007/978-3-319-09108-2_8},

doi = {10.1007/978-3-319-09108-2_8},

isbn = {978-3-319-09108-2},

year  = {2014},

date = {2014-01-01},

booktitle = {7th International Conference on Graph Transformation (ICGT'14)},

pages = {113-129},

publisher = {Springer},

address = {York, UK. July 22-24, 2014},

abstract = {We extend a previously proposed symbolic model transformation property prover for the DSLTrans transformation language. The original prover generated the set of path conditions (i.e., symbolic transformation executions), and verified atomic contracts (constraints on input-output model relations) on these path conditions. The prover evaluated atomic contracts to yield either true or false for the transformation when run on any input model. In this paper we extend the prover such that it can verify atomic contracts and more complex properties composed of atomic contracts. Besides demonstrating our prover on a simple transformation, we use it to verify different kinds of properties of an industrial transformation. Experiments on this transformation using our prover show a speed-up in verification run-time by two orders of magnitude over another verification tool that we evaluated in previous research.},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{PD14,

title = {Contract-based Specification and Analysis of AADL models},

author = {Ernesto Posse and Juergen Dingel},

url = {ceur-ws.org/Vol-1233},

year  = {2014},

date = {2014-01-01},

booktitle = {Architecture Centric Virtual Integration Workshop (ACVI'14)},

volume = {CEUR},

number = {1233},

address = {Valencia, Spain. September 29, 2014},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{Selim2014,

title = {Specification and Verification of Graph-Based Model Transformation Properties},

author = {Gehan M K Selim and Levi Lúcio and James R Cordy and Juergen Dingel and Bentley J Oakes},

url = {http://dx.doi.org/10.1007/978-3-319-09108-2_8},

doi = {10.1007/978-3-319-09108-2_8},

isbn = {978-3-319-09108-2},

year  = {2014},

date = {2014-01-01},

booktitle = {7th International Conference on Graph Transformation (ICGT'14)},

pages = {113-129},

publisher = {Springer},

address = {York, UK. July 22-24, 2014},

abstract = {We extend a previously proposed symbolic model transformation property prover for the DSLTrans transformation language. The original prover generated the set of path conditions (i.e., symbolic transformation executions), and verified atomic contracts (constraints on input-output model relations) on these path conditions. The prover evaluated atomic contracts to yield either true or false for the transformation when run on any input model. In this paper we extend the prover such that it can verify atomic contracts and more complex properties composed of atomic contracts. Besides demonstrating our prover on a simple transformation, we use it to verify different kinds of properties of an industrial transformation. Experiments on this transformation using our prover show a speed-up in verification run-time by two orders of magnitude over another verification tool that we evaluated in previous research.},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{Zurowska2013,

title = {Model Checking of UML-RT Models Using Lazy Composition},

author = {Karolina Zurowska and Juergen Dingel},

url = {http://dx.doi.org/10.1007/978-3-642-41533-3_19},

doi = {10.1007/978-3-642-41533-3_19},

isbn = {978-3-642-41533-3},

year  = {2013},

date = {2013-01-01},

booktitle = {ACM/IEEE 16th International Conference on Model-Driven Engineering Languages and Systems (MODELS'13)},

pages = {304-319},

publisher = {Springer},

address = {Miami, FL, USA. September 29 - October 4, 2013},

abstract = {Formal analysis of models is an important aspect of the Model Driven Development (MDD) paradigm. In this paper we introduce a technique to analyze models with hierarchically organized and asynchronously communicating components as found in, e.g., UML-RT. Typically, the more components are composed during analysis, the less scalable it becomes. In our technique we reduce composition by leveraging the communication topology and the property to be checked. To this end we introduce an extension of Computation Tree Logic (CTL) to express properties of models and we show an algorithm to check such properties. In the algorithm, components are represented by their symbolic execution trees and their composition is lazy, i.e., only performed when necessary. To demonstrate some of the benefits of the technique, its implementation for UML-RT models and case studies are discussed.},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{Selim2013,

title = {Automated Verification of Model Transformations in the Automotive Industry},

author = {Gehan M K Selim and Fabian Büttner and James R Cordy and Juergen Dingel and Shige Wang},

url = {http://dx.doi.org/10.1007/978-3-642-41533-3_42},

doi = {10.1007/978-3-642-41533-3_42},

isbn = {978-3-642-41533-3},

year  = {2013},

date = {2013-01-01},

booktitle = {ACM/IEEE 16th International Conference on Model-Driven Engineering Languages and Systems (MODELS'13)},

pages = {690-706},

publisher = {Springer},

address = {Miami, FL, USA. September 29 - October 4, 2013},

abstract = {Many companies have adopted MDD for developing their software systems. Several studies have reported on such industrial experiences by discussing the effects of MDD and the issues that still need to be addressed. However, only a few studies have discussed using automated verification of industrial model transformations. We previously demonstrated how transformations can be used to migrate GM legacy models to AUTOSAR models. In this study, we investigate using automated verification for such industrial transformations. We report on applying an automated verification approach to the GM-to-AUTOSAR transformation that is based on checking the satisfiability of a relational transformation representation, or a transformation model, with respect to well-formedness OCL constraints. An implementation of this approach is available as a prototype for the ATL language. We present the verification results of this transformation and discuss the practicality of using such tools on industrial size problems.},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{Zurowska2013b,

title = {Model Checking of UML-RT Models Using Lazy Composition},

author = {Karolina Zurowska and Juergen Dingel},

url = {http://dx.doi.org/10.1007/978-3-642-41533-3_19},

doi = {10.1007/978-3-642-41533-3_19},

isbn = {978-3-642-41533-3},

year  = {2013},

date = {2013-01-01},

booktitle = {ACM/IEEE 16th International Conference on Model-Driven Engineering Languages and Systems (MODELS'13)},

pages = {304-319},

publisher = {Springer},

address = {Miami, FL, USA. September 29 - October 4, 2013},

abstract = {Formal analysis of models is an important aspect of the Model Driven Development (MDD) paradigm. In this paper we introduce a technique to analyze models with hierarchically organized and asynchronously communicating components as found in, e.g., UML-RT. Typically, the more components are composed during analysis, the less scalable it becomes. In our technique we reduce composition by leveraging the communication topology and the property to be checked. To this end we introduce an extension of Computation Tree Logic (CTL) to express properties of models and we show an algorithm to check such properties. In the algorithm, components are represented by their symbolic execution trees and their composition is lazy, i.e., only performed when necessary. To demonstrate some of the benefits of the technique, its implementation for UML-RT models and case studies are discussed.},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{Selim2013b,

title = {Automated Verification of Model Transformations in the Automotive Industry},

author = {Gehan M K Selim and Fabian Büttner and James R Cordy and Juergen Dingel and Shige Wang},

url = {http://dx.doi.org/10.1007/978-3-642-41533-3_42},

doi = {10.1007/978-3-642-41533-3_42},

isbn = {978-3-642-41533-3},

year  = {2013},

date = {2013-01-01},

booktitle = {ACM/IEEE 16th International Conference on Model-Driven Engineering Languages and Systems (MODELS'13)},

pages = {690-706},

publisher = {Springer},

address = {Miami, FL, USA. September 29 - October 4, 2013},

abstract = {Many companies have adopted MDD for developing their software systems. Several studies have reported on such industrial experiences by discussing the effects of MDD and the issues that still need to be addressed. However, only a few studies have discussed using automated verification of industrial model transformations. We previously demonstrated how transformations can be used to migrate GM legacy models to AUTOSAR models. In this study, we investigate using automated verification for such industrial transformations. We report on applying an automated verification approach to the GM-to-AUTOSAR transformation that is based on checking the satisfiability of a relational transformation representation, or a transformation model, with respect to well-formedness OCL constraints. An implementation of this approach is available as a prototype for the ATL language. We present the verification results of this transformation and discuss the practicality of using such tools on industrial size problems.},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}