{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T22:25:28Z","timestamp":1759184728269,"version":"3.41.0"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319175805"},{"type":"electronic","value":"9783319175812"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-17581-2_2","type":"book-chapter","created":{"date-parts":[[2015,4,15]],"date-time":"2015-04-15T12:22:36Z","timestamp":1429100556000},"page":"17-31","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Safety, Dependability and Performance Analysis of Aerospace Systems"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Noll","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,4,16]]},"reference":[{"issue":"6","key":"2_CR1","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."},{"key":"2_CR2","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"issue":"5","key":"2_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-2(5:5)2006","volume":"2","author":"A Biere","year":"2006","unstructured":"Biere, A., Heljanko, K., Junttila, T.A., Latvala, T., Schuppan, V.: Linear encodings of bounded LTL model checking. Log. Methods Comput. Sci. 2(5), 1\u201364 (2006)","journal-title":"Log. Methods Comput. Sci."},{"key":"2_CR5","unstructured":"Bittner, B., Bozzano, M., Cimatti, A., Olive, X.: Symbolic synthesis of observability requirements for diagnosability. In: Proceedings of 11th Symposium on Advanced Space Technologies in Robotics and Automation (ASTRA 2011), ESA\/ESTEC (2011) http:\/\/robotics.estec.esa.int\/ASTRA\/Astra2011\/Astra2011_Proceedings.zip"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Boudali, H., Crouzen, P., Stoelinga, M.: A rigorous, compositional and extensible framework for dynamic fault tree analysis. In: Dependable and Secure Computing, pp. 128\u2013143. IEEE (2010)","DOI":"10.1109\/TDSC.2009.45"},{"key":"2_CR7","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/s10817-005-9004-z","volume":"35","author":"M Bozzano","year":"2005","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., van Rossum, P., Schulz, S., Sebastiani, R.: Mathsat: tight integration of SAT and mathematical decision procedures. J. Autom. Reasoning 35, 265\u2013293 (2005)","journal-title":"J. Autom. Reasoning"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-642-04468-7_15","volume-title":"Computer Safety, Reliability, and Security","author":"M Bozzano","year":"2009","unstructured":"Bozzano, M., Cimatti, A., Katoen, J.-P., Nguyen, V.Y., Noll, T., Roveri, M.: The COMPASS approach: correctness, modelling and performability of aerospace systems. In: Buth, B., Rabe, G., Seyfarth, T. (eds.) SAFECOMP 2009. LNCS, vol. 5775, pp. 173\u2013186. Springer, Heidelberg (2009)"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-540-75596-8_13","volume-title":"Automated Technology for Verification and Analysis","author":"M Bozzano","year":"2007","unstructured":"Bozzano, M., Cimatti, A., Tapparo, F.: Symbolic fault tree analysis for reactive systems. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 162\u2013176. Springer, Heidelberg (2007)"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Bozzano, M., Cavada, R., Cimatti, A., Katoen, J.P., Nguyen, V.Y., Noll, T., Olive, X.: Formal verification and validation of aadl models. In: Embedded Real Time Software and Systems Conference, AAAF & SEE (2010)","DOI":"10.1145\/1595696.1595744"},{"key":"2_CR11","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."},{"issue":"5","key":"2_CR12","doi-asserted-by":"publisher","first-page":"754","DOI":"10.1093\/comjnl\/bxq024","volume":"54","author":"M Bozzano","year":"2011","unstructured":"Bozzano, M., Cimatti, A., Katoen, J.P., Nguyen, V.Y., Noll, T., Roveri, M.: Safety, dependability, and performance analysis of extended AADL models. Comput. J. 54(5), 754\u2013775 (2011)","journal-title":"Comput. J."},{"key":"2_CR13","unstructured":"Cimatti, A., Pecheur, C., Cavada, R.: Formal verification of diagnosability via symbolic model checking. In: International Joint Conference on Artificial Intelligence (IJCAI), pp. 363\u2013369. Morgan Kaufmann (2003)"},{"key":"2_CR14","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":"2_CR15","unstructured":"COMPASS Consortium: The COMPASS project web site. http:\/\/compass.informatik.rwth-aachen.de\/"},{"issue":"6","key":"2_CR16","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1016\/S0020-0190(03)00343-0","volume":"87","author":"S Derisavi","year":"2003","unstructured":"Derisavi, S., Hermanns, H., Sanders, W.H.: Optimal state-space lumping in Markov chains. Inf. Process. Lett. 87(6), 309\u2013315 (2003)","journal-title":"Inf. Process. Lett."},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"Dwyer, M., Avrunin, G., Corbett, J.: Patterns in property specifications for finite-state verification. In: International Conference on Software Engineering (ICSE), pp. 411\u2013420. IEEE CS Press (1999)","DOI":"10.1145\/302405.302672"},{"key":"2_CR18","unstructured":"ECSS: Space product assurance: Fault tree analysis - adoption notice ECSS\/IEC 61025. ECSS Standard Q-ST-40-12C, European Cooperation for Space Standardization, July 2008"},{"key":"2_CR19","unstructured":"ECSS: Space product assurance: Failure modes, effects (and criticality) analysis (FMEA\/FMECA). ECSS Standard Q-ST-30-02C, European Cooperation for Space Standardization, March 2009"},{"key":"2_CR20","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: 34th International Conference on Software Engineering (ICSE 2012), pp. 1022\u20131031. ACM and IEEE CS Press (2012)","DOI":"10.1109\/ICSE.2012.6227118"},{"key":"2_CR21","unstructured":"FBK: FSAP: The formal safety analysis platform. http:\/\/fsap.fbk.eu\/"},{"key":"2_CR22","unstructured":"FBK: MathSAT. http:\/\/mathsat.fbk.eu"},{"key":"2_CR23","unstructured":"FBK: NuSMV: A new symbolic model checker. http:\/\/nusmv.fbk.eu"},{"key":"2_CR24","volume-title":"Model-Based Engineering with AADL: an introduction to the sae architecture analysis & design language","author":"PH Feiler","year":"2012","unstructured":"Feiler, P.H., Gluch, D.P.: Model-Based Engineering with AADL: an introduction to the sae architecture analysis & design language. Addison-Wesley Professional, Boston (2012)"},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"Grunske, L.: Specification patterns for probabilistic quality properties. In: International Conference on Software Engineering (ICSE), pp. 31\u201340. ACM (2008)","DOI":"10.1145\/1368088.1368094"},{"key":"2_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/978-3-642-28891-3_4","volume-title":"NASA Formal Methods","author":"D Guck","year":"2012","unstructured":"Guck, D., Han, T., Katoen, J.-P., Neuh\u00e4u\u00dfer, M.R.: Quantitative timed analysis of interactive Markov chains. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 8\u201323. Springer, Heidelberg (2012)"},{"key":"2_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/11513988_10","volume-title":"Computer Aided Verification","author":"K Heljanko","year":"2005","unstructured":"Heljanko, K., Junttila, T.A., Latvala, T.: Incremental and complete bounded model checking for full PLTL. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 98\u2013111. Springer, Heidelberg (2005)"},{"key":"2_CR28","doi-asserted-by":"crossref","unstructured":"Henzinger, T.: The theory of hybrid automata. In: IEEE Symposium on Logic in Computer Science (LICS), pp. 278\u2013292. IEEE CS Press (1996)","DOI":"10.1109\/LICS.1996.561342"},{"key":"2_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/3-540-45804-2_6","volume-title":"Interactive Markov Chains","author":"H Hermanns","year":"2002","unstructured":"Hermanns, H.: Interactive Markov chains in practice. In: Hermanns, H. (ed.) Interactive Markov Chains. LNCS, vol. 2428, p. 129. Springer, Heidelberg (2002)"},{"issue":"2","key":"2_CR30","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1016\/j.peva.2010.04.001","volume":"68","author":"JP Katoen","year":"2011","unstructured":"Katoen, J.P., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker MRMC. Perform. Eval. 68(2), 90\u2013104 (2011)","journal-title":"Perform. Eval."},{"key":"2_CR31","unstructured":"MRMC Consortium: MRMC \u2013 The Markov Reward Model Checker. http:\/\/www.mrmc-tool.org\/"},{"key":"2_CR32","unstructured":"SAE: Architecture Analysis and Design Language (AADL). SAE Standard AS5506, International Society of Automotive Engineers, May 2004"},{"key":"2_CR33","unstructured":"SAE: Architecture Analysis and Design Language (AADL) Annex, Volume 1, Annex A: Graphical AADL Notation. SAE Standard AS5506\/1, International Society of Automotive Engineers, June 2006"},{"key":"2_CR34","unstructured":"SAE: Architecture Analysis and Design Language Annex (AADL), Volume 1, Annex E: Error Model Annex. SAE Standard AS5506\/1, International Society of Automotive Engineers, June 2006"},{"key":"2_CR35","unstructured":"SAE: Architecture Analysis and Design Language (AADL) Rev. B. SAE Standard AS5506B, International Society of Automotive Engineers, September 2012"},{"key":"2_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/978-3-642-12002-2_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Valmari","year":"2010","unstructured":"Valmari, A., Franceschinis, G.: Simple O(m logn) time Markov chain lumping. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 38\u201352. Springer, Heidelberg (2010)"},{"key":"2_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/11901914_35","volume-title":"Automated Technology for Verification and Analysis","author":"R Wimmer","year":"2006","unstructured":"Wimmer, R., Herbstritt, M., Hermanns, H., Strampp, K., Becker, B.: Sigref \u2013 a symbolic bisimulation tool box. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol. 4218, pp. 477\u2013492. Springer, Heidelberg (2006)"},{"key":"2_CR38","doi-asserted-by":"crossref","unstructured":"Yushtein, Y., Bozzano, M., Cimatti, A., Katoen, J.P., Nguyen, V., Noll, T., Olive, X., Roveri, M.: System-software co-engineering: dependability and safety perspective. In: Proceedings of the 4th IEEE International Conference on Space Mission Challenges for Information Technology (SMC-IT 2011), pp. 18\u201325. IEEE CS Press (2011)","DOI":"10.1109\/SMC-IT.2011.16"}],"container-title":["Communications in Computer and Information Science","Formal Techniques for Safety-Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-17581-2_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,22]],"date-time":"2025-05-22T15:36:49Z","timestamp":1747928209000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-17581-2_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319175805","9783319175812"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-17581-2_2","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"16 April 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}