A clock-based dynamic logic for the verification of CCSL specifications in synchronous systems

摘要

The Clock Constraint Specification Language (CCSL) is a clock-based specification language for real-time embedded systems. With logical clocks defined as first-class citizens, CCSL provides a natural way for describing clock constraints in synchronous systems - a classical model of concurrency for real-time embedded systems. In this paper, we propose a clock-based dynamic logic called CCSL Dynamic Logic (CDL) for the verification of CCSL specifications in synchronous systems. It extends the first-order dynamic logic with a synchronous execution mechanism in its program model and with CCSL primitives as terms in its logical formulae. We build a sound and relatively complete proof system for CDL to support the verification. Compared with previous approaches for verifying CCSL specifications, which are based on model checking and SMT checking techniques, our approach, which is based on theorem-proving, offers a unified verification framework in which both bounded and unbounded CCSL specifications can be verified. Technically, with the proof system of CDL, a complex CDL formula can be semi-automatically transformed into a set of quantifier-free, arithmetical first-order logic (QF-AFOL) formulae which can be checked by an SMT solver in an efficient way. As a case study, we analyze a simple synchronous system throughout the paper to illustrate how CDL works. We analyze and prove the soundness and completeness of the proof system for CDL. Currently, CDL is partially mechanized in Coq.