Automated Verification for Real-Time Systems - via Implicit Clocks and an Extended Antimirov Algorithm

Abstract

Abstract The correctness of real-time systems depends both on the correct functionalities and the realtime constraints. To go beyond the existing Timed Automata based techniques, we propose a novel solution that integrates a modular Hoare-style forward verifier with a term rewriting system (TRS) on Timed Effects ( TimEffs ). The main purposes are to: increase the expressiveness, dynamically manipulate clocks, and efficiently solve clock constraints. We formally define a core language $$ C^{t} $$ C t , generalizing the real-time systems, modeled using mutable variables and timed behavioral patterns, such as delay , timeout , interrupt , deadline . Secondly, to capture real-time specifications, we introduce TimEffs , a new effects logic, that extends regular expressions with dependent values and arithmetic constraints. Thirdly, the forward verifier reasons temporal behaviors – expressed in TimEffs – of target $$ C^{t} $$ C t programs. Lastly, we present a purely algebraic TRS, i.e., an extended Antimirov algorithm , to efficiently check language inclusions between TimEffs . To demonstrate the feasibility of our proposal, we prototype the verification system; prove its soundness; report on case studies and experimental results.