PSTeC: A Location-Time Driven Modelling Formalism for Probabilistic Real-Time Systems

  • Kangli He
  • Yixiang ChenEmail author
  • Min Zhang
  • Yuanrui Zhang
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9629)


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.


  1. 1.
    Bohnenkamp, H., DArgenio, P.R., Hermanns, H., Katoen, J.: Modest: a compositional modeling formalism for hard and softly timed systems. IEEE Trans. Softw. Eng. 32(10), 812–830 (2006)CrossRefGoogle Scholar
  2. 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
  3. 3.
    Chen, Y., Wu, H.: Semantics of sub-probabilistic programs. Front. Comput. Sci. China 2(1), 29–38 (2008)CrossRefGoogle Scholar
  4. 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
  5. 5.
    Dijkstra, E.W.: A Discipline of Programming, vol. 1. Prentice-Hall, Englewood Cliffs (1976)zbMATHGoogle Scholar
  6. 6.
    Hahn, E.M., Hartmanns, A., Hermanns, H., Katoen, J.: A compositional modelling and analysis framework for stochastic hybrid systems. Formal Methods Syst. Des. 43(2), 191–232 (2013)CrossRefzbMATHGoogle Scholar
  7. 7.
    Hahn, E.M., Hermanns, H., Wachter, B., Zhang, L.: INFAMY: an infinite-state markov model checker. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 641–647. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  8. 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. 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
  10. 10.
    Jifeng, H., Seidel, K., McIver, A.: Probabilistic models for the guarded command language. Sci. Comput. Program. 28(2), 171–192 (1997)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Katoen, J., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker MRMC. Perform. Eval. 68(2), 90–104 (2011)CrossRefGoogle Scholar
  12. 12.
    Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  13. 13.
    Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theor. Comput. Sci. 282(1), 101–150 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Kwiatkowska, M., Norman, G., Sproston, J., Wang, F.: Symbolic model checking for probabilistic timed automata. Inf. Comput. 205(7), 1027–1077 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Plotkin, G.D.: A structural approach to operational semantics (1981)Google Scholar
  16. 16.
    Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 481–496. Springer, Heidelberg (1994)CrossRefGoogle Scholar
  17. 17.
    Shiryaev, A.N.: Probability. Graduate Texts in Mathematics, vol. 95 (1996)Google Scholar
  18. 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
  19. 19.
    Ying, M.: Reasoning about probabilistic sequential programs in a probabilistic logic. Acta Informatica 39(5), 315–389 (2003)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  • Kangli He
    • 1
  • Yixiang Chen
    • 1
    Email author
  • Min Zhang
    • 2
  • Yuanrui Zhang
    • 1
  1. 1.MoE Engineering Research Center for Software/Hardware Co-design Technology and ApplicationEast China Normal UniversityShanghaiChina
  2. 2.Shanghai Key Laboratory of Trustworthy ComputingEast China Normal UniversityShanghaiChina

Personalised recommendations