Divergence Detection for CCSL Specification via Clock Causality Chain - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2016

Divergence Detection for CCSL Specification via Clock Causality Chain

Résumé

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.
Fichier non déposé

Dates et versions

hal-01372694 , version 1 (27-09-2016)

Identifiants

Citer

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⟩
161 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More