Embedding CCSL into Dynamic Logic: A Logical Approach for the Verification of CCSL Specifications

Yuanrui Zhang 1 Hengyang Wu 1 Yixiang Chen 1 Frédéric Mallet 2
2 KAIROS - Logical Time for Formal Embedded System Design
CRISAM - Inria Sophia Antipolis - Méditerranée , Laboratoire I3S - COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
Abstract : The Clock Constraint Specification Language (CCSL) is a clock-based specification language for capturing causal and chronometric constraints between events in Real-Time Embedded Systems (RTESs). Due to the limitations of the existing verification approaches, CCSL lacks a full verification support for 'unsafe CCSL specifications' and a unified proof framework. In this paper, we propose a novel verification approach based on theorem proving and SMT-checking. We firstly build a logic called CCSL Dynamic Logic (CDL), which extends the traditional dynamic logic with 'signals' and 'clock relations' as primitives, and with synchronous execution mechanism for modelling RTESs. Then we propose a sound and relatively complete proof system for CDL to provide the verification support. We show how CDL can be used to capture RTES and verify CCSL specifications by analyzing a simple case study.
Document type :
Conference papers
Liste complète des métadonnées

https://hal.inria.fr/hal-01929184
Contributor : Frédéric Mallet <>
Submitted on : Wednesday, November 21, 2018 - 9:18:41 AM
Last modification on : Thursday, November 22, 2018 - 1:20:17 AM
Document(s) archivé(s) le : Friday, February 22, 2019 - 12:58:59 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01929184, version 1

Collections

Citation

Yuanrui Zhang, Hengyang Wu, Yixiang Chen, Frédéric Mallet. Embedding CCSL into Dynamic Logic: A Logical Approach for the Verification of CCSL Specifications. ICFEM / FTSCS 2018, Nov 2018, Gold Coast, Australia. ⟨hal-01929184⟩

Share

Metrics

Record views

46

Files downloads

34