Book chapter 1223 views
A Specification Theory of Real-Time Processes
Chris Chilton,
Marta Kwiatkowska,
Faron Moller 
,
Xu Wang
,
Xu Wang
Concurrency, Security, and Puzzles, Volume: 10160, Pages: 18 - 38
Swansea University Author:
Faron Moller
Full text not available from this repository: check for access using links below.
DOI (Published version): 10.1007/978-3-319-51046-0_2
Abstract
This paper presents an assume-guarantee specification theory for modular synthesis and verification of real-time processes with critical timing constraints. Four operations - conjunction, disjunction, parallel and quotient - are defined over specifications, drawing inspirations from classic specific...
| Published in: | Concurrency, Security, and Puzzles |
|---|---|
| ISBN: | 9783319510453 9783319510460 |
| ISSN: | 0302-9743 1611-3349 |
| Published: |
Cham
Springer International Publishing
2016
|
| Online Access: |
Check full text
|
| URI: | https://cronfa.swan.ac.uk/Record/cronfa33932 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Abstract: |
This paper presents an assume-guarantee specification theory for modular synthesis and verification of real-time processes with critical timing constraints. Four operations - conjunction, disjunction, parallel and quotient - are defined over specifications, drawing inspirations from classic specification theories like refinement calculus. We show that a (pre-)congruence characterised by a trace-based semantics captures exactly the notion of substitutivity andrefinement between specifications. |
|---|---|
| Keywords: |
concurrency, specification, refinement |
| College: |
Faculty of Science and Engineering |
| Start Page: |
18 |
| End Page: |
38 |