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 metadatas
Contributor : Team Kairos <>
Submitted on : Tuesday, September 27, 2016 - 3:25:57 PM
Last modification on : Thursday, January 21, 2021 - 10:46:03 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⟩



Record views