Oxford logo
[CKMW17] C. Chilton, M. Kwiatkowska, F. Moller and X. Wang. A Specification Theory of Real-Time Processes. In Concurrency, Security, and Puzzles - Essays Dedicated to Andrew William Roscoe on the Occasion of His 60th Birthday, volume 10160 of Lecture Notes in Computer Science, pages 18-38, Springer. 2017. [pdf] [bib]
Downloads:  pdf pdf (483 KB)  bib bib
Notes: The original publication is available at link.springer.com.
Abstract. This paper presents an assume-guarantee specification theory (aka interface theory from [11]) for modular synthesis and verification of real-time processes with critical timing constraints. Four operations, i.e. conjunction, disjunction, parallel and quotient, are defined over specifications, drawing inspirations from classic specification theories like refinement calculus [4,19]. We show that a congruence (or pre-congruence) characterised by a trace-based semantics [14] captures exactly the notion of substitutivity (or refinement) between specifications.