Book chapter 1223 views
A Specification Theory of Real-Time Processes
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 |