A proof-based method for modelling timed systems

Alexei Iliasov, J. Bryans

    Research output: Chapter in Book/Report/Conference proceedingChapter

    3 Citations (Scopus)

    Abstract

    We present a novel method for reasoning about time in state-based proof-oriented formalisms. The method builds on a non-classical model of time, the Leibnizian model, in which time is a relative property determined by the observations of an evolving subject, rather than one of the fundamental dimensions. It proves to be remarkably effective in the context of the Event-B formalism. We illustrate the method with a machine-checked proof of Fischer’s algorithm that, to our knowledge, is simpler than other proofs available in the literature.
    Original languageEnglish
    Title of host publicationInternational Andrei Ershov Memorial Conference on Perspectives of System Informatics
    Place of PublicationBerlin
    PublisherSpringer Verlag
    Pages161-176
    Number of pages16
    Volume8974
    ISBN (Electronic)978-3-662-46823-4
    ISBN (Print)978-3-662-46822-7
    DOIs
    Publication statusE-pub ahead of print - 19 Apr 2015

    Fingerprint

    formalism

    Cite this

    Iliasov, A., & Bryans, J. (2015). A proof-based method for modelling timed systems. In International Andrei Ershov Memorial Conference on Perspectives of System Informatics (Vol. 8974, pp. 161-176). Berlin: Springer Verlag. https://doi.org/10.1007/978-3-662-46823-4_14

    A proof-based method for modelling timed systems. / Iliasov, Alexei; Bryans, J.

    International Andrei Ershov Memorial Conference on Perspectives of System Informatics. Vol. 8974 Berlin : Springer Verlag, 2015. p. 161-176.

    Research output: Chapter in Book/Report/Conference proceedingChapter

    Iliasov, A & Bryans, J 2015, A proof-based method for modelling timed systems. in International Andrei Ershov Memorial Conference on Perspectives of System Informatics. vol. 8974, Springer Verlag, Berlin, pp. 161-176. https://doi.org/10.1007/978-3-662-46823-4_14
    Iliasov A, Bryans J. A proof-based method for modelling timed systems. In International Andrei Ershov Memorial Conference on Perspectives of System Informatics. Vol. 8974. Berlin: Springer Verlag. 2015. p. 161-176 https://doi.org/10.1007/978-3-662-46823-4_14
    Iliasov, Alexei ; Bryans, J. / A proof-based method for modelling timed systems. International Andrei Ershov Memorial Conference on Perspectives of System Informatics. Vol. 8974 Berlin : Springer Verlag, 2015. pp. 161-176
    @inbook{49f59f353d0d40b1bec1ce47a4443532,
    title = "A proof-based method for modelling timed systems",
    abstract = "We present a novel method for reasoning about time in state-based proof-oriented formalisms. The method builds on a non-classical model of time, the Leibnizian model, in which time is a relative property determined by the observations of an evolving subject, rather than one of the fundamental dimensions. It proves to be remarkably effective in the context of the Event-B formalism. We illustrate the method with a machine-checked proof of Fischer’s algorithm that, to our knowledge, is simpler than other proofs available in the literature.",
    author = "Alexei Iliasov and J. Bryans",
    year = "2015",
    month = "4",
    day = "19",
    doi = "10.1007/978-3-662-46823-4_14",
    language = "English",
    isbn = "978-3-662-46822-7",
    volume = "8974",
    pages = "161--176",
    booktitle = "International Andrei Ershov Memorial Conference on Perspectives of System Informatics",
    publisher = "Springer Verlag",
    address = "Austria",

    }

    TY - CHAP

    T1 - A proof-based method for modelling timed systems

    AU - Iliasov, Alexei

    AU - Bryans, J.

    PY - 2015/4/19

    Y1 - 2015/4/19

    N2 - We present a novel method for reasoning about time in state-based proof-oriented formalisms. The method builds on a non-classical model of time, the Leibnizian model, in which time is a relative property determined by the observations of an evolving subject, rather than one of the fundamental dimensions. It proves to be remarkably effective in the context of the Event-B formalism. We illustrate the method with a machine-checked proof of Fischer’s algorithm that, to our knowledge, is simpler than other proofs available in the literature.

    AB - We present a novel method for reasoning about time in state-based proof-oriented formalisms. The method builds on a non-classical model of time, the Leibnizian model, in which time is a relative property determined by the observations of an evolving subject, rather than one of the fundamental dimensions. It proves to be remarkably effective in the context of the Event-B formalism. We illustrate the method with a machine-checked proof of Fischer’s algorithm that, to our knowledge, is simpler than other proofs available in the literature.

    U2 - 10.1007/978-3-662-46823-4_14

    DO - 10.1007/978-3-662-46823-4_14

    M3 - Chapter

    SN - 978-3-662-46822-7

    VL - 8974

    SP - 161

    EP - 176

    BT - International Andrei Ershov Memorial Conference on Perspectives of System Informatics

    PB - Springer Verlag

    CY - Berlin

    ER -