Paper Info
Title
Module Isolation for Efficient Model Checking and its Application to FMEA in Model-driven Engineering.
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.
Year
DOI
Venue
2013
10.5220/0004557502180225
ENASE: PROCEEDINGS OF THE 8TH INTERNATIONAL CONFERENCE ON EVALUATION OF NOVEL APPROACHES TO SOFTWARE ENGINEERING
Keywords
Field
DocType
Model-driven Engineering,Formal Methods,Software Modelling,Failure Mode Effects Analysis
Model checking,Systems engineering,Model-driven architecture,Engineering
Conference
Citations 
PageRank 
References 
5
0.43
0
Authors
2
Name
Order
Citations
PageRank
vladimir estivillcastro1903107.50
René Hexel27912.65