A verification framework for spatio-temporal consistency language with CCSL as a specification language

Abstract : The Spatio-Temporal Consistency Language (STeC) is a high-level modeling language that deals natively with spatio-temporal behaviour, i.e., behaviour relating to certain locations and time. Such restriction by both locations and time is of first importance for some types of real-time systems. CCSL is a formal specification language based on logical clocks. It is used to describe some crucial safety properties for real-time systems, due to its powerful expressiveness of logical and chronometric time constraints. We consider a novel verification framework combining STeC and CCSL, with the advantages of addressing spatio-temporal consistency of system behaviour and easily expressing some crucial time constraints. We propose a theory combining these two languages and a method verifying CCSL properties in STeC models. We adopt UPPAAL as the model checking tool and give a simple example to illustrate how to carry out verification in our framework.
Type de document :
Article dans une revue
Frontiers of Computer Science, Springer Verlag, 2018, 〈10.1007/s11704-018-7054-8〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01924463
Contributeur : Frédéric Mallet <>
Soumis le : vendredi 16 novembre 2018 - 06:19:55
Dernière modification le : vendredi 7 décembre 2018 - 10:54:32

Identifiants

Collections

Citation

Yuanrui Zhang, Frédéric Mallet, Yixiang Chen. A verification framework for spatio-temporal consistency language with CCSL as a specification language. Frontiers of Computer Science, Springer Verlag, 2018, 〈10.1007/s11704-018-7054-8〉. 〈hal-01924463〉

Partager

Métriques

Consultations de la notice

50