Abstract
In this paper, we propose a general compositional approach for modelling and verification of stochastic hybrid systems (SHSs). We extend Hybrid CSP (HCSP), a very expressive process algebra-like formal modeling language for hybrid systems, by introducing probability and stochasticity to model SHSs, which we call stochastic HCSP (SHCSP). Especially, non-deterministic choice is replaced by probabilistic choice, ordinary differential equations are replaced by stochastic differential equations (SDEs), and communication interrupts are generalized by communication interrupts with weights. We extend Hybrid Hoare Logic to specify and reason about SHCSP processes: On the one hand, we introduce the probabilistic formulas for describing probabilistic states, and on the other hand, we propose the notions of local stochastic differential invariants for characterizing SDEs and global loop invariants for repetition. Throughout the paper, we demonstrate our approach by an aircraft running example.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Altman E, Gaitsgory V (1997) Asymptotic optimization of a nonlinear hybrid system governed by a Markov decision process. SIAM J Control Optim 35(6): 2070–2085
Abate A, Prandini M, Lygeros J, Sastry S (2008) Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems. Automatica 44(11): 2724–2734
Banach R, Butler M, Qin S, Verma N, Zhu H (2015) Core hybrid event-B I: single hybrid event-B machines. Sci Comput Program 105: 92–123
Bujorianu ML, Lygeros J (2006) Toward a general theory of stochastic hybrid systems. In: Lecture notes in control and information sciences (LNCIS), vol 337, pp 3–30
Bujorianu Manuela L, Lygeros John, Bujorianu Marius C (2005) Bisimulation for general stochastic hybrid systems. In: HSCC’05, LNCS, vol 3414, pp 198–214
Bujorianu ML (2004) Extended stochastic hybrid systems and their reachability problem. In: HSCC’04, LNCS, vol 2993, pp 234–249
Chen M, Fränzle M, Li Y, Mosaad PN, Zhan N (2016) Validated simulation-based verification of delayed differential dynamics. In: FM’16, LNCS, vol 9995, pp 137–154
Castelan EB, Hennet JC (1993) On invariant polyhedra of continuous-time linear systems. IEEE Trans Autom Control 38(11): 1680–1685
Fränzle M, Hahn EM, Hermanns H, Wolovick N, Zhang L (2011) Measurability and safety verification for stochastic hybrid systems. In: HSCC’11, pp 43–52. ACM
Goubault E, Jourdan J-H, Putot S, Sankaranarayanan S (2014) Finding non-polynomial positive invariants and Lyapunov functions for polynomial systems through Darboux polynomials. In: ACC 2014, pp 3571–3578
Gretz F, Katoen J-P, McIver A (2014) Operational versus weakest pre-expectation semantics for the probabilistic guarded command language. Perform Eval 73: 110–132
Gulwani S, Tiwari A (2008) Constraint-based approach for analysis of hybrid systems. In: Gupta A, Malik S (eds) CAV’08, LNCS, vol 5123, pp 190–203. Springer, Berlin
Hartog JI (1999) Verifying probabilistic programs using a hoare like logic. In: ASIAN 1999, LNCS, vol 1742, pp 113–125
He J (1994) From CSP to hybrid systems. In: A classical mind, essays in Honour of C.A.R. Hoare. Prentice Hall International (UK) Ltd, London, pp 171–189
Henzinger TA (July 1996) The theory of hybrid automata. In: LICS’96, pp 278–292
Hahn EM, Hartmanns A, Hermanns H, Katoen J.-P. (2013) A compositional modelling and analysis framework for stochastic hybrid systems. Form Methods Syst Des 43(2): 191–232
Hahn EM, Hermanns H, Wachter B, Zhang L (2010) PASS: abstraction refinement for infinite probabilistic models. In: TACAS’10, LNCS, vol 6015, pp 353–357
Hu J, Lygeros J, Sastry S (2002) Towards a theory of stochastic hybrid systems. In: HSCC’02, LNCS, vol 1790, pp 160–173
Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM 12(10):576–580
Hoare CAR (1985) Communicating sequential processes. Prentice-Hall, Englewood Cliffs
Kwiatkowska M, Norman G, Parker D, Qu H (2010) Assume-guarantee verification for probabilistic systems. In: TACAS 2010, LNCS, vol 6015, pp 23–37
Liu J, Lv J, Quan Z, Zhan N, Zhao H, Zhou C, Zou L (2010) A calculus for hybrid CSP. In: APLAS’10, LNCS, vol 6461, pp 1–15
Liu J, Zhan N, Zhao H, Zou L (2015) Abstraction of elementary hybrid systems by variable transformation. In: FM 2015, LNCS, vol 9109. Springer International Publishing, pp 360–377
Morgan C, McIver A, Seidel K (1996) Probabilistic predicate transformers. ACM Transactions on Programming Languages and Systems, 18(3): 325–353
Morgan C, McIver A, Seidel K, Sanders JW (1996) Refinement-oriented probability for CSP. Form Asp Comput 8(6): 617–647
Meseguer J, Sharykin R (2006) Specification and analysis of distributed object-based stochastic hybrid systems. In: HSCC’06, LNCS, vol 3927, pp 460–475
Øksendal B (2007) Stochastic differential equations: an introduction with applications. Springer, Berlin
Platzer A, Clarke EM (2008) Computing differential invariants of hybrid systems as fixedpoints. In: CAV 2008, LNCS, vol 5123, pp 176–189
Prandini M, Hu J (2008) Application of reachability analysis for stochastic hybrid systems to aircraft conflict prediction. In: 47th IEEE conference on decision and control (CDC). IEEE, pp 4036 – 4041
Prajna S, Jadbabaie A, Pappas GJ (2007) A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Trans Autom Control 52(8): 1415–1428
Platzer A (2010) Differential-algebraic dynamic logic for differential-algebraic programs. J Log Comput 20(1): 309–352
Platzer A (2011) Stochastic differential dynamic logic for stochastic hybrid programs. In: CADE’11, LNCS, vol 6803, pp 446–460
Peng Y, Wang S, Zhan N, Zhang L (2015) Extending hybrid CSP with probability and stochasticity. In: SETTA’15, LNCS, vol 9409, pp 87–102
Rebiha R, Matringe N, Moura AV (2012) Transcendental inductive invariants generation for non-linear differential and hybrid systems. In: HSCC 2012, New York, NY, USA. ACM, pp 25–34
Sankaranarayanan S (2010) Automatic invariant generation for hybrid systems using ideal fixed points. In: HSCC’10, New York, NY, USA. ACM, pp 221–230
Sproston J (2000) Decidable model checking of probabilistic hybrid automata. In: Formal techniques in real-time and fault-tolerant systems, LNCS, vol 1926, pp 31–45
Sankaranarayanan S, Sipma HB, Manna Z (2004) Constructing invariants for hybrid systems. In: Alur R, Pappas GJ (eds) HSCC’04, LNCS, vol 2993, pp 539–554
Tang X, Zou X (2008) Global attractivity in a predator-prey system with pure delays. Proc Edinburgh Math Soc 51: 495–508
Wang S, Zhan N, Guelev D (2012) An assume/guarantee based compositional calculus for hybrid CSP. In: Agrawal M, Cooper SB, Li A (eds) TAMC 2012, LNCS, vol 7287. Springer, Berlin, pp 72–83
Yang Z, Lin W, Wu M (2015) Exact safety verification of hybrid systems based on bilinear SOS representation. ACM Trans Embed Comput Syst 14(1): 16–11619
Zou L, Fränzle M, Zhan N, Mosaad PN (2015) Automatic verification of stability and safety for delay differential equations. In: CAV’15, LNCS, vol 9207, pp 338–355
Zuliani P, Platzer A, Clarke EM (2013) Bayesian statistical model checking with application to stateflow/simulink verification. Form Methods Syst Des 43(2): 338–367
Zhang L, She Z, Ratschan S, Hermanns H, Hahn EM (2010) Safety verification for probabilistic hybrid systems. In: CAV’10, LNCS, vol 6174, pp 196–211
Zhou C, Wang J, Ravn AP (1996) A formal description of hybrid systems. In: Hybrid systems III, LNCS, vol 1066, pp 511–530
Zhan N, Wang S, Zhao H (2013) Formal modelling, analysis and verification of hybrid systems. In: Unifying theories of programming and formal engineering methods, LNCS, vol 8050, pp 207–281
Author information
Authors and Affiliations
Corresponding author
Additional information
Cliff Jones, Xuandong Li, and Zhiming Liu
Rights and permissions
About this article
Cite this article
Wang, S., Zhan, N. & Zhang, L. A Compositional Modelling and Verification Framework for Stochastic Hybrid Systems. Form Asp Comp 29, 751–775 (2017). https://doi.org/10.1007/s00165-017-0421-7
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-017-0421-7