Sample-Guided Automated Synthesis for CCSL Specifications

Abstract : The Clock Constraint Specification Language (CCSL) has been widely investigated in verifying causal and temporal timing behaviors of real-time embedded systems. However, due to limited expertise in formal modeling, it is difficult for requirement engineers to completely and accurately derive CCSL specifications from natural language-based design descriptions. To address this problem, we present a novel approach that facilitates automated synthesis of CCSL specifications under the guidance of sampled (expected) timing behaviors of target systems. By encoding sampled behaviors and incomplete CCSL constraints provided by requirement engineers using our proposed transformation templates, the CCSL specification synthesis problem can be naturally converted into a SKETCH synthesis problem, which enables the automated generation of CCSL specifications with high accuracy. Experiments on both well-known benchmarks and synthetic examples demonstrate the effectiveness and scalability of our approach.
Document type :
Conference papers
Complete list of metadatas

Cited literature [15 references]  Display  Hide  Download

https://hal.inria.fr/hal-02402971
Contributor : Frédéric Mallet <>
Submitted on : Monday, January 6, 2020 - 5:19:43 PM
Last modification on : Tuesday, January 7, 2020 - 9:34:38 AM

File

DAC19_authorversion.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Ming Hu, Tongquan Wei, Min Zhang, Frédéric Mallet, Mingsong Chen. Sample-Guided Automated Synthesis for CCSL Specifications. DAC 2019 - 56th Annual Design Automation Conference 2019, Jun 2019, Las Vegas, United States. pp.1-6, ⟨10.1145/3316781.3317904⟩. ⟨hal-02402971⟩

Share

Metrics

Record views

26

Files downloads

45