×

Statistical model checking for networks of priced timed automata. (English) Zbl 1348.68130

Fahrenberg, Uli (ed.) et al., Formal modeling and analysis of timed systems. 9th international conference, FORMATS 2011, Aalborg, Denmark, September 21–23, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-24309-7/pbk). Lecture Notes in Computer Science 6919, 80-96 (2011).
Summary: This paper offers a natural stochastic semantics of Networks of Priced Timed Automata (NPTA) based on races between components. The semantics provides the basis for satisfaction of Probabilistic Weighted CTL properties (PWCTL), conservatively extending the classical satisfaction of timed automata with respect to TCTL. In particular the extension allows for hard real-time properties of timed automata expressible in TCTL to be refined by performance properties, e.g. in terms of probabilistic guarantees of time- and cost-bounded properties. A second contribution of the paper is the application of Statistical Model Checking (SMC) to efficiently estimate the correctness of non-nested PWCTL model checking problems with a desired level of confidence, based on a number of independent runs of the NPTA. In addition to applying classical SMC algorithms, we also offer an extension that allows to efficiently compare performance properties of NPTAs in a parametric setting. The third contribution is an efficient tool implementation of our result and applications to several case studies.
For the entire collection see [Zbl 1223.68006].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68Q45 Formal languages and automata
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)

Software:

Ymer; HyTech; Uppaal; PHAVer; APMC
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoretical Computer Science 138(1), 3–34 (1995) · Zbl 0874.68206 · doi:10.1016/0304-3975(94)00202-T
[2] Alur, R., Dill, D.: A Theory of Timed Automata. Theoretical Computer Science 126, 183–235 (1994) · Zbl 0803.68071 · doi:10.1016/0304-3975(94)90010-8
[3] Alur, R., La Torre, S., Pappas, G.J.: Optimal paths in weighted timed automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) [7], pp. 49–62 · Zbl 0991.93076 · doi:10.1007/3-540-45351-2_8
[4] Baier, C., Bertrand, N., Bouyer, P., Brihaye, T., Größer, M.: Probabilistic and topological semantics for timed automata. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol. 4855, pp. 179–191. Springer, Heidelberg (2007) · Zbl 1135.68464 · doi:10.1007/978-3-540-77050-3_15
[5] Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004) · Zbl 1105.68350 · doi:10.1007/978-3-540-30080-9_7
[6] Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J., Vaandrager, F.W.: Minimum-cost reachability for priced timed automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) [7], pp. 147–161 · Zbl 0991.68037 · doi:10.7146/brics.v8i3.20457
[7] Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.): HSCC 2001. LNCS, vol. 2034. Springer, Heidelberg (2001) · Zbl 0990.00076
[8] Bertrand, N., Bouyer, P., Brihaye, T., Markey, N.: Quantitative model-checking of one-clock timed automata under probabilistic semantics. In: QEST, pp. 55–64. IEEE Computer Society, Los Alamitos (2008)
[9] Bogdoll, J., Fiorti, L.-M., Hartmanns, A., Hermanns, H.: Partial order methods for statistical model checking and simulation. In: Bruni, R., Dingel, J. (eds.) FORTE 2011 and FMOODS 2011. LNCS, vol. 6722, pp. 59–74. Springer, Heidelberg (2011) · Zbl 05908870 · doi:10.1007/978-3-642-21461-5_4
[10] Bohnenkamp, H., D’Argenio, P.R., Hermanns, H., Katoen, J.-P.: Modest: A compositional modeling formalism for real-time and stochastic systems. Technical Report CTIT 04-46, University of Twente (2004)
[11] Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
[12] Clarke, E.M., Donzé, A., Legay, A.: Statistical model checking of mixed-analog circuits with an application to a third order delta-sigma modulator. In: Chockler, H., Hu, A.J. (eds.) HVC 2008. LNCS, vol. 5394, pp. 149–163. Springer, Heidelberg (2009) · Zbl 05546343 · doi:10.1007/978-3-642-01702-5_16
[13] David, A., Larsen, K.G., Legay, A., Wang, Z., Mikucionis, M.: Time for real statistical model-checking: Statistical model-checking for real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 349–355. Springer, Heidelberg (2011) · Zbl 05940725 · doi:10.1007/978-3-642-22110-1_27
[14] David, A., Larsen, K.G., Legay, A., Nyman, U., Wasowski, A.: Timed I/O automata: a complete specification theory for real-time systems. In: HSCC. ACM, New York (2010) · Zbl 1361.68143
[15] Fehnker, A., van Hoesel, L., Mader, A.: Modelling and verification of the lmac protocol for wireless sensor networks. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 253–272. Springer, Heidelberg (2007) · Zbl 05523885 · doi:10.1007/978-3-540-73210-5_14
[16] Frehse, G.: Phaver: algorithmic verification of hybrid systems past hytech. STTT 10(3), 263–279 (2008) · Zbl 05536139 · doi:10.1007/s10009-007-0062-x
[17] Gómez, R.: A compositional translation of timed automata with deadlines to uppaal timed automata. In: Ouaknine, J., Vaandrager, F.W. (eds.) FORMATS 2009. LNCS, vol. 5813, pp. 179–194. Springer, Heidelberg (2009) · Zbl 1262.68091 · doi:10.1007/978-3-642-04368-0_15
[18] Hérault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 73–84. Springer, Heidelberg (2004) · Zbl 1202.68249 · doi:10.1007/978-3-540-24622-0_8
[19] Hérault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 73–84. Springer, Heidelberg (2004) · Zbl 1202.68249 · doi:10.1007/978-3-540-24622-0_8
[20] Jha, S.K., Clarke, E.M., Langmead, C.J., Legay, A., Platzer, A., Zuliani, P.: A bayesian approach to model checking biological systems. In: Degano, P., Gorrieri, R. (eds.) CMSB 2009. LNCS, vol. 5688, pp. 218–234. Springer, Heidelberg (2009) · Zbl 05609278 · doi:10.1007/978-3-642-03845-7_15
[21] Kaczmarczyk, V., Sir, M., Bradac, Z.: Stochastic timed automata simulator. In: 4th European Computing Conference. WSEAS
[22] Kaczmarczyk, V., Sir, M., Bradac, Z.: Stochastic timed automata simulator. In: Proceedings of the 4th European Computing Conference (2010)
[23] Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. In: POPL, pp. 344–352 (1989) · Zbl 0756.68035
[24] Maler, O., Larsen, K.G., Krogh, B.H.: On zone-based analysis of duration probabilistic automata. In: INFINITY. EPTCS, vol. 39, pp. 33–46 (2010) · doi:10.4204/EPTCS.39.3
[25] Minea, M.: Partial Order Reduction for Verification of Timed Systems. PhD thesis, Carnegie Mellon (1999) · Zbl 0939.68085
[26] Panangaden, P.: Labelled Markov Processes. Imperial College Press (2010) · Zbl 1190.60001
[27] Poulsen, D., van Vliet, J.: Duration probabilistic automata. Technical report, Aalborg University (2011)
[28] Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 202–215. Springer, Heidelberg (2004) · Zbl 1103.68639 · doi:10.1007/978-3-540-27813-9_16
[29] The smv model checker, http://www.kenmcmil.com/smv.html
[30] The spin tool (spin), http://spinroot.com/spin/whatispin.html
[31] Teige, T., Eggers, A., Fränzle, M.: Constraint-based analysis of concurrent probabilistic hybrid systems: An application to networked automation systems. In: Nonlinear Analysis: Hybrid Systems (2011) · Zbl 1225.93102 · doi:10.1016/j.nahs.2010.04.009
[32] The uppaal tool, http://www.uppaal.com/
[33] van Hoesel, L.F.W.: Sensors on speaking terms: schedule-based medium access control protocols for wireless sensor networks. PhD thesis, University of Twente (June 2007)
[34] Wald, R.: Sequential Analysis. Dove Publisher (2004) · Zbl 0029.15805
[35] Younes, H.L.S.: Verification and Planning for Stochastic Processes with Asynchronous Events. PhD thesis, Carnegie Mellon (2005)
[36] Younes, H.L.S.: Ymer: A statistical model checker. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 429–433. Springer, Heidelberg (2005) · Zbl 1081.68642 · doi:10.1007/11513988_43
[37] Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 223–235. Springer, Heidelberg (2002) · Zbl 1010.68513 · doi:10.1007/3-540-45657-0_17
[38] Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to simulink/stateflow verification. In: HSCC, pp. 243–252. ACM, New York (2010) · Zbl 1361.68154 · doi:10.1145/1755952.1755987
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.