Using a DSL and fine-grained model : transformations to explore the boundaries of model verification

M.F. Amstel, van, M.G.J. Brand, van den, L.J.P. Engelen

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

55 Downloads (Pure)

Abstract

Traditionally, the state-space explosion problem in model checking is handled by applying abstractions and simplifications to the model that needs to be verified. In this paper, we propose a model-driven engineering approach that works the other way around. Instead of making a concrete model more abstract, we propose to refine an abstract model to make it more concrete. We propose to use fine-grained model transformations to enable model checking of models that are as close to the implementation model as possible. We applied our approach in a case study. The results show that it is possible to validate models that are more concrete when fine-grained transformations are applied.
Original languageEnglish
Title of host publicationProceedings of the 2011 Fifth International Conference on Secure Software Integration and Reliability Improvement (SSIRI, Jeju Island, South Korea, June 27-29, 2011)
PublisherInstitute of Electrical and Electronics Engineers
Pages120-127
ISBN (Print)978-1-4577-0781-0
DOIs
Publication statusPublished - 2011

Fingerprint

DSL
Model checking
Concretes
Explosions

Cite this

Amstel, van, M. F., Brand, van den, M. G. J., & Engelen, L. J. P. (2011). Using a DSL and fine-grained model : transformations to explore the boundaries of model verification. In Proceedings of the 2011 Fifth International Conference on Secure Software Integration and Reliability Improvement (SSIRI, Jeju Island, South Korea, June 27-29, 2011) (pp. 120-127). Institute of Electrical and Electronics Engineers. https://doi.org/10.1109/SSIRI-C.2011.26
Amstel, van, M.F. ; Brand, van den, M.G.J. ; Engelen, L.J.P. / Using a DSL and fine-grained model : transformations to explore the boundaries of model verification. Proceedings of the 2011 Fifth International Conference on Secure Software Integration and Reliability Improvement (SSIRI, Jeju Island, South Korea, June 27-29, 2011). Institute of Electrical and Electronics Engineers, 2011. pp. 120-127
@inproceedings{6d996c1ce7b7427e907eaad3f8f8923d,
title = "Using a DSL and fine-grained model : transformations to explore the boundaries of model verification",
abstract = "Traditionally, the state-space explosion problem in model checking is handled by applying abstractions and simplifications to the model that needs to be verified. In this paper, we propose a model-driven engineering approach that works the other way around. Instead of making a concrete model more abstract, we propose to refine an abstract model to make it more concrete. We propose to use fine-grained model transformations to enable model checking of models that are as close to the implementation model as possible. We applied our approach in a case study. The results show that it is possible to validate models that are more concrete when fine-grained transformations are applied.",
author = "{Amstel, van}, M.F. and {Brand, van den}, M.G.J. and L.J.P. Engelen",
year = "2011",
doi = "10.1109/SSIRI-C.2011.26",
language = "English",
isbn = "978-1-4577-0781-0",
pages = "120--127",
booktitle = "Proceedings of the 2011 Fifth International Conference on Secure Software Integration and Reliability Improvement (SSIRI, Jeju Island, South Korea, June 27-29, 2011)",
publisher = "Institute of Electrical and Electronics Engineers",
address = "United States",

}

Amstel, van, MF, Brand, van den, MGJ & Engelen, LJP 2011, Using a DSL and fine-grained model : transformations to explore the boundaries of model verification. in Proceedings of the 2011 Fifth International Conference on Secure Software Integration and Reliability Improvement (SSIRI, Jeju Island, South Korea, June 27-29, 2011). Institute of Electrical and Electronics Engineers, pp. 120-127. https://doi.org/10.1109/SSIRI-C.2011.26

Using a DSL and fine-grained model : transformations to explore the boundaries of model verification. / Amstel, van, M.F.; Brand, van den, M.G.J.; Engelen, L.J.P.

Proceedings of the 2011 Fifth International Conference on Secure Software Integration and Reliability Improvement (SSIRI, Jeju Island, South Korea, June 27-29, 2011). Institute of Electrical and Electronics Engineers, 2011. p. 120-127.

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - Using a DSL and fine-grained model : transformations to explore the boundaries of model verification

AU - Amstel, van, M.F.

AU - Brand, van den, M.G.J.

AU - Engelen, L.J.P.

PY - 2011

Y1 - 2011

N2 - Traditionally, the state-space explosion problem in model checking is handled by applying abstractions and simplifications to the model that needs to be verified. In this paper, we propose a model-driven engineering approach that works the other way around. Instead of making a concrete model more abstract, we propose to refine an abstract model to make it more concrete. We propose to use fine-grained model transformations to enable model checking of models that are as close to the implementation model as possible. We applied our approach in a case study. The results show that it is possible to validate models that are more concrete when fine-grained transformations are applied.

AB - Traditionally, the state-space explosion problem in model checking is handled by applying abstractions and simplifications to the model that needs to be verified. In this paper, we propose a model-driven engineering approach that works the other way around. Instead of making a concrete model more abstract, we propose to refine an abstract model to make it more concrete. We propose to use fine-grained model transformations to enable model checking of models that are as close to the implementation model as possible. We applied our approach in a case study. The results show that it is possible to validate models that are more concrete when fine-grained transformations are applied.

U2 - 10.1109/SSIRI-C.2011.26

DO - 10.1109/SSIRI-C.2011.26

M3 - Conference contribution

SN - 978-1-4577-0781-0

SP - 120

EP - 127

BT - Proceedings of the 2011 Fifth International Conference on Secure Software Integration and Reliability Improvement (SSIRI, Jeju Island, South Korea, June 27-29, 2011)

PB - Institute of Electrical and Electronics Engineers

ER -

Amstel, van MF, Brand, van den MGJ, Engelen LJP. Using a DSL and fine-grained model : transformations to explore the boundaries of model verification. In Proceedings of the 2011 Fifth International Conference on Secure Software Integration and Reliability Improvement (SSIRI, Jeju Island, South Korea, June 27-29, 2011). Institute of Electrical and Electronics Engineers. 2011. p. 120-127 https://doi.org/10.1109/SSIRI-C.2011.26