Revisiting timed specification theories: a linear-time perspective

DOI10.1007/978-3-642-33365-1_7MaRDI QIDQ4649387zbMATH OpenOpenAlexFDO

Authors Chris Chilton, Marta Kwiatkowska, Xu Wang

Publication date 21 November 2012

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1206.4504

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: We consider the setting of component-based design for real-time systems with critical timing constraints. Based on our earlier work, we propose a compositional specification theory for timed automata with I/O distinction, which supports substitutive refinement. Our theory provides the operations of parallel composition for composing components at run-time, logical conjunction/disjunction for independent development, and quotient for incremental synthesis. The key novelty of our timed theory lies in a weakest congruence preserving safety as well as bounded liveness properties. We show that the congruence can be characterised by two linear-time semantics, timed-traces and timed-strategies, the latter of which is derived from a game-based interpretation of timed interaction.

Recommendations

• Timed I/O automata: a complete specification theory for real-time systems
• Refinement and Consistency of Timed Modal Specifications
• A specification theory of real-time processes
• Robust specification of real time components
• A compositional specification theory for component behaviours

Cited in

(12)

• Modal event-clock specifications for timed component-based design
• New results on timed specifications
• A compositional specification theory for component behaviours
• A Linear-Time–Branching-Time Spectrum of Behavioral Specification Theories
• Timed I/O automata: a complete specification theory for real-time systems
• The earlier the better: a theory of timed actor interfaces
• Methodologies for specification of real-time systems using timed I/O automata
• Robust specification of real time components
• An alternative definition for timed automata composition
• An algebraic theory of interface automata
• scientific article; zbMATH DE number 2017345 (Why is no real title available?)
• Progress-preserving refinements of CTA

Describes a project that uses

Uses Software

• ECDAR

This page was built for publication: Revisiting timed specification theories: a linear-time perspective

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4649387)