Formal Dependability Engineering with MIOA

    Research output: Book/ReportReportProfessional

    27 Downloads (Pure)

    Abstract

    In this paper, we introduce MIOA, a stochastic process algebra-like specification language with datatypes, as well as a logic intSPDL, and its model checking algorithms. MIOA, which stands for Markovian input/output automata language, is an extension of Lynch's input/automata with Markovian timed transitions.MIOA can serve both as a fully fledged ``stand-alone'' specification language and the semantic model for the architectural dependability modelling and evaluation language Arcade. The logic intSPDL is an extension of the stochastic logic SPDL, to deal with the specialties of MIOA. intSPDL in the context of Arcade can be seen as the semantic model of abstract and complex dependability measures that can be defined in the Arcade framework. We define syntax and semantics of both MIOA and intSPDL, and show examples of applying MIOA and intSPDL in the realm of dependability modelling with Arcade.
    Original languageUndefined
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    Number of pages25
    Publication statusPublished - 4 Jun 2008

    Publication series

    NameCTIT Technical Report Series
    PublisherCentre for Telematics and Information Technology, University of Twente
    No.274/TR-CTIT-08-39
    ISSN (Print)1381-3625

    Keywords

    • METIS-250986
    • EWI-12786
    • IR-64777

    Cite this

    Kuntz, G. W. M., & Haverkort, B. R. H. M. (2008). Formal Dependability Engineering with MIOA. (CTIT Technical Report Series; No. 274/TR-CTIT-08-39). Enschede: Centre for Telematics and Information Technology (CTIT).