A proof-based method for modelling timed systems

Alexei Iliasov; J. Bryans

doi:10.1007/978-3-662-46823-4_14

A proof-based method for modelling timed systems

Alexei Iliasov
, J. Bryans

Newcastle University

Research output: Chapter in Book/Report/Conference proceeding › Chapter › peer-review

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 language	English
Title of host publication	International Andrei Ershov Memorial Conference on Perspectives of System Informatics
Place of Publication	Berlin
Publisher	Springer Verlag
Pages	161-176
Number of pages	16
Volume	8974
ISBN (Electronic)	978-3-662-46823-4
ISBN (Print)	978-3-662-46822-7
DOIs	https://doi.org/10.1007/978-3-662-46823-4_14
Publication status	E-pub ahead of print - 19 Apr 2015

Access to Document

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

Jeremy Bryans
- Centre for Future Transport and Cities - Assistant Professor Research
Person: Teaching and Research

Cite this

@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{\textquoteright}s algorithm that, to our knowledge, is simpler than other proofs available in the literature.",

author = "Alexei Iliasov and J. Bryans",

year = "2015",

month = apr,

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 -

A proof-based method for modelling timed systems

Abstract

Access to Document

Fingerprint

Profiles

Jeremy Bryans

Cite this