A verification framework for spatio-temporal consistency language with CCSL as a specification language |
| |
Authors: | Yuanrui ZHANG Fr d ric MALLET Yixiang CHEN |
| |
Affiliation: | 1. MoE Engineering Research Center for Software/Hardware Co-design Technology and Application, East China Normal University, Shanghai 200062, China2. University Nice Sophia Antipolis, I3S, UMR 7271 CNRS, INRIA, 06900 Sophia Antipolis, France |
| |
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. |
| |
Keywords: | spatio-temporal consistency real-time systems spatio-temporal systems high-level modelling language clock constraint specification model checking verification framework |
本文献已被 维普 等数据库收录! |
| 点击此处可从《Frontiers of Computer Science》浏览原始摘要信息 |
|
点击此处可从《Frontiers of Computer Science》下载全文 |