Automated temporal verification with extended regular expressions
COM1 Level 2
SR3, COM1-02-12
Abstract:
Existing temporal verification approaches have sacrificed modularity in favor of achieving automation or vice-versa. To exploit the best of both worlds, this thesis presents a new framework to ensure temporal properties via Hoare-style verifiers and term rewriting systems (TRSs). The leading technique of temporal verification is automata-based model checking, which has current inadequacies: (i) it requires a manual modeling stage and needs to be bounded when encountering non-terminating traces; (ii) to conveniently deploy existing inclusion-checkers for automata, the expressiveness power is limited by the finite-state automata; and (iii) there is always a gap between the verified logic and the actual implementation of the program. To tackle these issues, this thesis proposes a framework that conducts local temporal verification, leading to a modular and compositional verification strategy, where modules can be replaced by their already verified properties. In our exploration, we proposed various effect logics to be the temporal specifications, which are extended regular expressions (REs) and more flexible/expressive than the most deployed linear temporal logic (LTL). Furthermore, the proposed framework devises purely algebraic TRS to check the inclusions for the novel logics, avoiding the complex translation into automata. This thesis demonstrates the applicability of the proposed framework and various REs-based temporal logics in different domains, such as synchronous programming, real-time systems, algebraic effects, etc. This thesis also presents the corresponding prototype systems, case studies, experimental results, and supporting proofs.