Attributes | Values |
---|
type
| |
seeAlso
| |
sameAs
| |
http://eprints.org/ontology/hasDocument
| |
http://eprints.org/ontology/hasPublished
| |
dc:hasVersion
| |
Title
| - Progress-preserving Refinements of CTA
- Progress-preserving Refinements of CTA
|
described by
| |
Date
| |
Creator
| |
status
| |
Publisher
| |
abstract
| - We develop a theory of refinement for timed asynchronous systems, in the setting of Communicating Timed Automata (CTA). Our refinement applies point-wise to the components of a system of CTA, and only affecting their time constraints—in this way, we achieve compositionality and decidability. We then establish a decidable condition under which our refinement preserves behavioural properties of systems,such as their global and local progress. Our theory provides guidelines on how to implement timed protocols using the real-time primitives of programming languages. We validate our theory through a series of experiments, supported by an open-source tool which implements our verification techniques.
- We develop a theory of refinement for timed asynchronous systems, in the setting of Communicating Timed Automata (CTA). Our refinement applies point-wise to the components of a system of CTA, and only affecting their time constraints—in this way, we achieve compositionality and decidability. We then establish a decidable condition under which our refinement preserves behavioural properties of systems,such as their global and local progress. Our theory provides guidelines on how to implement timed protocols using the real-time primitives of programming languages. We validate our theory through a series of experiments, supported by an open-source tool which implements our verification techniques.
|
Is Part Of
| |
Subject
| |
list of authors
| |
presented at
| |
is topic
of | |
is primary topic
of | |