Skip to Main content Skip to Navigation
Journal articles

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

Abstract : 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.
Document type :
Journal articles
Complete list of metadata

https://hal.inria.fr/hal-03135428
Contributor : Frédéric Mallet Connect in order to contact the contributor
Submitted on : Monday, February 8, 2021 - 11:25:19 PM
Last modification on : Thursday, January 20, 2022 - 5:28:59 PM

Links full text

Identifiers

Collections

Citation

Yuanrui Zhang, Hengyang Wu, Yixiang Chen, Frédéric Mallet. A clock-based dynamic logic for the verification of CCSL specifications in synchronous systems. Science of Computer Programming, Elsevier, 2021, 203, pp.102591. ⟨10.1016/j.scico.2020.102591⟩. ⟨hal-03135428⟩

Share

Metrics

Les métriques sont temporairement indisponibles