Back to Search
Start Over
Sample-Guided Automated Synthesis for CCSL Specifications
- Source :
- DAC, DAC 2019-56th Annual Design Automation Conference 2019, DAC 2019-56th Annual Design Automation Conference 2019, Jun 2019, Las Vegas, United States. pp.1-6, ⟨10.1145/3316781.3317904⟩
- Publication Year :
- 2019
- Publisher :
- ACM, 2019.
-
Abstract
- International audience; 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.
- Subjects :
- Computer science
Programming language
Clock constraint specification language
020207 software engineering
Sample (statistics)
02 engineering and technology
computer.software_genre
Transformation (function)
Scalability
0202 electrical engineering, electronic engineering, information engineering
[INFO.INFO-ES]Computer Science [cs]/Embedded Systems
020201 artificial intelligence & image processing
computer
Natural language
Subjects
Details
- Database :
- OpenAIRE
- Journal :
- Proceedings of the 56th Annual Design Automation Conference 2019
- Accession number :
- edsair.doi.dedup.....54906f924c1d3e824e398415d3bc07e0