Incremental formal verification for model refining

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

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-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 languageEnglish
    Title of host publicationProceedings of the 9th Workshop on Model-Driven Engineering, Verification and Validation (MoDeVVa'12), 30 September 2012, Innsbruck, Austria
    Place of PublicationNew York
    PublisherAssociation for Computing Machinery, Inc
    Pages29-34
    ISBN (Print)978-1-4503-1801-3
    DOIs
    Publication statusPublished - 2012

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

    Cite this