{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:31:10Z","timestamp":1725564670988},"publisher-location":"Berlin, Heidelberg","reference-count":48,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642152962"},{"type":"electronic","value":"9783642152979"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-15297-9_4","type":"book-chapter","created":{"date-parts":[[2010,9,6]],"date-time":"2010-09-06T08:11:13Z","timestamp":1283760673000},"page":"25-45","source":"Crossref","is-referenced-by-count":8,"title":["A Framework for Verification of Software with Time and Probabilities"],"prefix":"10.1007","author":[{"given":"Marta","family":"Kwiatkowska","sequence":"first","affiliation":[]},{"given":"Gethin","family":"Norman","sequence":"additional","affiliation":[]},{"given":"David","family":"Parker","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K. Larsen","year":"1997","unstructured":"Larsen, K., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. Journal on Software Tools for Technology Transfer\u00a01, 134\u2013152 (1997)","journal-title":"Int. Journal on Software Tools for Technology Transfer"},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/11691372_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Hinton","year":"2006","unstructured":"Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: A tool for automatic verification of probabilistic systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 441\u2013444. Springer, Heidelberg (2006)"},{"key":"4_CR3","volume-title":"Proc. QEST\u201909","author":"J.-P. Katoen","year":"2009","unstructured":"Katoen, J.-P., Hahn, E., Hermanns, H., Jansen, D., Zapreev, I.: The ins and outs of the probabilistic model checker MRMC. In: Proc. QEST\u201909, IEEE Press, Los Alamitos (2009)"},{"key":"4_CR4","unstructured":"Uppaal-PRO, http:\/\/www.cs.aau.dk\/~arild\/uppaal-probabilistic\/"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/978-3-642-04368-0_17","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"M. Kwiatkowska","year":"2009","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Stochastic games for verification of probabilistic timed automata. In: Ouaknine, J., Vaandrager, F.W. (eds.) FORMATS 2009. LNCS, vol.\u00a05813, pp. 212\u2013227. Springer, Heidelberg (2009)"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Hartmanns, A., Hermanns, H.: A Modest approach to checking probabilistic timed automata. In: Proc. QEST\u201909, pp. 187\u2013196 (2009)","DOI":"10.1109\/QEST.2009.41"},{"key":"4_CR7","volume-title":"Proc. QEST\u201910","author":"J. Berendsen","year":"2010","unstructured":"Berendsen, J., Jansen, D., Vaandrager, F.: Fortuna: Model checking priced probabilistic timed automata. In: Proc. QEST\u201910, IEEE Press, Los Alamitos (2010)"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-540-93900-9_17","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M. Kattenbelt","year":"2009","unstructured":"Kattenbelt, M., Kwiatkowska, M., Norman, G., Parker, D.: Abstraction refinement for probabilistic software. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) VMCAI 2009. LNCS, vol.\u00a05403, pp. 182\u2013197. Springer, Heidelberg (2009)"},{"key":"4_CR9","first-page":"157","volume-title":"Proc. QEST\u201906","author":"M. Kwiatkowska","year":"2006","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Game-based abstraction for Markov decision processes. In: Proc. QEST\u201906, pp. 157\u2013166. IEEE Press, Los Alamitos (2006)"},{"key":"4_CR10","unstructured":"Kattenbelt, M., Kwiatkowska, M., Norman, G., Parker, D.: A game-based abstraction-refinement framework for Markov decision processes. Technical Report RR-08-06, Oxford University Computing Laboratory (2008)"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Vardi, M.: Formal techniques for SystemC verification. In: Proc. DAC\u201907, pp. 188\u2013192 (2007); Position Paper","DOI":"10.1145\/1278480.1278527"},{"key":"4_CR12","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: A framework for verification of software with time and probabilities (extended version), http:\/\/qav.comlab.ox.ac.uk\/papers\/formats10extended.pdf"},{"key":"4_CR13","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-9455-6","volume-title":"Denumerable Markov Chains","author":"J. Kemeny","year":"1976","unstructured":"Kemeny, J., Snell, J., Knapp, A.: Denumerable Markov Chains. Springer, Heidelberg (1976)"},{"key":"4_CR14","doi-asserted-by":"publisher","first-page":"1095","DOI":"10.1073\/pnas.39.10.1095","volume":"39","author":"L. Shapley","year":"1953","unstructured":"Shapley, L.: Stochastic games. Proc. National Academy of Science\u00a039, 1095\u20131100 (1953)","journal-title":"Proc. National Academy of Science"},{"key":"4_CR15","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1016\/0890-5401(92)90048-K","volume":"96","author":"A. Condon","year":"1992","unstructured":"Condon, A.: The complexity of stochastic games. Inf. and Comp.\u00a096, 203\u2013224 (1992)","journal-title":"Inf. and Comp."},{"key":"4_CR16","doi-asserted-by":"crossref","DOI":"10.1002\/9780470316887","volume-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"M. Puterman","year":"1994","unstructured":"Puterman, M.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley and Sons, Chichester (1994)"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1007\/978-3-642-11319-2_26","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"B. Wachter","year":"2010","unstructured":"Wachter, B., Zhang, L.: Best probabilistic transformers. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol.\u00a05944, pp. 362\u2013379. Springer, Heidelberg (2010)"},{"key":"4_CR18","first-page":"238","volume-title":"Proc. POPL\u201977","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. POPL\u201977, pp. 238\u2013252. ACM Press, New York (1977)"},{"key":"4_CR19","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"T. Henzinger","year":"1994","unstructured":"Henzinger, T., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Information and Computation\u00a0111, 193\u2013244 (1994)","journal-title":"Information and Computation"},{"key":"4_CR20","unstructured":"Tripakis, S.: The formal analysis of timed systems in practice. PhD thesis, Universit\u00e9 Joseph Fourier (1998)"},{"key":"4_CR21","unstructured":"Jensen, H.: Model checking probabilistic real time systems. In: Proc. 7th Nordic Workshop on Programming Theory, pp. 247\u2013261 (1996)"},{"key":"4_CR22","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0304-3975(01)00046-9","volume":"282","author":"M. Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theoretical Computer Science\u00a0282, 101\u2013150 (2002)","journal-title":"Theoretical Computer Science"},{"key":"4_CR23","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/S0304-3975(01)00215-8","volume":"292","author":"D. Beauquier","year":"2003","unstructured":"Beauquier, D.: Probabilistic timed automata. Theoretical Computer Science\u00a0292, 65\u201384 (2003)","journal-title":"Theoretical Computer Science"},{"key":"4_CR24","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/s10703-006-0005-2","volume":"29","author":"M. Kwiatkowska","year":"2006","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Sproston, J.: Performance analysis of probabilistic timed automata using digital clocks. Formal Methods in System Design\u00a029, 33\u201378 (2006)","journal-title":"Formal Methods in System Design"},{"key":"4_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"4_CR26","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R. Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Dill, D.: Model-checking in dense real-time. Information and Computation\u00a0104, 2\u201334 (1993)","journal-title":"Information and Computation"},{"key":"4_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/11513988_5","volume-title":"Computer Aided Verification","author":"S. Lahiri","year":"2005","unstructured":"Lahiri, S., Ball, T., Cook, B.: Predicate abstraction via symbolic decision procedures. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 24\u201338. Springer, Heidelberg (2005)"},{"key":"4_CR28","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1023\/B:FORM.0000040025.89719.f3","volume":"25","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSI-C programs using SAT. Formal Methods in System Design\u00a025, 105\u2013127 (2004)","journal-title":"Formal Methods in System Design"},{"key":"4_CR29","first-page":"337","volume-title":"Proc. DSD\u201902","author":"R. Drechsler","year":"2002","unstructured":"Drechsler, R., Grosse, D.: Reachability analysis for formal verification of SystemC. In: Proc. DSD\u201902, p. 337. IEEE Press, Los Alamitos (2002)"},{"key":"4_CR30","first-page":"101","volume-title":"Proc. MEMOCODE\u201905","author":"D. Kroening","year":"2005","unstructured":"Kroening, D., Sharygina, N.: Formal verification of SystemC by automatic hardware\/software partitioning. In: Proc. MEMOCODE\u201905, pp. 101\u2013110. IEEE Press, Los Alamitos (2005)"},{"key":"4_CR31","first-page":"43","volume-title":"Proc. 16th ACM Great Lakes Symp. VLSI","author":"D. Grosse","year":"2006","unstructured":"Grosse, D., K\u00fchne, U., Drechsler, R.: HW\/SW co-verification of embedded systems using bounded model checking. In: Proc. 16th ACM Great Lakes Symp. VLSI, pp. 43\u201348. ACM Press, New York (2006)"},{"key":"4_CR32","doi-asserted-by":"crossref","unstructured":"Karlsson, D., Eles, P., Peng, Z.: Formal verification of SystemC designs using a Petri-net based representation. In: Proc. DATE\u201906, EDAA, pp. 1228\u20131233 (2006)","DOI":"10.1109\/DATE.2006.244076"},{"key":"4_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/978-3-540-73370-6_14","volume-title":"Model Checking Software","author":"C. Traulsen","year":"2007","unstructured":"Traulsen, C., Cornet, J., Moy, M., Maraninchi, F.: A SystemC\/TLM semantics in Promela and its possible applications. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol.\u00a04595, pp. 204\u2013222. Springer, Heidelberg (2007)"},{"key":"4_CR34","doi-asserted-by":"crossref","unstructured":"Herber, P., Fellmuth, J., Glesner, S.: Model checking SystemC designs using timed automata. In: Proc. CODES+ISSS\u201908, pp. 131\u2013136 (2008)","DOI":"10.1145\/1450135.1450166"},{"key":"4_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1007\/978-3-540-78800-3_36","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N. Blanc","year":"2008","unstructured":"Blanc, N., Kroening, D., Sharygina, N.: Scoot: A tool for the analysis of SystemC models. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 467\u2013470. Springer, Heidelberg (2008)"},{"key":"4_CR36","doi-asserted-by":"crossref","unstructured":"Moy, M., Maraninchi, F., Maillet-Contoz, L.: Pinapa: An extraction tool for SystemC descriptions of Systems-on-a-Chip. In: Proc. EMSOFT\u201905, pp. 317\u2013324 (2005)","DOI":"10.1145\/1086228.1086286"},{"key":"4_CR37","unstructured":"IEEE Standards Association: IEEE standard 1666: SystemC language reference manual (2005), http:\/\/www.systemc.org\/"},{"key":"4_CR38","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/s10009-003-0118-5","volume":"5","author":"C. Daws","year":"2004","unstructured":"Daws, C., Kwiatkowska, M., Norman, G.: Automatic verification of the IEEE 1394 root contention protocol with KRONOS and PRISM. Int. Journal on Software Tools for Technology Transfer\u00a05, 221\u2013236 (2004)","journal-title":"Int. Journal on Software Tools for Technology Transfer"},{"key":"4_CR39","doi-asserted-by":"publisher","first-page":"1027","DOI":"10.1016\/j.ic.2007.01.004","volume":"205","author":"M. Kwiatkowska","year":"2007","unstructured":"Kwiatkowska, M., Norman, G., Sproston, J., Wang, F.: Symbolic model checking for probabilistic timed automata. Inf. and Comp.\u00a0205, 1027\u20131077 (2007)","journal-title":"Inf. and Comp."},{"key":"4_CR40","first-page":"311","volume-title":"Proc. QEST\u201906","author":"J. Berendsen","year":"2006","unstructured":"Berendsen, J., Jansen, D., Katoen, J.P.: Probably on time and within budget on reachability in priced probabilistic timed automata. In: Proc. QEST\u201906, pp. 311\u2013322. IEEE Press, Los Alamitos (2006)"},{"key":"4_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/3-540-45605-8_5","volume-title":"Process Algebra and Probabilistic Methods. Performance Modeling and Verification","author":"P. D\u2019Argenio","year":"2002","unstructured":"D\u2019Argenio, P., Jeannet, B., Jensen, H., Larsen, K.: Reduction and refinement strategies for probabilistic analysis. In: Hermanns, H., Segala, R. (eds.) PROBMIV 2002, PAPM-PROBMIV 2002, and PAPM 2002. LNCS, vol.\u00a02399, pp. 57\u201376. Springer, Heidelberg (2002)"},{"key":"4_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-540-70545-1_16","volume-title":"Computer Aided Verification","author":"H. Hermanns","year":"2008","unstructured":"Hermanns, H., Wachter, B., Zhang, L.: Probabilistic CEGAR. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 162\u2013175. Springer, Heidelberg (2008)"},{"key":"4_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-540-73368-3_38","volume-title":"Computer Aided Verification","author":"L. Alfaro de","year":"2007","unstructured":"de Alfaro, L., Roy, P.: Magnifying-lens abstraction for Markov decision processes. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 325\u2013338. Springer, Heidelberg (2007)"},{"key":"4_CR44","doi-asserted-by":"crossref","unstructured":"Chadha, R., Viswanathan, M.: A counterexample guided abstraction-refinement framework for Markov decision processes. ACM Transactions on Computational Logic (to appear, 2010)","DOI":"10.1145\/1838552.1838553"},{"key":"4_CR45","doi-asserted-by":"crossref","unstructured":"Kemper, S., Platzer, A.: SAT-based abstraction refinement for real-time systems. In: STACS 1985. ENTCS, vol.\u00a0182, pp. 107\u2013122 (2006)","DOI":"10.1016\/j.entcs.2006.09.034"},{"key":"4_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/978-3-540-30206-3_25","volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"M. Sorea","year":"2004","unstructured":"Sorea, M.: Lazy approximation for dense real-time systems. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol.\u00a03253, pp. 363\u2013378. Springer, Heidelberg (2004)"},{"key":"4_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-540-75454-1_10","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"H. Dierks","year":"2007","unstructured":"Dierks, H., Kupferschmid, S., Larsen, K.: Automatic abstraction refinement for timed automata. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol.\u00a04763, pp. 114\u2013129. Springer, Heidelberg (2007)"},{"key":"4_CR48","first-page":"579","volume":"79","author":"A. Zbrzezny","year":"2008","unstructured":"Zbrzezny, A., P\u00f3\u0142rola: SAT-based reachability checking for timed automata with discrete data. Fundamenta Informaticae\u00a079, 579\u2013593 (2008)","journal-title":"Fundamenta Informaticae"}],"container-title":["Lecture Notes in Computer Science","Formal Modeling and Analysis of Timed Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15297-9_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T03:04:32Z","timestamp":1606187072000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15297-9_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642152962","9783642152979"],"references-count":48,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15297-9_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}