{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T05:58:48Z","timestamp":1742968728607,"version":"3.40.3"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319682693"},{"type":"electronic","value":"9783319682709"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-68270-9_18","type":"book-chapter","created":{"date-parts":[[2017,9,26]],"date-time":"2017-09-26T07:17:19Z","timestamp":1506410239000},"page":"357-367","source":"Crossref","is-referenced-by-count":0,"title":["From Lotosphere to Thermosphere"],"prefix":"10.1007","author":[{"given":"Holger","family":"Hermanns","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,9,27]]},"reference":[{"key":"18_CR1","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126, 183\u2013235 (1994)","journal-title":"Theoret. Comput. Sci."},{"key":"18_CR2","unstructured":"Behrmann, G., Brinksma, E., Hendriks, M., Mader, A.: Production scheduling by reachability analysis - a case study. In: 19th International Parallel and Distributed Processing Symposium (IPDPS 2005), CD-ROM\/Abstracts Proceedings, Denver, CO, USA, 4\u20138 April 2005. IEEE Computer Society (2005)"},{"key":"18_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/BFb0020949","volume-title":"Hybrid Systems III","author":"J Bengtsson","year":"1996","unstructured":"Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., Yi, W.: UPPAAL\u2014a tool suite for automatic verification of real-time systems. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) HS 1995. LNCS, vol. 1066, pp. 232\u2013243. Springer, Heidelberg (1996). doi: 10.1007\/BFb0020949"},{"issue":"10","key":"18_CR4","doi-asserted-by":"crossref","first-page":"812","DOI":"10.1109\/TSE.2006.104","volume":"32","author":"HC Bohnenkamp","year":"2006","unstructured":"Bohnenkamp, H.C., D\u2019Argenio, P.R., Hermanns, H., Katoen, J.-P.: MODEST: a compositional modeling formalism for hard and softly timed systems. IEEE Trans. Softw. Eng. 32(10), 812\u2013830 (2006)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"18_CR5","doi-asserted-by":"crossref","unstructured":"Bohnenkamp, H.C., Hermanns, H., Klaren, R., Mader, A., Usenko, Y.S.: Synthesis and stochastic assessment of schedules for lacquer production. In: 1st International Conference on Quantitative Evaluation of Systems (QEST 2004), Enschede, The Netherlands, 27\u201330 September 2004, pp. 28\u201337. IEEE Computer Society (2004)","DOI":"10.1109\/QEST.2004.1348013"},{"key":"18_CR6","first-page":"25","volume":"14","author":"T Bolognesi","year":"1987","unstructured":"Bolognesi, T., Brinksma, E.: Introduction to the ISO specification language LOTOS. Comput. Netw. 14, 25\u201359 (1987)","journal-title":"Comput. Netw."},{"key":"18_CR7","unstructured":"Brinksma, E.: A theory for the derivation of tests. In: Aggarwal, S., Sabnani, K.K. (eds.) Protocol Specification, Testing and Verification V, Proceedings of the IFIP WG6.1 Eighth International Conference on Protocol Specification, Testing and Verification, pp. 171\u2013194. North-Holland (1988)"},{"key":"18_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/3-540-52559-9_63","volume-title":"Stepwise Refinement of Distributed Systems Models, Formalisms, Correctness","author":"E Brinksma","year":"1990","unstructured":"Brinksma, E.: Constraint-oriented specification in a constructive formal description technique. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1989. LNCS, vol. 430, pp. 130\u2013152. Springer, Heidelberg (1990). doi: 10.1007\/3-540-52559-9_63"},{"issue":"3","key":"18_CR9","doi-asserted-by":"crossref","first-page":"560","DOI":"10.1145\/828.833","volume":"31","author":"SD Brookes","year":"1984","unstructured":"Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. J. ACM 31(3), 560\u2013599 (1984)","journal-title":"J. ACM"},{"issue":"1","key":"18_CR10","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1145\/151646.151648","volume":"15","author":"R Cleaveland","year":"1993","unstructured":"Cleaveland, R., Parrow, J., Steffen, B.: The concurrency workbench: a semantics-based tool for the verification of concurrent systems. ACM Trans. Program. Lang. Syst. 15(1), 36\u201372 (1993)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"18_CR11","doi-asserted-by":"crossref","unstructured":"Creese, S.J., Roscoe, A.W.: Verifying an infinite family of inductions simultaneously using data independence and FDR. In: Wu, J., Chanson, S.T., Gao, Q. (eds.) Formal Methods for Protocol Engineering and Distributed Systems, FORTE XII\/PSTV XIX 1999, IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XII) and Protocol Specification, Testing and Verification (PSTV XIX), IFIP Conference Proceedings, Beijing, China, 5\u20138 October 1999, vol. 156, pp. 437\u2013452. Kluwer (1999)","DOI":"10.1007\/978-0-387-35578-8_25"},{"key":"18_CR12","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1016\/0304-3975(84)90113-0","volume":"34","author":"R Nicola De","year":"1984","unstructured":"De Nicola, R., Hennessy, M.: Testing equivalences for processes. Theoret. Comput. Sci. 34, 83\u2013133 (1984)","journal-title":"Theoret. Comput. Sci."},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"Garavel, H., Serwe,W.: The unheralded value of the multiway rendezvous: illustration with the production cell benchmark. In: Hermanns, H., H\u00f6fner, P. (eds.) Proceedings 2nd Workshop on Models for Formal Analysis of Real Systems, MARS@ETAPS 2017, EPTCS, Uppsala, Sweden, 29 April 2017, vol. 244, pp. 230\u2013270 (2017)","DOI":"10.4204\/EPTCS.244.10"},{"key":"18_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-319-67113-0_5","volume-title":"Critical Systems: Formal Methods and Automated Verification","author":"A Graf-Brill","year":"2017","unstructured":"Graf-Brill, A., Hermanns, H.: Model-based testing for asynchronous systems. In: Petrucci, L., Seceleanu, C., Cavalcanti, A. (eds.) FMICS 2017, AVoCS 2017. LNCS, vol. 10471, pp. 66\u201382. Springer, Cham (2017). doi: 10.1007\/978-3-319-67113-0_5"},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"Graf-Brill, A., Hartmanns, A., Hermanns, H., Rose, S.: Modelling and certification for electric mobility. In: 15th IEEE International Conference on Industrial Informatics, INDIN 2017, Emden, Germany, 24\u201326 July 2017. IEEE (2017)","DOI":"10.1109\/INDIN.2017.8104755"},{"key":"18_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-662-43613-4_6","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"A Graf-Brill","year":"2014","unstructured":"Graf-Brill, A., Hermanns, H., Garavel, H.: A model-based certification framework for the EnergyBus standard. In: \u00c1brah\u00e1m, E., Palamidessi, C. (eds.) FORTE 2014. LNCS, vol. 8461, pp. 84\u201399. Springer, Heidelberg (2014). doi: 10.1007\/978-3-662-43613-4_6"},{"issue":"2","key":"18_CR17","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/s10703-012-0167-z","volume":"43","author":"ME Hahn","year":"2013","unstructured":"Hahn, M.E., Hartmanns, A., Hermanns, H., Katoen, J.-P.: A compositional modelling and analysis framework for stochastic hybrid systems. Formal Methods Syst. Des. 43(2), 191\u2013232 (2013)","journal-title":"Formal Methods Syst. Des."},{"key":"18_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"593","DOI":"10.1007\/978-3-642-54862-8_51","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Hartmanns","year":"2014","unstructured":"Hartmanns, A., Hermanns, H.: The modest toolset: an integrated environment for quantitative modelling and verification. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 593\u2013598. Springer, Heidelberg (2014). doi: 10.1007\/978-3-642-54862-8_51"},{"key":"18_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/3-540-48778-6_17","volume-title":"Formal Methods for Real-Time and Probabilistic Systems","author":"K Havelund","year":"1999","unstructured":"Havelund, K., Larsen, K.G., Skou, A.: Formal verification of a power controller using the real-time model checker Uppaal. In: Katoen, J.-P. (ed.) ARTS 1999. LNCS, vol. 1601, pp. 277\u2013298. Springer, Heidelberg (1999). doi: 10.1007\/3-540-48778-6_17"},{"key":"18_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45804-2","volume-title":"Interactive Markov Chains: And the Quest for Quantified Quality","author":"H Hermanns","year":"2002","unstructured":"Hermanns, H.: Interactive Markov Chains: And the Quest for Quantified Quality. LNCS, vol. 2428. Springer, Heidelberg (2002). doi: 10.1007\/3-540-45804-2"},{"issue":"1","key":"18_CR21","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/S0167-6423(99)00019-2","volume":"36","author":"H Hermanns","year":"2000","unstructured":"Hermanns, H., Katoen, J.-P.: Automated compositional Markov chain generation for a plain-old telephone system. Sci. Comput. Program. 36(1), 97\u2013127 (2000)","journal-title":"Sci. Comput. Program."},{"key":"18_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1007\/3-540-44585-4_47","volume-title":"Computer Aided Verification","author":"K Larsen","year":"2001","unstructured":"Larsen, K., Behrmann, G., Brinksma, E., Fehnker, A., Hune, T., Pettersson, P., Romijn, J.: As cheap as possible: effcient cost-optimal reachability for priced timed automata. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 493\u2013505. Springer, Heidelberg (2001). doi: 10.1007\/3-540-44585-4_47"},{"issue":"5","key":"18_CR23","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1007\/s10009-009-0129-y","volume":"12","author":"A Mader","year":"2010","unstructured":"Mader, A., Bohnenkamp, H.C., Usenko, Y.S., Jansen, D.N., Hurink, J., Hermanns, H.: Synthesis and stochastic assessment of cost-optimal schedules. STTT 12(5), 305\u2013318 (2010)","journal-title":"STTT"},{"key":"18_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-78917-8_1","volume-title":"Formal Methods and Testing","author":"J Tretmans","year":"2008","unstructured":"Tretmans, J.: Model based testing with labelled transition systems. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) Formal Methods and Testing. LNCS, vol. 4949, pp. 1\u201338. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-78917-8_1"},{"key":"18_CR25","unstructured":"Tretmans, J., Kars, P., Brinksma, E.: Protocol conformance testing: a formal perspective on ISO IS-9646. In: Kroon, J., Heijink, R.J., Brinksma, E. (eds.) Protocol Test Systems IV, Proceedings of the IFIP TC6\/WG6.1 Fourth International Workshop on Protocol Test Systems, IFIP Transactions, Leidschendam, The Netherlands, 15\u201317 October 1991, vol. C-3, pp. 131\u2013142. North-Holland (1991)"},{"key":"18_CR26","unstructured":"Uppaal Cora (2005). http:\/\/people.cs.aau.dk\/~adavid\/cora\/introduction.html . Accessed 31 July 2017"},{"key":"18_CR27","unstructured":"Catastrophic Surface Pro 3 battery life finally has its firmware fix (2016). http:\/\/arstechnica.com\/?p=945575 . Accessed 31 July 2017"},{"key":"18_CR28","unstructured":"Samsung recalls Galaxy Note 7 worldwide due to exploding battery fears (2016). http:\/\/theverge.com\/2016\/9\/2\/12767670 . Accessed 31 July 2017"},{"key":"18_CR29","unstructured":"Basis Peak watches recalled (2016). http:\/\/techcrunch.com\/2016\/08\/03\/basis-peak-watches-recalled-due-to-overheating\/ . Accessed 31 July 2017"},{"key":"18_CR30","unstructured":"Important: Medical device correction, EnRhythm pacemakers (2010). http:\/\/www.medtronic.com\/enrhythm-advisory\/downloads\/enrhythm-battery-issues_physician-letter.pdf . Accessed 31 July 2017"},{"key":"18_CR31","unstructured":"Qualit\u00e4tsprobleme bei E-Bikes: Schlappe Akkus, anf\u00e4llige Elektronik (2011). http:\/\/www.spiegel.de\/auto\/aktuell\/a-790142.html . Accessed 31 July 2017"}],"container-title":["Lecture Notes in Computer Science","ModelEd, TestEd, TrustEd"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-68270-9_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,3]],"date-time":"2019-10-03T19:51:58Z","timestamp":1570132318000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-68270-9_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319682693","9783319682709"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-68270-9_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}