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.
|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|
|Publication status||Published - 2012|