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

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/Congresprocedure › Conferentiebijdrage › Academic › peer review

1 Citaat (Scopus)

161 Downloads (Pure)

Samenvatting

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.

Originele taal-2	Engels
Titel	Proceedings of the 2011 Fifth International Conference on Secure Software Integration and Reliability Improvement (SSIRI, Jeju Island, South Korea, June 27-29, 2011)
Uitgeverij	Institute of Electrical and Electronics Engineers
Pagina's	120-127
ISBN van geprinte versie	978-1-4577-0781-0
DOI's	https://doi.org/10.1109/SSIRI-C.2011.26
Status	Gepubliceerd - 2011

Toegang tot document

10.1109/SSIRI-C.2011.26

publishers versionDefinitieve gepubliceerde versie, 381 KB

Citeer dit

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) (blz. 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. blz. 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, blz. 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. blz. 120-127.

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/Congresprocedure › Conferentiebijdrage › 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. blz. 120-127 doi: 10.1109/SSIRI-C.2011.26

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

Samenvatting

Toegang tot document

Vingerafdruk

Citeer dit