A compositional modelling and analysis framework for stochastic hybrid systems. (English) Zbl 1291.68293
Summary: The theory of hybrid systems is well-established as a model for real-world systems consisting of continuous behaviour and discrete control. In practice, the behaviour of such systems is also subject to uncertainties, such as measurement errors, or is controlled by randomised algorithms. These aspects can be modelled and analysed using stochastic hybrid systems. In this paper, we present HModest, an extension to the Modest modelling language – which is originally designed for stochastic timed systems without complex continuous aspects – that adds differential equations and inclusions as an expressive way to describe the continuous system evolution. Modest is a high-level language inspired by classical process algebras, thus compositional modelling is an integral feature. We define the syntax and semantics of HModest and show that it is a conservative extension of Modest that retains the compositional modelling approach. To allow the analysis of HModest models, we report on the implementation of a connection to recently developed tools for the safety verification of stochastic hybrid systems, and illustrate the language and the tool support with a set of small, but instructive case studies.
MSC:
| 68Q87 | Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) |
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
References:
| [1] | Abate A, Katoen J, Lygeros J, Prandini M (2010) Approximate model checking of stochastic hybrid systems. Eur J Control 16(6):624-641 · Zbl 1216.93091 · doi:10.3166/ejc.16.624-641 |
| [2] | 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 · Zbl 1152.93051 · doi:10.1016/j.automatica.2008.03.027 |
| [3] | 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 · Zbl 0905.90176 · doi:10.1137/S0363012995279985 |
| [4] | Alur R, Courcoubetis C, Halbwachs N, Henzinger TA, Ho PH, Nicollin X, Olivero A, Sifakis J, Yovine S (1995) The algorithmic analysis of hybrid systems. Theor Comput Sci 138:3-34 · Zbl 0874.68206 · doi:10.1016/0304-3975(94)00202-T |
| [5] | Alur R, Dang T, Esposito JM, Hur Y, Ivancic F, Kumar V, Lee I, Mishra P, Pappas GJ, Sokolsky O (2003) Hierarchical modeling and analysis of embedded systems. Proc IEEE 91(1):11-28 · doi:10.1109/JPROC.2002.805817 |
| [6] | Alur R, Dang T, Ivancic F (2006) Predicate abstraction for reachability analysis of hybrid systems. ACM Trans Embed Comput Syst 5(1):152-199 · doi:10.1145/1132357.1132363 |
| [7] | Alur R, Dill DL (1994) A theory of timed automata. Theor Comput Sci 126(2):183-235 · Zbl 0803.68071 · doi:10.1016/0304-3975(94)90010-8 |
| [8] | Baró Graf, H.; Hermanns, H.; Kulshrestha, J.; Peter, J.; Vahldiek, A.; Vasudevan, A., A verified wireless safety critical hard real-time design (2011), New York |
| [9] | van Beek DA, Man KL, Reniers MA, Rooda JE, Schiffelers RRH (2006) Syntax and consistent equation semantics of hybrid Chi. J Log Algebr Program 68(1-2):129-210 · Zbl 1088.68111 · doi:10.1016/j.jlap.2005.10.005 |
| [10] | Behrmann, G.; David, A.; Larsen, KG, A tutorial on uppaal, No. 3185, 200-236 (2004), Berlin · Zbl 1105.68350 · doi:10.1007/978-3-540-30080-9_7 |
| [11] | Berendsen, J.; Jansen, DN; Katoen, JP, Probably on time and within budget: on reachability in priced probabilistic timed automata, 311-322 (2006), Los Alamitos |
| [12] | Bernadsky, M.; Sharykin, R.; Alur, R., Structured modeling of concurrent stochastic hybrid systems, No. 3253, 309-324 (2004), Berlin · Zbl 1109.68510 · doi:10.1007/978-3-540-30206-3_22 |
| [13] | Berrang P, Bogdoll J, Hahn EM, Hartmanns A, Hermanns H (2012) Dependability results for power grids with decentralized stabilization strategies. Reports of SFB/TR 14 AVACS 83, SFB/TR 14 AVACS, ISSN: 1860-9821. www.avacs.org |
| [14] | Blom H, Lygeros J (2006) Stochastic hybrid systems: theory and safety critical applications. Lecture notes in control and information sciences, vol 337. Springer, Berlin · Zbl 1094.93003 · doi:10.1007/11587392 |
| [15] | Bogdoll, J.; David, A.; Hartmanns, A.; Hermanns, H., mctau: bridging the gap between Modest and UPPAAL, Oxford, UK, July 23-24, Berlin · doi:10.1007/978-3-642-31759-0_16 |
| [16] | Bogdoll, J.; Fioriti, LMF; Hartmanns, A.; Hermanns, H., Partial order methods for statistical model checking and simulation, No. 6722, 59-74 (2011), Berlin · doi:10.1007/978-3-642-21461-5_4 |
| [17] | Bohnenkamp HC, D’Argenio PR, Hermanns H, Katoen JP (2006) MoDeST: a compositional modeling formalism for hard and softly timed systems. IEEE Trans Softw Eng 32(10):812-830 · doi:10.1109/TSE.2006.104 |
| [18] | Bohnenkamp, HC; Gorter, J.; Guidi, J.; Katoen, JP, Are you still there?—A lightweight algorithm to monitor node presence in self-configuring networks, 704-709 (2005), Los Alamitos |
| [19] | Brinksma, E.; Krilavicius, T.; Usenko, YS, A process-algebraic approach to hybrid systems (2005), Laxenburg |
| [20] | Bujorianu, ML, Extended stochastic hybrid systems and their reachability problem, No. 2993, 234-249 (2004), Berlin · Zbl 1135.93373 · doi:10.1007/978-3-540-24743-2_16 |
| [21] | Bujorianu, ML; Lygeros, J.; Bujorianu, MC, Bisimulation for general stochastic hybrid systems, No. 3414, 198-214 (2005), Berlin · Zbl 1078.93062 · doi:10.1007/978-3-540-31954-2_13 |
| [22] | Clarke, E.; Fehnker, A.; Han, Z.; Krogh, B.; Stursberg, O.; Theobald, M., Verification of hybrid systems based on counterexample-guided abstraction refinement, No. 2619, 192-207 (2003), Berlin · Zbl 1031.68078 · doi:10.1007/3-540-36577-X_14 |
| [23] | Cuijpers PJL, Reniers MA (2005) Hybrid process algebra. J Log Algebr Program 62(2):191-245 · Zbl 1090.68071 · doi:10.1016/j.jlap.2004.02.001 |
| [24] | Dang, T.; Maler, O., Reachability analysis via face lifting, No. 1386, 96-109 (1998), Berlin · doi:10.1007/3-540-64358-3_34 |
| [25] | D’Argenio, PR; Wolovick, N.; Terraf, PS; Celayes, P., Nondeterministic labeled Markov processes: bisimulations and logical characterization, 11-20 (2009), Los Alamitos |
| [26] | Davis MHA (1993) Markov models and optimization. Chapman & Hall, London · Zbl 0780.60002 |
| [27] | Desharnais J, Edalat A, Panangaden P (2002) Bisimulation for labelled Markov processes. Inf Comput 179(2):163-193 · Zbl 1096.68103 · doi:10.1006/inco.2001.2962 |
| [28] | Edwards S, Lavagno L, Lee EA, Sangiovanni-Vincentelli A (1997) Design of embedded systems: formal models, validation, and synthesis. Proc IEEE 85(3):366-390 · doi:10.1109/5.558710 |
| [29] | Fränzle, M.; Hahn, EM; Hermanns, H.; Wolovick, N.; Zhang, L., Measurability and safety verification for stochastic hybrid systems, 43-52 (2011), New York · Zbl 1362.68170 |
| [30] | Fränzle M, Herde C, Teige T, Ratschan S, Schubert T (2007) Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. J. Satisf. Boolean Model. Comput. 1(3-4):209-236 · Zbl 1144.68371 |
| [31] | Frehse G (2008) Phaver: algorithmic verification of hybrid systems past HyTech. Int J Softw Tools Technol Transf 10(3):263-279 · doi:10.1007/s10009-007-0062-x |
| [32] | Frehse, G.; Guernic, CL; Donzé, A.; Cotton, S.; Ray, R.; Lebeltel, O.; Ripado, R.; Girard, A.; Dang, T.; Maler, O., Spaceex: scalable verification of hybrid systems, No. 6806, 379-395 (2011), Berlin · doi:10.1007/978-3-642-22110-1_30 |
| [33] | Giry, M., A categorical approach to probability theory, 68-85 (1982), Berlin · Zbl 0486.60034 · doi:10.1007/BFb0092872 |
| [34] | Groß, C.; Hermanns, H.; Pulungan, R., Does clock precision influence Zigbee’s energy consumptions?, No. 4878, 174-188 (2007), Berlin · doi:10.1007/978-3-540-77096-1_13 |
| [35] | Grosu R, Stauner T (2002) Modular and visual specification of hybrid systems: an introduction to HyCharts. Form Methods Syst Des 21(1):5-38 · Zbl 1018.68047 · doi:10.1023/A:1016001318739 |
| [36] | Hartmanns, A., Model-checking and simulation for stochastic timed systems, No. 6957, 372-391 (2010), Berlin |
| [37] | Hartmanns, A.; Hermanns, H., A Modest approach to checking probabilistic timed automata, 187-196 (2009), Los Alamitos |
| [38] | Henzinger, TA, The theory of hybrid automata, 278-292 (1996) |
| [39] | Henzinger TA, Ho PH, Wong-Toi H (1997) HYTECH: a model checker for hybrid systems. Int J Softw Tools Technol Transf 1(1-2):110-122 · Zbl 1060.68603 · doi:10.1007/s100090050008 |
| [40] | Herde, C.; Eggers, A.; Fränzle, M.; Teige, T., Analysis of hybrid systems using HySAT, 196-201 (2008), Los Alamitos · doi:10.1109/ICONS.2008.17 |
| [41] | Hermanns H, Herzog U, Katoen JP (2002) Process algebra for performance evaluation. Theor Comput Sci 274(1-2):43-87 · Zbl 0992.68149 · doi:10.1016/S0304-3975(00)00305-4 |
| [42] | Hillston J (1994) A compositional approach to performance modelling. PhD thesis, Univ of Edinburgh · Zbl 1080.68003 |
| [43] | Hu, J.; Lygeros, J.; Sastry, S., Towards a theory of stochastic hybrid systems, No. 1790, 160-173 (2000), Berlin · Zbl 0962.93082 · doi:10.1007/3-540-46430-1_16 |
| [44] | Kwiatkowska, M.; Norman, G.; Parker, D., PRISM 4.0: verification of probabilistic real-time systems, No. 6806, 585-591 (2011), Berlin · doi:10.1007/978-3-642-22110-1_47 |
| [45] | Kwiatkowska, M.; Norman, G.; Segala, R.; Sproston, J., Verifying quantitative properties of continuous probabilistic timed automata, No. 1877, 123-137 (2000), Berlin · Zbl 0999.68125 |
| [46] | Kwiatkowska MZ, Norman G, Segala R, Sproston J (2002) Automatic verification of real-time systems with discrete probability distributions. Theor Comput Sci 282(1):101-150 · Zbl 1050.68094 · doi:10.1016/S0304-3975(01)00046-9 |
| [47] | Lee, EA; Zelkowitz, M. (ed.), Embedded software, No. 56 (2002), San Diego |
| [48] | Legay, A.; Delahaye, B.; Bensalem, S., Statistical model checking: an overview, No. 6418, 122-135 (2010), Berlin · doi:10.1007/978-3-642-16612-9_11 |
| [49] | Lynch NA, Segala R, Vaandrager FW (2003) Hybrid i/o automata. Inf Comput 185(1):105-157 · Zbl 1069.68067 · doi:10.1016/S0890-5401(03)00067-1 |
| [50] | Mader A, Bohnenkamp HC, Usenko YS, Jansen DN, Hurink J, Hermanns H (2010) Synthesis and stochastic assessment of cost-optimal schedules. Int J Softw Tools Technol Transf 12(5):305-318 · doi:10.1007/s10009-009-0129-y |
| [51] | Meseguer, J.; Sharykin, R., Specification and analysis of distributed object-based stochastic hybrid systems, No. 3927, 460-475 (2006), Berlin · Zbl 1178.68350 · doi:10.1007/11730637_35 |
| [52] | Panangaden P (2008) Labelled Markov processes. World Scientific, Singapore |
| [53] | Penna GD, Intrigila B, Melatti I, Tronci E, Zilli MV (2006) Finite horizon analysis of Markov chains with the Murphy verifier. Int J Softw Tools Technol Transf 8(4-5):397-409 · doi:10.1007/s10009-005-0216-7 |
| [54] | Platzer, A.; Bjørner, N. (ed.); Sofronie-Stokkermans, V. (ed.), Stochastic differential dynamic logic for stochastic hybrid programs, No. 6803, 446-460 (2011), Berlin · Zbl 1341.68030 |
| [55] | Preußig, J.; Kowalewski, S.; Wong-Toi, H.; Henzinger, T., An algorithm for the approximative analysis of rectangular automata, No. 1486, 228-240 (1998), Berlin · doi:10.1007/BFb0055350 |
| [56] | Ratschan S, She Z (2007) Safety verification of hybrid systems by constraint propagation-based abstraction refinement. ACM Trans Embed Comput Syst 6(1):8 · Zbl 1078.93508 · doi:10.1145/1210268.1210276 |
| [57] | Segala R (1995) Modelling and verification of randomized distributed real-time systems. PhD thesis, MIT, Cambridge, MA, USA · Zbl 0803.68071 |
| [58] | Segala R, Lynch NA (1995) Probabilistic simulations for probabilistic processes. Nord J Comput 2(2):250-273 · Zbl 0839.68067 |
| [59] | Sproston, J., Decidable model checking of probabilistic hybrid automata, No. 1926, 31-45 (2000), Berlin · Zbl 0986.68058 · doi:10.1007/3-540-45352-0_5 |
| [60] | Strubbe, S.; Schaft, A.; Cassandras, CG (ed.); Lygeros, J. (ed.), Compositional modelling of stochastic hybrid systems, 47-77 (2006), London · doi:10.1201/9781420008548.ch3 |
| [61] | Wolovick N (2012) Continuous probability and nondeterminism in labeled transition systems. PhD thesis, FaMAF, UNC, Córdoba, Argentina |
| [62] | Yue, H.; Bohnenkamp, HC; Kampschulte, M.; Katoen, JP, Analysing and improving energy efficiency of distributed slotted aloha, No. 6869, 197-208 (2011), Berlin · doi:10.1007/978-3-642-22875-9_18 |
| [63] | Zhang, L.; She, Z.; Ratschan, S.; Hermanns, H.; Hahn, E., Safety verification for probabilistic hybrid systems, No. 6174, 196-211 (2010), Berlin · doi:10.1007/978-3-642-14295-6_21 |
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
