Skip to Main content Skip to Navigation
New interface
Conference papers

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 metadata

Cited literature [15 references]  Display  Hide  Download
Contributor : Frédéric Mallet Connect in order to contact the contributor
Submitted on : Monday, January 6, 2020 - 5:19:43 PM
Last modification on : Thursday, August 4, 2022 - 4:59:30 PM
Long-term archiving on: : Wednesday, April 8, 2020 - 12:27:52 AM


Files produced by the author(s)




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⟩



Record views


Files downloads