Modeling and Verifying Uncertainty-Aware Timing Behaviors using Parametric Logical Time Constraint - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2020

Modeling and Verifying Uncertainty-Aware Timing Behaviors using Parametric Logical Time Constraint

Résumé

The Clock Constraint Specification Language (CCSL) is a logical time based modeling language to formalize timing behaviors of real-time and embedded systems. However, it cannot capture timing behaviors that contain uncertainties, e.g., uncertainty in execution time and period. This limits the application of the language to real-world systems, as uncertainty often exists in practice due to both internal and external factors. To capture uncertainties in timing behaviors, in this paper we extend CCSL by introducing parameters into constraints. We then propose an approach to transform parametric CCSL constraints into SMT formulas for efficient verification. We apply our approach to an industrial case which is proposed as the FMTV (Formal Methods for Timing Verification) Challenge in 2015, which shows that timing behaviors with uncertainties can be effectively modeled and verified using the parametric CCSL.
Fichier principal
Vignette du fichier
main.pdf (890.58 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02429533 , version 1 (06-01-2020)

Identifiants

  • HAL Id : hal-02429533 , version 1

Citer

Fei Gao, Frédéric Mallet, Min Zhang, Mingsong Chen. Modeling and Verifying Uncertainty-Aware Timing Behaviors using Parametric Logical Time Constraint. DATE 2020 - Design, Automation and Test in Europe Conference, Mar 2020, Grenoble, France. ⟨hal-02429533⟩
152 Consultations
201 Téléchargements

Partager

Gmail Facebook X LinkedIn More