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

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 new term rewriting system (TRS) on Timed Effects (TimEffs). The main purposes are to increase the expressiveness, dy- namically create clocks, and efficiently solve constraints on the clocks. We formally define a core language Ct, generalizing the real-time systems, modeled using mutable variables and timed behavioral patterns, such as delay, deadline, interrupt, etc. Secondly, to capture real-time specifications, we introduce TimEffs, a new effects logic, that extends Regular Ex- pressions with dependent values and arithmetic constraints. Thirdly, the forward verifier infers temporal behaviors of given Ct programs, expressed in TimEffs. Lastly, we present a purely algebraic TRS, i.e., an extended Antimirov algorithm, to efficiently prove language inclusions between TimEffs. To demonstrate the proposal’s feasibility, we prototype the verification system; prove its soundness; report on experimental results.