Procedure-modular specification and verification of temporal safety properties

Siavash Soleimanifard, Dilian Gurov, Marieke Huisman

    Research output: Contribution to journalArticleAcademicpeer-review

    2 Citations (Scopus)
    13 Downloads (Pure)

    Abstract

    This paper describes ProMoVer, a tool for fully automated procedure-modular verification of Java programs equipped with method-local and global assertions that specify safety properties of sequences of method invocations. Modularity at the procedure-level is a natural instantiation of the modular verification paradigm, where correctness of global properties is relativized on the local properties of the methods rather than on their implementations. Here, it is based on the construction of maximal models for a program model that abstracts away from program data. This approach allows global properties to be verified in the presence of code evolution, multiple method implementations (as arising from software product lines), or even unknown method implementations (as in mobile code for open platforms). ProMoVer automates a typical verification scenario for a previously developed tool set for compositional verification of control flow safety properties, and provides appropriate pre- and post-processing. Both linear-time temporal logic and finite automata are supported as formalisms for expressing local and global safety properties, allowing the user to choose a suitable format for the property at hand. Modularity is exploited by a mechanism for proof reuse that detects and minimizes the verification tasks resulting from changes in the code and the specifications. The verification task is relatively light-weight due to support for abstraction from private methods and automatic extraction of candidate specifications from method implementations. We evaluate the tool on a number of applications from the domains of Java Card and web-based application.
    Original languageEnglish
    Pages (from-to)83-100
    Number of pages18
    JournalSoftware and systems modeling
    Volume14
    Issue number1
    DOIs
    Publication statusPublished - Feb 2015

    Fingerprint

    Safety
    Specification
    Specifications
    Modularity
    Java
    Compositional Verification
    Temporal logic
    Finite automata
    Software Product Lines
    Processing
    Flow control
    Local Properties
    Finite Automata
    Temporal Logic
    Flow Control
    Post-processing
    Assertion
    Web-based
    Reuse
    Preprocessing

    Keywords

    • Temporal logic
    • Model checking
    • Maximal models

    Cite this

    Soleimanifard, Siavash ; Gurov, Dilian ; Huisman, Marieke. / Procedure-modular specification and verification of temporal safety properties. In: Software and systems modeling. 2015 ; Vol. 14, No. 1. pp. 83-100.
    @article{744df1b48002404fa83ee91dd00c765d,
    title = "Procedure-modular specification and verification of temporal safety properties",
    abstract = "This paper describes ProMoVer, a tool for fully automated procedure-modular verification of Java programs equipped with method-local and global assertions that specify safety properties of sequences of method invocations. Modularity at the procedure-level is a natural instantiation of the modular verification paradigm, where correctness of global properties is relativized on the local properties of the methods rather than on their implementations. Here, it is based on the construction of maximal models for a program model that abstracts away from program data. This approach allows global properties to be verified in the presence of code evolution, multiple method implementations (as arising from software product lines), or even unknown method implementations (as in mobile code for open platforms). ProMoVer automates a typical verification scenario for a previously developed tool set for compositional verification of control flow safety properties, and provides appropriate pre- and post-processing. Both linear-time temporal logic and finite automata are supported as formalisms for expressing local and global safety properties, allowing the user to choose a suitable format for the property at hand. Modularity is exploited by a mechanism for proof reuse that detects and minimizes the verification tasks resulting from changes in the code and the specifications. The verification task is relatively light-weight due to support for abstraction from private methods and automatic extraction of candidate specifications from method implementations. We evaluate the tool on a number of applications from the domains of Java Card and web-based application.",
    keywords = "Temporal logic, Model checking, Maximal models",
    author = "Siavash Soleimanifard and Dilian Gurov and Marieke Huisman",
    year = "2015",
    month = "2",
    doi = "10.1007/s10270-013-0321-0",
    language = "English",
    volume = "14",
    pages = "83--100",
    journal = "Software and systems modeling",
    issn = "1619-1366",
    publisher = "Springer",
    number = "1",

    }

    Procedure-modular specification and verification of temporal safety properties. / Soleimanifard, Siavash; Gurov, Dilian; Huisman, Marieke.

    In: Software and systems modeling, Vol. 14, No. 1, 02.2015, p. 83-100.

    Research output: Contribution to journalArticleAcademicpeer-review

    TY - JOUR

    T1 - Procedure-modular specification and verification of temporal safety properties

    AU - Soleimanifard, Siavash

    AU - Gurov, Dilian

    AU - Huisman, Marieke

    PY - 2015/2

    Y1 - 2015/2

    N2 - This paper describes ProMoVer, a tool for fully automated procedure-modular verification of Java programs equipped with method-local and global assertions that specify safety properties of sequences of method invocations. Modularity at the procedure-level is a natural instantiation of the modular verification paradigm, where correctness of global properties is relativized on the local properties of the methods rather than on their implementations. Here, it is based on the construction of maximal models for a program model that abstracts away from program data. This approach allows global properties to be verified in the presence of code evolution, multiple method implementations (as arising from software product lines), or even unknown method implementations (as in mobile code for open platforms). ProMoVer automates a typical verification scenario for a previously developed tool set for compositional verification of control flow safety properties, and provides appropriate pre- and post-processing. Both linear-time temporal logic and finite automata are supported as formalisms for expressing local and global safety properties, allowing the user to choose a suitable format for the property at hand. Modularity is exploited by a mechanism for proof reuse that detects and minimizes the verification tasks resulting from changes in the code and the specifications. The verification task is relatively light-weight due to support for abstraction from private methods and automatic extraction of candidate specifications from method implementations. We evaluate the tool on a number of applications from the domains of Java Card and web-based application.

    AB - This paper describes ProMoVer, a tool for fully automated procedure-modular verification of Java programs equipped with method-local and global assertions that specify safety properties of sequences of method invocations. Modularity at the procedure-level is a natural instantiation of the modular verification paradigm, where correctness of global properties is relativized on the local properties of the methods rather than on their implementations. Here, it is based on the construction of maximal models for a program model that abstracts away from program data. This approach allows global properties to be verified in the presence of code evolution, multiple method implementations (as arising from software product lines), or even unknown method implementations (as in mobile code for open platforms). ProMoVer automates a typical verification scenario for a previously developed tool set for compositional verification of control flow safety properties, and provides appropriate pre- and post-processing. Both linear-time temporal logic and finite automata are supported as formalisms for expressing local and global safety properties, allowing the user to choose a suitable format for the property at hand. Modularity is exploited by a mechanism for proof reuse that detects and minimizes the verification tasks resulting from changes in the code and the specifications. The verification task is relatively light-weight due to support for abstraction from private methods and automatic extraction of candidate specifications from method implementations. We evaluate the tool on a number of applications from the domains of Java Card and web-based application.

    KW - Temporal logic

    KW - Model checking

    KW - Maximal models

    U2 - 10.1007/s10270-013-0321-0

    DO - 10.1007/s10270-013-0321-0

    M3 - Article

    VL - 14

    SP - 83

    EP - 100

    JO - Software and systems modeling

    JF - Software and systems modeling

    SN - 1619-1366

    IS - 1

    ER -