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

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

doi:10.1109/ICSTW.2011.8

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

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

5 Citations (Scopus)

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 models that are more concrete can be validated when fine-grained transformations are applied.

Original language	English
Title of host publication	Proceedings of the 2011 IEEE Fourth International Conference on Software Testing, Verification and Validation Workshops (ICSTW 2011, Berlin, Germany, March 21-25, 2011)
Place of Publication	Piscataway
Publisher	Institute of Electrical and Electronics Engineers
Pages	63-66
ISBN (Print)	978-0-7695-4345-1
DOIs	https://doi.org/10.1109/ICSTW.2011.8
Publication status	Published - 2011
Event	4th IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW 2011) - Berlin, Germany Duration: 21 Mar 2011 → 25 Mar 2011 Conference number: 4

Conference

Conference	4th IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW 2011)
Abbreviated title	ICSTW 2011
Country/Territory	Germany
City	Berlin
Period	21/03/11 → 25/03/11

Access to Document

10.1109/ICSTW.2011.8

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 (Extended abstract). In Proceedings of the 2011 IEEE Fourth International Conference on Software Testing, Verification and Validation Workshops (ICSTW 2011, Berlin, Germany, March 21-25, 2011) (pp. 63-66). Institute of Electrical and Electronics Engineers. https://doi.org/10.1109/ICSTW.2011.8

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 (Extended abstract). Proceedings of the 2011 IEEE Fourth International Conference on Software Testing, Verification and Validation Workshops (ICSTW 2011, Berlin, Germany, March 21-25, 2011). Piscataway : Institute of Electrical and Electronics Engineers, 2011. pp. 63-66

@inproceedings{d65de1bd2179423fafe25b378b832d0e,

title = "Using a DSL and fine-grained model : transformations to explore the boundaries of model verification (Extended abstract)",

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 models that are more concrete can be validated 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/ICSTW.2011.8",

language = "English",

isbn = "978-0-7695-4345-1",

pages = "63--66",

booktitle = "Proceedings of the 2011 IEEE Fourth International Conference on Software Testing, Verification and Validation Workshops (ICSTW 2011, Berlin, Germany, March 21-25, 2011)",

publisher = "Institute of Electrical and Electronics Engineers",

address = "United States",

note = "4th IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW 2011), ICSTW 2011 ; Conference date: 21-03-2011 Through 25-03-2011",

}

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 (Extended abstract). in Proceedings of the 2011 IEEE Fourth International Conference on Software Testing, Verification and Validation Workshops (ICSTW 2011, Berlin, Germany, March 21-25, 2011). Institute of Electrical and Electronics Engineers, Piscataway, pp. 63-66, 4th IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW 2011), Berlin, Germany, 21/03/11. https://doi.org/10.1109/ICSTW.2011.8

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

Proceedings of the 2011 IEEE Fourth International Conference on Software Testing, Verification and Validation Workshops (ICSTW 2011, Berlin, Germany, March 21-25, 2011). Piscataway : Institute of Electrical and Electronics Engineers, 2011. p. 63-66.

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 (Extended abstract)

AU - Amstel, van, M.F.

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

AU - Engelen, L.J.P.

N1 - Conference code: 4

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 models that are more concrete can be validated 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 models that are more concrete can be validated when fine-grained transformations are applied.

U2 - 10.1109/ICSTW.2011.8

DO - 10.1109/ICSTW.2011.8

M3 - Conference contribution

SN - 978-0-7695-4345-1

SP - 63

EP - 66

BT - Proceedings of the 2011 IEEE Fourth International Conference on Software Testing, Verification and Validation Workshops (ICSTW 2011, Berlin, Germany, March 21-25, 2011)

PB - Institute of Electrical and Electronics Engineers

CY - Piscataway

T2 - 4th IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW 2011)

Y2 - 21 March 2011 through 25 March 2011

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 (Extended abstract). In Proceedings of the 2011 IEEE Fourth International Conference on Software Testing, Verification and Validation Workshops (ICSTW 2011, Berlin, Germany, March 21-25, 2011). Piscataway: Institute of Electrical and Electronics Engineers. 2011. p. 63-66 doi: 10.1109/ICSTW.2011.8

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

Abstract

Conference

Access to Document

Fingerprint

Cite this