PSTeC: A Location-Time Driven Modelling Formalism for Probabilistic Real-Time Systems
Internet of Things (IoT) and Cyber-Physical Systems (CPS) have become important topics in both theory and industry. In some application domains, such as when specifying the behaviour of precision mechanics, we need to include features of spatial-temporal consistency. How to model probabilistic real-time systems in such domains is a challenge. This paper presents a modelling formalism, called PSTeC, for describing the behaviour of probabilistic real-time systems focusing on spatial-temporal consistency with nondeterministic, probabilistic and real-time aspects. The consistency restricts a process to start and finish at the required location and time. Communications between agents is specified by interactive actions. The language we propose is an extension of STeC, which is a specification language for location-aware real-time systems, adding probabilistic operations so as to support the incorporation of probabilistic aspects. We first give a formal definition of the syntax for PSTeC, then focus on the details of its operational semantics, which maps a PSTeC term onto a Probabilistic Spatial-Temporal Transition System (PSTTS) following the structured operational semantics style. A simple example demonstrates the expressiveness of PSTeC.
This work is supported by the National Basic Research Program of China (Grant No. 2011CB302802), the Innovation Group Project of the National Natural Science Foundation (Grant No. 61321064), the National Natural Science Foundation of China (Grant No. 61370100), the NSFC projects (Grant No. 61361136002 and No. 61202105) and Shanghai Knowledge Service Platform for Trustworthy Internet of Things (Grant No. ZF1213). Part of this work was done while the first author was visiting Saarland University, Germany. The authors thank Holger Hermanns (Saarland University, Germany) for his valuable contributions and discussions and helpful comments on the structure and contents of this paper. The authors would also like to thank the anonymous referees for their invaluable comments and suggestions.
- 2.Chen, Y.: STeC: a location-triggered specification language for real-timesystems. In: 2012 15th IEEE International Symposium on Object/Component/Service-Oriented Real-Time DistributedComputing Workshops (ISORCW), pp.1–6. IEEE (2012)Google Scholar
- 4.Chen, Y., Zhang, Y.: A hybrid clock system related to STeC language. In: 2014 IEEE EighthInternational Conference on Software Security and Reliability-Companion (SERE-C), pp. 199–203. IEEE (2014)Google Scholar
- 8.He, K., Zhang, M., He, J., Chen, Y.: Probabilistic model checking of pipe protocol. In: 2015 International Symposium on Theoretical Aspects of Software Engineering (TASE), pp. 135–138. IEEE (2015)Google Scholar
- 9.Hermanns, H., Katoen, J.P., Meyer-Kayser, J., Siegle, M.: ETMCC: model checking performability properties of markov chains. In: Null, p. 673. IEEE (2003)Google Scholar
- 15.Plotkin, G.D.: A structural approach to operational semantics (1981)Google Scholar
- 17.Shiryaev, A.N.: Probability. Graduate Texts in Mathematics, vol. 95 (1996)Google Scholar
- 18.Wu, H., Chen, Y., Zhang, M.: On denotational semantics of spatial-temporal consistency language-stec. In: 2013 International Symposium on Theoretical Aspects of Software Engineering (TASE), pp. 113–120. IEEE (2013)Google Scholar