{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,17]],"date-time":"2026-08-17T15:01:21Z","timestamp":1786978881435,"version":"build-2736575974"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031197550","type":"print"},{"value":"9783031197567","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-19756-7_7","type":"book-chapter","created":{"date-parts":[[2022,10,19]],"date-time":"2022-10-19T03:02:54Z","timestamp":1666148574000},"page":"105-134","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Formalization of\u00a0the\u00a0AADL Run-Time Services"],"prefix":"10.1007","author":[{"given":"John","family":"Hatcliff","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jerome","family":"Hugues","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Danielle","family":"Stewart","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lutz","family":"Wrage","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2022,10,17]]},"reference":[{"key":"7_CR1","unstructured":"SAE AS5506\/2. AADL annex volume 2"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/978-3-319-17524-9_7","volume-title":"NASA Formal Methods","author":"J Backes","year":"2015","unstructured":"Backes, J., Cofer, D., Miller, S., Whalen, M.W.: Requirements analysis of a quad-redundant flight control system. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 82\u201396. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-17524-9_7"},{"key":"7_CR3","volume-title":"Programming in ADA","author":"JG Barnes","year":"1984","unstructured":"Barnes, J.G.: Programming in ADA. Addison-Wesley Longman Publishing Co., Inc, London (1984)"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-642-01924-1_15","volume-title":"Reliable Software Technologies \u2013 Ada-Europe 2009","author":"B Berthomieu","year":"2009","unstructured":"Berthomieu, B., Bodeveix, J.-P., Chaudet, C., Dal Zilio, S., Filali, M., Vernadat, F.: Formal verification of AADL specifications in the topcased environment. In: Kordon, F., Kermarrec, Y. (eds.) Ada-Europe 2009. LNCS, vol. 5570, pp. 207\u2013221. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-01924-1_15"},{"key":"7_CR5","unstructured":"Berthomieu, B., et al.: Formal verification of AADL models with Fiacre and Tina. In: ERTSS 2010-Embedded Real-Time Software and Systems, pp. 1\u20139 (2010)"},{"key":"7_CR6","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-981-10-4436-6_3","volume-title":"Cyber-Physical System Design from an Architecture Analysis Viewpoint","author":"L Besnard","year":"2017","unstructured":"Besnard, L., et al.: Formal semantics of behavior specifications in the architecture analysis and design language standard. In: Nakajima, S., Talpin, J.-P., Toyoshima, M., Yu, H. (eds.) Cyber-Physical System Design from an Architecture Analysis Viewpoint, pp. 53\u201379. Springer, Singapore (2017). https:\/\/doi.org\/10.1007\/978-981-10-4436-6_3"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Borde, E., Rahmoun, S., Cadoret, F., Pautet, L., Singhoff, F., Dissaux, P.: Architecture models refinement for fine grain timing analysis of embedded systems. In: 2014 25nd IEEE International Symposium on Rapid System Prototyping, pp. 44\u201350 (2014)","DOI":"10.1109\/RSP.2014.6966691"},{"key":"7_CR8","unstructured":"Burns, A., Wellings, A.: Analysable real-time systems: programmed in Ada. CreateSpace (2016)"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Carr\u00e9, B., Garnsworthy, J.: SPARK - an annotated Ada subset for safety-critical programming. In: Proceedings of the Conference on TRI-ADA 1990, pp. 392\u2013402 (1990)","DOI":"10.1145\/255471.255563"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-642-01648-6_2","volume-title":"Models in Software Engineering","author":"MY Chkouri","year":"2009","unstructured":"Chkouri, M.Y., Robert, A., Bozga, M., Sifakis, J.: Translating AADL into BIP - application to the verification of real-time systems. In: Chaudron, M.R.V. (ed.) MODELS 2008. LNCS, vol. 5421, pp. 5\u201319. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-01648-6_2"},{"key":"7_CR11","first-page":"2","volume":"01","author":"D Cofer","year":"2022","unstructured":"Cofer, D., et al.: Cyber-assured systems engineering at scale. IEEE Secur. Priv. 01, 2\u201314 (2022)","journal-title":"IEEE Secur. Priv."},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-642-28891-3_13","volume-title":"NASA Formal Methods","author":"D Cofer","year":"2012","unstructured":"Cofer, D., Gacek, A., Miller, S., Whalen, M.W., LaValley, B., Sha, L.: Compositional verification of architectural models. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 126\u2013140. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28891-3_13"},{"key":"7_CR13","unstructured":"Feiler, P., Rugina, A.: Dependability modeling with the architecture analysis and design language (AADL). Technical report, Software Engineering INST, Carnegie-Mellon University, Pittsburgh, PA (2007)"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Feiler, P.H.: Efficient embedded runtime systems through port communication optimization. In: 13th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2008), pp. 294\u2013300 (2008)","DOI":"10.1109\/ICECCS.2008.20"},{"key":"7_CR15","volume-title":"Model-Based Engineering with AADL: An Introduction to the SAE Architecture Analysis and Design Language","author":"PH Feiler","year":"2013","unstructured":"Feiler, P.H., Gluch, D.P.: Model-Based Engineering with AADL: An Introduction to the SAE Architecture Analysis and Design Language. Addison-Wesley, Reading (2013)"},{"key":"7_CR16","doi-asserted-by":"publisher","first-page":"72814","DOI":"10.1109\/ACCESS.2020.2987972","volume":"8","author":"ASA Hadad","year":"2020","unstructured":"Hadad, A.S.A., Ma, C., Ahmed, A.A.O.: Formal verification of AADL models by Event-B. IEEE Access 8, 72814\u201372834 (2020)","journal-title":"IEEE Access"},{"key":"7_CR17","doi-asserted-by":"publisher","unstructured":"Hatcliff, J., Belt, J., Robby, Carpenter, T.: HAMR: an AADL multi-platform code generation toolset. In: Margaria, T., Steffen, B. (eds.) ISoLA 2021. LNCS, vol. 13036, pp. 274\u2013295. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-89159-6_18","DOI":"10.1007\/978-3-030-89159-6_18"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Hatcliff, J., Hugues, J., Stewart, D., Wrage, L.: Formalization of the AADL run-time services (extended version) (2021)","DOI":"10.1007\/978-3-031-19756-7_7"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"Hugues, J.: A correct-by-construction AADL runtime for the Ravenscar profile using SPARK2014. J. Syst. Archit., 102376 (2022). https:\/\/www.sciencedirect.com\/science\/article\/pii\/S1383762121002599","DOI":"10.1016\/j.sysarc.2021.102376"},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"Hugues, J., Zalila, B., Pautet, L., Kordon, F.: Rapid prototyping of distributed real-time embedded systems using the AADL and Ocarina. In: IEEE International Workshop on Rapid System Prototyping, vol. 7 (2007)","DOI":"10.1145\/1376804.1376810"},{"key":"7_CR21","unstructured":"SAE International: SAE AS5506\/1, AADL Annex E: Error Model Annex. SAE International (2015). http:\/\/www.sae.org"},{"key":"7_CR22","unstructured":"SAE International: SAE AS5506 Rev. C Architecture Analysis and Design Language (AADL). SAE International (2017)"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"Klein, G., et al.: seL4: formal verification of an OS kernel. In: Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, pp. 207\u2013220 (2009)","DOI":"10.1145\/1629575.1629596"},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"Larson, B., Hatcliff, J., Fowler, K., Delange, J.: Illustrating the AADL error modeling annex (v.2) using a simple safety-critical medical device. In: Proceedings of the 2013 ACM SIGAda Annual Conference on High Integrity Language Technology, HILT 2013, pp. 65\u201384. ACM, New York (2013)","DOI":"10.1145\/2527269.2527271"},{"key":"7_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/978-3-642-38088-4_19","volume-title":"NASA Formal Methods","author":"BR Larson","year":"2013","unstructured":"Larson, B.R., Chalin, P., Hatcliff, J.: BLESS: formal specification and verification of behaviors for embedded systems with software. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 276\u2013290. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38088-4_19"},{"key":"7_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-642-01924-1_17","volume-title":"Reliable Software Technologies \u2013 Ada-Europe 2009","author":"G Lasnier","year":"2009","unstructured":"Lasnier, G., Zalila, B., Pautet, L., Hugues, J.: Ocarina: an environment for AADL models analysis and automatic code generation for high integrity applications. In: Kordon, F., Kermarrec, Y. (eds.) Ada-Europe 2009. LNCS, vol. 5570, pp. 237\u2013250. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-01924-1_17"},{"key":"7_CR27","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-540-74107-7_8","volume-title":"Logics of Specification Languages","author":"S Merz","year":"2008","unstructured":"Merz, S.: The specification language TLA+. In: Bj\u00f8rner, D., Henson, M.C. (eds.) Logics of Specification Languages, pp. 401\u2013451. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-74107-7_8"},{"issue":"2","key":"7_CR28","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/s10009-019-00513-7","volume":"22","author":"H Mkaouar","year":"2019","unstructured":"Mkaouar, H., Zalila, B., Hugues, J., Jmaiel, M.: A formal approach to AADL model-based software engineering. Int. J. Softw. Tools Technol. Transf. 22(2), 219\u2013247 (2019). https:\/\/doi.org\/10.1007\/s10009-019-00513-7","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"7_CR29","doi-asserted-by":"crossref","unstructured":"Perrotin, M., Conquet, E., Delange, J., Schiele, A., Tsiodras, T.: TASTE: a real-time software engineering tool-chain overview, status, and future, pp. 26\u201337, January 2011","DOI":"10.1007\/978-3-642-25264-8_4"},{"key":"7_CR30","doi-asserted-by":"publisher","unstructured":"Robby, Hatcliff, J.: Slang: the Sireum programming language. In: Margaria, T., Steffen, B. (eds.) ISoLA 2021. LNCS, vol. 13036, pp. 253\u2013273. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-89159-6_17","DOI":"10.1007\/978-3-030-89159-6_17"},{"key":"7_CR31","unstructured":"Rolland, J.F., Bodeveix, J.P., Chemouil, D., Filali, M., Thomas, D.: Towards a formal semantics for AADL execution model. In: Embedded Real Time Software and Systems (ERTS 2008) (2008)"},{"key":"7_CR32","doi-asserted-by":"crossref","unstructured":"Sokolsky, O., Lee, I., Clarke, D.: Schedulability analysis of AADL models. In: Proceedings 20th IEEE International Parallel and Distributed Processing Symposium, p. 8. IEEE (2006)","DOI":"10.1109\/IPDPS.2006.1639421"},{"key":"7_CR33","doi-asserted-by":"publisher","DOI":"10.1016\/j.ress.2021.107649","volume":"213","author":"D Stewart","year":"2021","unstructured":"Stewart, D., Liu, J.J., Cofer, D., Heimdahl, M., Whalen, M.W., Peterson, M.: AADL-based safety analysis using formal methods applied to aircraft digital systems. Reliab. Eng. Syst. Saf. 213, 107649 (2021)","journal-title":"Reliab. Eng. Syst. Saf."},{"key":"7_CR34","unstructured":"Stewart, D., Liu, J.J., Whalen, M., Cofer, D., Peterson, M.: Safety annex for architecture analysis design and analysis language. In: ERTS 2020: 10th European Conference Embedded Real Time Systems (2020)"},{"key":"7_CR35","doi-asserted-by":"crossref","unstructured":"Tan, Y., Zhao, Y., Ma, D., Zhang, X.: A comprehensive formalization of AADL with behavior annex. Sci. Program. 2022 (2022)","DOI":"10.1155\/2022\/2079880"},{"key":"7_CR36","doi-asserted-by":"crossref","unstructured":"VanderLeest, S.H.: ARINC 653 hypervisor. In: 29th Digital Avionics Systems Conference, pp. 5-E. IEEE (2010)","DOI":"10.1109\/DASC.2010.5655298"},{"key":"7_CR37","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1016\/j.jss.2014.02.058","volume":"93","author":"Z Yang","year":"2014","unstructured":"Yang, Z., Hu, K., Ma, D., Bodeveix, J.P., Pi, L., Talpin, J.P.: From AADL to timed abstract state machines: a verified model transformation. J. Syst. Softw. 93, 42\u201368 (2014)","journal-title":"J. Syst. Softw."},{"key":"7_CR38","doi-asserted-by":"publisher","unstructured":"Yuan, C., Wu, K., Chen, G., Mo, Y.: An automatic transformation method from AADL reliability model to CTMC. In: 2021 IEEE International Conference on Information Communication and Software Engineering (ICICSE), pp. 322\u2013326 (2021). https:\/\/doi.org\/10.1109\/ICICSE52190.2021.9404135","DOI":"10.1109\/ICICSE52190.2021.9404135"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-19756-7_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,4]],"date-time":"2023-04-04T20:05:27Z","timestamp":1680638727000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-19756-7_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031197550","9783031197567"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-19756-7_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"17 October 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Leveraging Applications of Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rhodes","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 October 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 October 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isola2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.isola-conference.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}