A Logical Approach for the Schedulability Analysis of CCSL

Yuanrui Zhang (1) , Frédéric Mallet (2, 3, 4, 5) , Huibiao Zhu (6) , Yixiang Chen (1)

1 Software Engineering Institute [Shangaï]
2 Laboratoire I3S - COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
3 I3S - Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis
4 UNS - Université Nice Sophia Antipolis (1965 - 2019)
5 KAIROS - Logical Time for Formal Embedded System Design
6 ECNU - East China Normal University [Shangaï]

The Clock Constraint Specification Language (CCSL) is a clock-based formalism for formal specification and analysis of real-time embedded systems. Previous approaches for the schedulability analysis of CCSL specifications are mainly based on model checking or SMT-checking. In this paper we propose a logical approach mainly based on theorem proving. We build a dynamic logic called 'clock-based dynamic logic' (cDL) to capture the CCSL specifications and build a proof calculus to analyze the schedule problem of the specifications. Comparing with previous approaches, our method benefits from the dynamic logic that provides a natural way of capturing the dynamic behaviour of CCSL and a divide-and-conquer way for 'decomposing' a complex formula into simple ones for an SMT-checking procedure. Based on cDL, we outline a method for the schedulability analysis of CCSL. We illustrate our theory through one example

Mots clés: Index Terms-CCSL; dynamic logic; schedulability analysis

Domaines: Systèmes embarqués

Yuanrui Zhang, Frédéric Mallet, Huibiao Zhu, Yixiang Chen. A Logical Approach for the Schedulability Analysis of CCSL. TASE 2019 - 13th International Symposium on Theoretical Aspects of Software Engineering, Jul 2019, Guilin, China. pp.25-32, ⟨10.1109/TASE.2019.00-23⟩. ⟨hal-02402976⟩