Skip to Main content Skip to Navigation
Conference papers

Divergence Detection for CCSL Specification via Clock Causality Chain

Abstract : The Clock Constraint Specification Language (CCSL), first introduced as a companion language for Modeling and Analysis of Real-Time and Embedded systems (MARTE), has now evolved beyond the time specification of MARTE, and has become a full-fledged domain specific modeling language widely used in many domains. A CCSL specification is a set of constraints, which symbolically represents a set of valid clock schedules, where a schedule represents the order of the actions in a system. This paper proposes an algorithm to detect the divergence behavior in the schedules that satisfy a given CCSL specification (i.e. it proposes to detect the presence of infinite but non periodic schedules in a CCSL specification). We investigate the divergence by constructing causality chains among the clocks resulting from the constraints of the specification. Depending on cycles in the causality chains, a bounded clock set built by our proposed algorithm can be used to decide whether the given specification is divergence-freedom or not. The approach is illustrated on one example for architecture-driven analysis.
Document type :
Conference papers
Complete list of metadata
Contributor : Team Kairos Connect in order to contact the contributor
Submitted on : Tuesday, September 27, 2016 - 3:25:57 PM
Last modification on : Friday, January 21, 2022 - 3:16:43 AM




Qingguo Xu, Julien Deantoni, Robert de Simone. Divergence Detection for CCSL Specification via Clock Causality Chain. Symposium on Dependable Software Engineering Theories, Tools and Applications, Nov 2016, Beijing, China. ⟨10.1007/978-3-319-47677-3_2⟩. ⟨hal-01372694⟩



Les métriques sont temporairement indisponibles