{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T15:59:57Z","timestamp":1743004797108,"version":"3.40.3"},"publisher-location":"Cham","reference-count":15,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319295091"},{"type":"electronic","value":"9783319295107"}],"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":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-29510-7_10","type":"book-chapter","created":{"date-parts":[[2016,1,29]],"date-time":"2016-01-29T14:39:16Z","timestamp":1454078356000},"page":"172-186","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Leveraging Abstraction to Establish Out-of-Nominal Safety Properties"],"prefix":"10.1007","author":[{"given":"Jackson R.","family":"Mayo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert C.","family":"Armstrong","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Geoffrey C.","family":"Hulette","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,1,30]]},"reference":[{"key":"10_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, Cambridge (2010)","edition":"1"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359\u2013364. Springer, Heidelberg (2002)"},{"key":"10_CR3","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E Clarke","year":"2003","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50, 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-642-25929-6_4","volume-title":"Mathematical and Engineering Methods in Computer Science","author":"G Fey","year":"2012","unstructured":"Fey, G.: Assessing system vulnerability using formal verification techniques. In: Kot\u00e1sek, Z., Bouda, J., \u010cern\u00e1, I., Sekanina, L., Vojnar, T., Anto\u0161, D. (eds.) MEMICS 2011. LNCS, vol. 7119, pp. 47\u201356. Springer, Heidelberg (2012)"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"G\u00fcdemann, M., Ortmeier, F.: Probabilistic model-based safety analysis. In: Proceedings of the 8th Workshop on Quantitative Aspects of Programming Languages, pp. 114\u2013128, March 2010","DOI":"10.4204\/EPTCS.28.8"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Jackson, M., Zave, P.: Deriving specifications from requirements: an example. In: Proceedings of the 17th International Conference on Software Engineering, pp. 15\u201324 (1995)","DOI":"10.1145\/225014.225016"},{"key":"10_CR7","unstructured":"Joshi, A., Heimdahl, M.P.E., Miller, S.P., Whalen, M.W.: Model-based safety analysis. NASA Contractor Report CR-2006-213953, February 2006"},{"key":"10_CR8","unstructured":"Joshi, A., Miller, S.P., Whalen, M., Heimdahl, M.P.: A proposal for model-based safety analysis. In: Proceedings of the 24th Digital Avionics Systems Conference, October 2005"},{"key":"10_CR9","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780195079517.001.0001","volume-title":"The Origins of Order: Self-Organization and Selection in Evolution","author":"SA Kauffman","year":"1993","unstructured":"Kauffman, S.A.: The Origins of Order: Self-Organization and Selection in Evolution. Oxford University Press, Oxford (1993)"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and CEGAR for higher-order model checking. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 222\u2013233, June 2011","DOI":"10.1145\/1993498.1993525"},{"key":"10_CR11","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"L Lamport","year":"2002","unstructured":"Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston (2002)"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Mayo, J.R., Armstrong, R.C., Hulette, G.C.: Digital system robustness via design constraints: the lesson of formal methods. In: Proceedings of the 9th Annual IEEE International Systems Conference, pp. 109\u2013114, April 2015","DOI":"10.1109\/SYSCON.2015.7116737"},{"key":"10_CR13","doi-asserted-by":"publisher","first-page":"033124","DOI":"10.1063\/1.3187791","volume":"19","author":"T Mytkowicz","year":"2009","unstructured":"Mytkowicz, T., Diwan, A., Bradley, E.: Computer systems are dynamical systems. Chaos 19, 033124 (2009)","journal-title":"Chaos"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Seshia, S.A., Li, W., Mitra, S.: Verification-guided soft error resilience. In: Proceedings of the Conference on Design, Automation and Test in Europe, pp. 1442\u20131447, April 2007","DOI":"10.1109\/DATE.2007.364501"},{"key":"10_CR15","doi-asserted-by":"publisher","first-page":"108702","DOI":"10.1103\/PhysRevLett.107.108702","volume":"107","author":"Y Vorobeychik","year":"2011","unstructured":"Vorobeychik, Y., Mayo, J.R., Armstrong, R.C., Ruthruff, J.R.: Noncooperatively optimized tolerance: decentralized strategic optimization in complex systems. Phys. Rev. Lett. 107, 108702 (2011)","journal-title":"Phys. Rev. Lett."}],"container-title":["Communications in Computer and Information Science","Formal Techniques for Safety-Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-29510-7_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,14]],"date-time":"2024-06-14T01:48:01Z","timestamp":1718329681000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-29510-7_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319295091","9783319295107"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-29510-7_10","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"30 January 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}