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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

2 Citations (Scopus)

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.

Original language	English
Title of host publication	Proceedings of the 9th Workshop on Model-Driven Engineering, Verification and Validation (MoDeVVa'12), 30 September 2012, Innsbruck, Austria
Place of Publication	New York
Publisher	Association for Computing Machinery, Inc
Pages	29-34
ISBN (Print)	978-1-4503-1801-3
DOIs	https://doi.org/10.1145/2427376.2427382
Publication status	Published - 2012

Access to Document

10.1145/2427376.2427382

Fingerprint Dive into the research topics of 'Incremental formal verification for model refining'. Together they form a unique fingerprint.

Cite this

@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. p. 29-34.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › 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 -