Timed Contract Automata

@InProceedings{10.1007/978-3-032-22774-4_20,
author="Beckert, Bernhard
and Bremer, Andreas
and Weigl, Alexander",
editor="Albert, Elvira
and Pasareanu, Corina",
title="Timed Contract Automata",
booktitle="Fundamental Approaches to Software Engineering",
year="2026",
publisher="Springer Nature Switzerland",
address="Cham",
pages="392--411",
abstract="Real-time systems are ubiquitous today and are often employed in safety-critical environments. Therefore, formally specifying and verifying the correctness of real-time systems is crucial. We introduce Timed Contract Automata to specify the functional and timing behavior of systems that are strong enough to formalize common real-time requirements. Timed Contract Automata model possible situations using modes and specify the expected inputs, outputs, and the timing of their arrival with formulae. Timed Contract Automata combine Contract Automata, which specify the allowed stimuli and system responses using assume-guarantee contracts, with the clocks of Timed Automata to specify the expected real-time behavior. We define the syntax and the game-based semantics of Timed Contract Automata. To validate system conformance, we have implemented a method for automatic runtime monitor generation. We demonstrate the feasibility and expressive power of Timed Contract Automata and validate the generated runtime monitor through multiple implemented case studies. From these case studies, we derive specification patterns for common real-time requirements.",
isbn="978-3-032-22774-4"
}