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 Dive into the research topics of 'A proof-based method for modelling timed systems'. Together they form a unique fingerprint.

    Cite this