Timed I/O Automata: It is never too late to complete your timed specification theory

2023/02/09 by Goorden, Martijn A., Larsen, Kim G., Legay, Axel +3 · 1 citation
#FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Software Engineering (cs.SE)

paper · doi:10.48550/arxiv.2302.04529

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.

Cited by

• Compositional Abstraction for Timed Systems with Broadcast Synchronization

Related

• Revisiting Timed Specification Theories: A Linear-Time Perspective
• Time Window Temporal Logic
• ATAC: A Tool for Automating Timed Automata Construction
• Timed Automata Benchmark Description
• Towards Focus on Time