{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,2]],"date-time":"2025-06-02T04:03:46Z","timestamp":1748837026082,"version":"3.41.0"},"publisher-location":"Cham","reference-count":14,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319294728"},{"type":"electronic","value":"9783319294735"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-29473-5_10","type":"book-chapter","created":{"date-parts":[[2016,1,23]],"date-time":"2016-01-23T07:58:11Z","timestamp":1453535891000},"page":"162-177","source":"Crossref","is-referenced-by-count":1,"title":["Time Performance Formal Evaluation of Complex Systems"],"prefix":"10.1007","author":[{"given":"Valdivino Alexandre","family":"de Santiago J\u00fanior","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sofi\u00e8ne","family":"Tahar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,1,24]]},"reference":[{"key":"10_CR1","doi-asserted-by":"publisher","DOI":"10.1002\/0471200581","volume-title":"Queueing Networks and Markov Chains","author":"G Bolch","year":"1998","unstructured":"Bolch, G., Greiner, S., de Meer, H., Trivedi, K.S.: Queueing Networks and Markov Chains. Jonh Wiley & Sons, New York (1998)"},{"issue":"9","key":"10_CR2","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1145\/1810891.1810912","volume":"53","author":"C Baier","year":"2010","unstructured":"Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Performance evaluation and model checking join forces. Commun. ACM 53(9), 76\u201385 (2010)","journal-title":"Commun. ACM"},{"issue":"6","key":"10_CR3","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","volume":"29","author":"C Baier","year":"2003","unstructured":"Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time markov chains. IEEE Trans. Softw. Eng. 29(6), 524\u2013541 (2003)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"11","key":"10_CR4","doi-asserted-by":"publisher","first-page":"1427","DOI":"10.1016\/j.conengprac.2006.07.003","volume":"15","author":"M Kwiatkowska","year":"2006","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Controller dependability analysis by probabilistic model checking. Control Eng. Pract. 15(11), 1427\u20131434 (2006)","journal-title":"Control Eng. Pract."},{"key":"10_CR5","series-title":"Lecture Notes in Computer Science","first-page":"39","volume-title":"Interactive Systems","author":"M Massink","year":"2006","unstructured":"Massink, M., ter Beek, M.H., Latella, D.: Towards model checking stochastic aspects of the thinkteam user interface. In: Gilroy, S.W., Harrison, M.D. (eds.) DSV-IS 2005. LNCS, vol. 3941, pp. 39\u201350. Springer, Heidelberg (2006)"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Haverkort, B.R., Hermanns, H., Katoen, J.-P.: On the use of model checking techniques for dependability evaluation. In: Proceedings of IEEE Symposium Reliable Distributed Systems, pp. 228\u2013237. IEEE (2000)","DOI":"10.1109\/RELDI.2000.885410"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Grunske, L.: Specification patterns for probabilistic quality properties. In: Proceedings of the International Conference on Software Engineering, pp. 31\u201340. ACM (2008)","DOI":"10.1145\/1368088.1368094"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of the International Conference on Software Engineering, pp. 411\u2013420. ACM (1999)","DOI":"10.1145\/302405.302672"},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Konrad, S., Cheng, B.H.C.L.: Real-time specification patterns. In: Proceedings of the International Conference on Software Engineering, pp. 372\u2013381. ACM (2005)","DOI":"10.1145\/1062455.1062526"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-642-27705-4_18","volume-title":"Verified Software: Theories, Tools, Experiments","author":"J Hoenicke","year":"2012","unstructured":"Hoenicke, J., Post, A.: Formalization and analysis of real-time requirements: a feasibility study at BOSCH. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 225\u2013240. Springer, Heidelberg (2012)"},{"key":"10_CR11","doi-asserted-by":"publisher","first-page":"A108","DOI":"10.1051\/0004-6361\/201526343","volume":"580","author":"J Braga","year":"2015","unstructured":"Braga, J., D\u2019Amico, F., Avila, M.A.C., Penacchioni, A.V., Sacahui, J.R., de Santiago Jr., V.A., Mattiello-Francisco, F., Strauss, C., Fialho, M.A.A.: The protoMIRAX hard X-ray imaging balloon experiment. Astron. Astrophy. 580, A108 (2015)","journal-title":"Astron. Astrophy."},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Esteve, M.-A., Katoen, J.-P., Nguyen, V.Y., Postma, B., Yushtein, Y.: Formal correctness, safety, dependability, and performance analysis of a satellite. In: Proceedings of the International Conference on Software Engineering, pp. 1022\u20131031. IEEE Press (2012)","DOI":"10.1109\/ICSE.2012.6227118"},{"key":"10_CR13","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1016\/j.ress.2014.07.003","volume":"132","author":"M Bozzano","year":"2014","unstructured":"Bozzano, M., Cimatti, A., Katoen, J.-P., Katsaros, P., Mokos, K., Nguyen, V.Y., Noll, T., Postma, B., Roveri, M.: Spacecraft early design validation using formal methods. Reliab. Eng. Syst. Saf. 132, 20\u201335 (2014)","journal-title":"Reliab. Eng. Syst. Saf."},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Kikuchi, S., Matsumoto, Y.: Performance modeling of concurrent live migration operations in cloud computing systems using PRISM probabilistic model checker. In: Proceedings of the IEEE International Conference on Cloud Computing, pp. 49\u201356. IEEE (2011)","DOI":"10.1109\/CLOUD.2011.48"}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Foundations and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-29473-5_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T06:36:41Z","timestamp":1748759801000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-29473-5_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319294728","9783319294735"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-29473-5_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}