Considering Typestate Verification for Quantified Event Automata

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    179 Downloads (Pure)

    Abstract

    This paper discusses how the existing static analyses developed for
    typestate properties may be extended to a more expressive class of properties
    expressible by a specification formalism originally developed for runtime verification.
    The notion of typestate was introduced as a refinement of the notion of
    type and captures the allowed operations in certain contexts (states) as a subset
    of those operations allowed on the type. Typestates therefore represent per-object safety properties. There exist effective static analysis techniques for checking typestate properties and this has been an area of research since typestates were first introduced in 1986. It has already been observed that common properties monitored in runtime verification activities take the form of typestate properties.
    Additionally, the notion of typestate has been extended to reflect the more expressive properties seen in this area and additional static and dynamic analyses have been introduced. This paper considers a highly expressive specification language for runtime verification, quantified event automata, and discusses how these could be viewed as typestate properties and if/how the static analysis techniques could be updated accordingly. The details have not been worked out yet and are not presented, this is intended for later work.
    Original languageEnglish
    Title of host publication7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2016)
    DOIs
    Publication statusPublished - 14 Oct 2016
    Event7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2016) - Corfu, Greece
    Duration: 5 Oct 201614 Oct 2016

    Conference

    Conference7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2016)
    Country/TerritoryGreece
    CityCorfu
    Period5/10/1614/10/16

    Fingerprint

    Dive into the research topics of 'Considering Typestate Verification for Quantified Event Automata'. Together they form a unique fingerprint.

    Cite this