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

doi:10.1109/SSIRI-C.2011.26

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 proceeding › Conference contribution › Academic › peer-review

124 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 language	English
Title of host publication	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
Pages	120-127
ISBN (Print)	978-1-4577-0781-0
DOIs	https://doi.org/10.1109/SSIRI-C.2011.26
Publication status	Published - 2011

Access to Document

10.1109/SSIRI-C.2011.26

publishers versionFinal published version, 381 KB

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 proceeding › Conference contribution › Academic › peer-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

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

Abstract

Access to Document

Fingerprint

Cite this