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 locatio...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.展开更多
1Introduction Synchronous models,a modelling paradigm proposed along with the development of synchronous programming languages[1]in,the 198os,are well-adapted for modelling and specifying reactive systemsa.type of sys...1Introduction Synchronous models,a modelling paradigm proposed along with the development of synchronous programming languages[1]in,the 198os,are well-adapted for modelling and specifying reactive systemsa.type of systems that consecutively interact with their environment at a particular environment-determined rate.In a synchronous model,system behaviours are interpreted as a sequence of reactions.展开更多
基金This work was supported by the National Natural Science Foundation of China(Grant Nos.61370100,61321064)Shanghai Knowledge Service Platform Project(ZF1213)+1 种基金Shanghai Municipal Science and Technology Commission Project(14511100400)Defense Industrial Technology Development Program JCKY(2016212B004-2).
文摘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.
基金supported by the Youth Project of National Natural Science Foundation of China(62102329)the Project of Natural Science Foundation of Chongqing(cste202jeyj-bsho204)the Capacity Development Grant of Southwest University(SWU116007)the Key Projects of National Natural Science Foundation of China(61732019,62032019)。
文摘1Introduction Synchronous models,a modelling paradigm proposed along with the development of synchronous programming languages[1]in,the 198os,are well-adapted for modelling and specifying reactive systemsa.type of systems that consecutively interact with their environment at a particular environment-determined rate.In a synchronous model,system behaviours are interpreted as a sequence of reactions.
