Timed I/O Automata: It is never too late to complete your timed specification theory
Formal Languages and Automata Theory
2023-07-14 v2 Software Engineering
Abstract
A specification theory combines notions of specifications and implementations with a satisfaction relation, a refinement relation and a set of operators supporting stepwise design. We develop a complete specification framework for real-time systems using Timed I/O Automata as the specification formalism, with the semantics expressed in terms of Timed I/O Transition Systems. We provide constructs for refinement, consistency checking, logical and structural composition, and quotient of specifications -- all indispensable ingredients of a compositional design methodology. The theory is backed by rigorous proofs and is being implemented in the open-source tool ECDAR.
Keywords
Cite
@article{arxiv.2302.04529,
title = {Timed I/O Automata: It is never too late to complete your timed specification theory},
author = {Martijn A. Goorden and Kim G. Larsen and Axel Legay and Florian Lorber and Ulrik Nyman and Andrzej Wasowski},
journal= {arXiv preprint arXiv:2302.04529},
year = {2023}
}
Comments
Version submitted for review