Incremental formal verification for model refining

A.J. Wijs; L.J.P. Engelen

doi:10.1145/2427376.2427382

Incremental formal verification for model refining

A.J. Wijs, L.J.P. Engelen

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

4 Citaten (Scopus)

Samenvatting

When developing complex software systems, it is vital to ensure that the final product satisfies all the stated requirements. Model checking can help to exhaustively check models of such systems, but due to its high computation demands, it is often not practical. In this paper, we present a new technique to check that properties are preserved when a model at a high level of abstraction is refined to one at a lower level through transformations. In this way, correctness of the resulting models can be determined efficiently. This technique has been implemented, and we demonstrate its usefulness in practice.

Originele taal-2	Engels
Titel	Proceedings of the 9th Workshop on Model-Driven Engineering, Verification and Validation (MoDeVVa'12), 30 September 2012, Innsbruck, Austria
Plaats van productie	New York
Uitgeverij	Association for Computing Machinery, Inc
Pagina's	29-34
ISBN van geprinte versie	978-1-4503-1801-3
DOI's	https://doi.org/10.1145/2427376.2427382
Status	Gepubliceerd - 2012

Toegang tot document

10.1145/2427376.2427382

Citeer dit

@inproceedings{5073ee5bbb7c4735a6e6c118340ed0d4,

title = "Incremental formal verification for model refining",

abstract = "When developing complex software systems, it is vital to ensure that the final product satisfies all the stated requirements. Model checking can help to exhaustively check models of such systems, but due to its high computation demands, it is often not practical. In this paper, we present a new technique to check that properties are preserved when a model at a high level of abstraction is refined to one at a lower level through transformations. In this way, correctness of the resulting models can be determined efficiently. This technique has been implemented, and we demonstrate its usefulness in practice.",

author = "A.J. Wijs and L.J.P. Engelen",

year = "2012",

doi = "10.1145/2427376.2427382",

language = "English",

isbn = "978-1-4503-1801-3",

pages = "29--34",

booktitle = "Proceedings of the 9th Workshop on Model-Driven Engineering, Verification and Validation (MoDeVVa'12), 30 September 2012, Innsbruck, Austria",

publisher = "Association for Computing Machinery, Inc",

address = "United States",

}

Incremental formal verification for model refining. / Wijs, A.J.; Engelen, L.J.P.
Proceedings of the 9th Workshop on Model-Driven Engineering, Verification and Validation (MoDeVVa'12), 30 September 2012, Innsbruck, Austria. New York: Association for Computing Machinery, Inc, 2012. blz. 29-34.

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

TY - GEN

T1 - Incremental formal verification for model refining

AU - Wijs, A.J.

AU - Engelen, L.J.P.

PY - 2012

Y1 - 2012

N2 - When developing complex software systems, it is vital to ensure that the final product satisfies all the stated requirements. Model checking can help to exhaustively check models of such systems, but due to its high computation demands, it is often not practical. In this paper, we present a new technique to check that properties are preserved when a model at a high level of abstraction is refined to one at a lower level through transformations. In this way, correctness of the resulting models can be determined efficiently. This technique has been implemented, and we demonstrate its usefulness in practice.

AB - When developing complex software systems, it is vital to ensure that the final product satisfies all the stated requirements. Model checking can help to exhaustively check models of such systems, but due to its high computation demands, it is often not practical. In this paper, we present a new technique to check that properties are preserved when a model at a high level of abstraction is refined to one at a lower level through transformations. In this way, correctness of the resulting models can be determined efficiently. This technique has been implemented, and we demonstrate its usefulness in practice.

U2 - 10.1145/2427376.2427382

DO - 10.1145/2427376.2427382

M3 - Conference contribution

SN - 978-1-4503-1801-3

SP - 29

EP - 34

BT - Proceedings of the 9th Workshop on Model-Driven Engineering, Verification and Validation (MoDeVVa'12), 30 September 2012, Innsbruck, Austria

PB - Association for Computing Machinery, Inc

CY - New York

ER -

Incremental formal verification for model refining

Samenvatting

Toegang tot document

Vingerafdruk

Citeer dit