[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]
|
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.
|