Module Isolation for Efficient Model Checking and its Application to FMEA in Model-driven Engineering

Vladimir Estivill-Castro, René Hexel

2013

Abstract

Model-driven development results in directly runnable implementations, and therefore it is of utmost importance to formally verify and validate such models. However, model-checking usually faces the challenge of concurrent modules generating a state space equal to the Cartesian product of the state spaces of all modules. This is even more dramatic as recent trends in model-driven-engineering aim at not only modelling the software in question, but other components of the system as well, in order to perform Failure Mode Effects Analysis (FMEA). These additional components further enlarge the collective state space. We provide an algorithm that identifies the sections of the system that are independent, enabling verification of separate sections of the system. As a consequence, formal verification of the system as well as the corresponding FMEA can be performed much more efficiently.

Paper Citation

in Harvard Style

Estivill-Castro V. and Hexel R. (2013). Module Isolation for Efficient Model Checking and its Application to FMEA in Model-driven Engineering . In Proceedings of the 8th International Conference on Evaluation of Novel Approaches to Software Engineering - Volume 1: ENASE, ISBN 978-989-8565-62-4, pages 218-225. DOI: 10.5220/0004557502180225

in Bibtex Style

@conference{enase13,
author={Vladimir Estivill-Castro and René Hexel},
title={Module Isolation for Efficient Model Checking and its Application to FMEA in Model-driven Engineering},
booktitle={Proceedings of the 8th International Conference on Evaluation of Novel Approaches to Software Engineering - Volume 1: ENASE,},
year={2013},
pages={218-225},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0004557502180225},
isbn={978-989-8565-62-4},
}

in EndNote Style

TY - CONF
JO - Proceedings of the 8th International Conference on Evaluation of Novel Approaches to Software Engineering - Volume 1: ENASE,
TI - Module Isolation for Efficient Model Checking and its Application to FMEA in Model-driven Engineering
SN - 978-989-8565-62-4
AU - Estivill-Castro V.
AU - Hexel R.
PY - 2013
SP - 218
EP - 225
DO - 10.5220/0004557502180225