A conformance testing relation for symbolic timed automata

S. Styp, von, H.C. Bohnenkamp, J. Schmaltz

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

    11 Citations (Scopus)

    Abstract

    We introduce Symbolic Timed Automata, an amalgamation of symbolic transition systems and timed automata, which allows to express nondeterministic data-dependent control flow with inputs and outputs and real-time behaviour. In particular, input data can influence the timing behaviour. We define two semantics for STA, a concrete one as timed labelled transition systems and another one on a symbolic level. We show that the symbolic semantics is complete and correct w.r.t. the concrete one. Finally, we introduce symbolic conformance relation stioco , which is an extension of the well-known ioco conformance relation. Relation stioco is defined using FO-logic on a purely symbolic level. We show that stioco corresponds on the concrete semantic level to Krichen and Tripakis’ implementation relation tioco for timed labelled transition systems.
    Original languageEnglish
    Title of host publicationFormal Modeling and Analysis of Timed Systems (8th International Conference, FORMATS 2010, Klosterneuburg, Austria, September 8-10, 2010. Proceedings)
    EditorsK. Chatterjee, T.A. Henzinger
    Place of PublicationBerlin
    PublisherSpringer
    Pages243-255
    ISBN (Print)978-3-642-15296-2
    DOIs
    Publication statusPublished - 2010

    Publication series

    NameLecture Notes in Computer Science
    Volume6246
    ISSN (Print)0302-9743

    Fingerprint

    Dive into the research topics of 'A conformance testing relation for symbolic timed automata'. Together they form a unique fingerprint.

    Cite this