×

zbMATH — the first resource for mathematics

A compositional modelling and verification framework for stochastic hybrid systems. (English) Zbl 1370.68220
Summary: 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.
MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)
93C30 Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems)
93C83 Control/observation systems involving computers (process control, etc.)
Software:
PASS
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Altman, E; Gaitsgory, V, Asymptotic optimization of a nonlinear hybrid system governed by a Markov decision process, SIAM J Control Optim, 35, 2070-2085, (1997) · Zbl 0905.90176
[2] Abate, A; Prandini, M; Lygeros, J; Sastry, S, Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems, Automatica, 44, 2724-2734, (2008) · Zbl 1152.93051
[3] Banach, R; Butler, M; Qin, S; Verma, N; Zhu, H, Core hybrid event-B I: single hybrid event-B machines, Sci Comput Program, 105, 92-123, (2015)
[4] 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 · Zbl 1130.93048
[5] Bujorianu Manuela L, Lygeros John, Bujorianu Marius C (2005) Bisimulation for general stochastic hybrid systems. In: HSCC’05, LNCS, vol 3414, pp 198-214 · Zbl 1078.93062
[6] Bujorianu ML (2004) Extended stochastic hybrid systems and their reachability problem. In: HSCC’04, LNCS, vol 2993, pp 234-249 · Zbl 1135.93373
[7] 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 · Zbl 1291.68293
[8] Castelan, EB; Hennet, JC, On invariant polyhedra of continuous-time linear systems, IEEE Trans Autom Control, 38, 1680-1685, (1993) · Zbl 0790.93099
[9] 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 · Zbl 1362.68170
[10] 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
[11] Gretz, F; Katoen, J-P; McIver, A, Operational versus weakest pre-expectation semantics for the probabilistic guarded command language, Perform Eval, 73, 110-132, (2014)
[12] 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 · Zbl 1155.68437
[13] Hartog JI (1999) Verifying probabilistic programs using a hoare like logic. In: ASIAN 1999, LNCS, vol 1742, pp 113-125 · Zbl 0959.68076
[14] 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 · Zbl 0905.90176
[15] Henzinger TA (July 1996) The theory of hybrid automata. In: LICS’96, pp 278-292
[16] Hahn, EM; Hartmanns, A; Hermanns, H; Katoen, J.-P., A compositional modelling and analysis framework for stochastic hybrid systems, Form Methods Syst Des, 43, 191-232, (2013) · Zbl 1291.68293
[17] 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
[18] Hu J, Lygeros J, Sastry S (2002) Towards a theory of stochastic hybrid systems. In: HSCC’02, LNCS, vol 1790, pp 160-173 · Zbl 0962.93082
[19] Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM 12(10):576-580 · Zbl 0179.23105
[20] Hoare CAR (1985) Communicating sequential processes. Prentice-Hall, Englewood Cliffs · Zbl 0637.68007
[21] Kwiatkowska M, Norman G, Parker D, Qu H (2010) Assume-guarantee verification for probabilistic systems. In: TACAS 2010, LNCS, vol 6015, pp 23-37 · Zbl 1284.68406
[22] 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 · Zbl 1152.93051
[23] 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 · Zbl 0905.90176
[24] Morgan, C; McIver, A; Seidel, K, Probabilistic predicate transformers, ACM Transactions on Programming Languages and Systems,, 18, 325-353, (1996)
[25] Morgan, C; McIver, A; Seidel, K; Sanders, JW, Refinement-oriented probability for CSP, Form Asp Comput, 8, 617-647, (1996) · Zbl 0862.68050
[26] Meseguer J, Sharykin R (2006) Specification and analysis of distributed object-based stochastic hybrid systems. In: HSCC’06, LNCS, vol 3927, pp 460-475 · Zbl 1178.68350
[27] Øksendal B (2007) Stochastic differential equations: an introduction with applications. Springer, Berlin · Zbl 0567.60055
[28] Platzer A, Clarke EM (2008) Computing differential invariants of hybrid systems as fixedpoints. In: CAV 2008, LNCS, vol 5123, pp 176-189 · Zbl 1155.68445
[29] 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
[30] Prajna, S; Jadbabaie, A; Pappas, GJ, A framework for worst-case and stochastic safety verification using barrier certificates, IEEE Trans Autom Control, 52, 1415-1428, (2007) · Zbl 1366.93711
[31] Platzer, A, Differential-algebraic dynamic logic for differential-algebraic programs, J Log Comput, 20, 309-352, (2010) · Zbl 1191.03024
[32] Platzer A (2011) Stochastic differential dynamic logic for stochastic hybrid programs. In: CADE’11, LNCS, vol 6803, pp 446-460 · Zbl 1341.68030
[33] 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 · Zbl 1369.68264
[34] 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 · Zbl 1362.68153
[35] Sankaranarayanan S (2010) Automatic invariant generation for hybrid systems using ideal fixed points. In: HSCC’10, New York, NY, USA. ACM, pp 221-230 · Zbl 1360.34082
[36] 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 · Zbl 0986.68058
[37] 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 · Zbl 1135.93322
[38] Tang, X; Zou, X, Global attractivity in a predator-prey system with pure delays, Proc Edinburgh Math Soc, 51, 495-508, (2008) · Zbl 1155.34040
[39] 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 · Zbl 1354.68204
[40] Yang, Z; Lin, W; Wu, M, Exact safety verification of hybrid systems based on bilinear SOS representation, ACM Trans Embed Comput Syst, 14, 16-11619, (2015)
[41] 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 · Zbl 1381.68188
[42] Zuliani, P; Platzer, A; Clarke, EM, Bayesian statistical model checking with application to stateflow/simulink verification, Form Methods Syst Des, 43, 338-367, (2013) · Zbl 1291.68273
[43] 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 · Zbl 1291.93294
[44] Zhou C, Wang J, Ravn AP (1996) A formal description of hybrid systems. In: Hybrid systems III, LNCS, vol 1066, pp 511-530
[45] 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 · Zbl 1444.68105
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.