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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Timed Contract Automata

  • Bernhard Beckert,
  • Andreas Bremer,
  • Alexander Weigl

摘要

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.