DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2015 · 31 citations · 0 references
ComputingComputer ScienceComputer SystemsFormal MethodsReal-time SystemsSafety EngineeringAutomata TheoryFinite AutomataFinite-state MachinesModel CheckingReal-time Systems DesignTemporal LogicCommunication ChannelsReal-time Systems VerificationTimed AutomataTimed Automata SemanticsTimed Finite State Machines
This paper studies safety, progress, and non-zeno properties of Communicating Timed Automata (CTAs), which are timed automata (TA) extended with unbounded communication channels, and presents a procedure to build timed global specifications from systems of CTAs. We define safety and progress properties for CTAs by extending properties studied in communicating finite-state machines to the timed setting. We then study non-zenoness for CTAs; our aim is to prevent scenarios in which the participants have to execute an infinite number of actions in a finite amount of time. We propose sound and decidable conditions for these properties, and demonstrate the practicality of our approach with an implementation and experimental evaluations of our theory.