A modal specification theory for components with data

Sebastian S. Bauer, Kim Guldstrand Larsen, Axel Legay, Ulrik Mathias Nyman, Andrzej Wasowski

    Research output: Journal Article or Conference Article in JournalJournal articleResearchpeer-review

    Abstract

    Modal specification is a well-known formalism used as an abstraction theory for transition systems. Modal specifications are transition systems equipped with two types of transitions: must-transitions that are mandatory to any implementation, and may-transitions that are optional. The duality of transitions allows for developing a unique approach for both logical and structural compositions, and eases the step-wise refinement process for building implementations. We propose Modal Specifications with Data (MSDs), the first modal specification theory with explicit representation of data. Our new theory includes the most commonly seen ingredients of a specification theory; that is parallel composition, conjunction and quotient. As MSDs are by nature potentially infinite-state systems, we propose symbolic representations based on effective predicates. Our theory serves as a new abstraction-based formalism for transition systems with data.

    Original languageEnglish
    JournalScience of Computer Programming
    Volume83
    Pages (from-to)106-128
    ISSN0167-6423
    Publication statusPublished - 2014

    Keywords

    • Modal transition systems
    • Specifications
    • Interfaces
    • Data abstraction
    • Modal specifications with data

    Fingerprint

    Dive into the research topics of 'A modal specification theory for components with data'. Together they form a unique fingerprint.

    Cite this