{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,15]],"date-time":"2026-02-15T08:51:25Z","timestamp":1771145485465,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642380877","type":"print"},{"value":"9783642380884","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38088-4_19","type":"book-chapter","created":{"date-parts":[[2013,5,8]],"date-time":"2013-05-08T20:38:27Z","timestamp":1368045507000},"page":"276-290","source":"Crossref","is-referenced-by-count":38,"title":["BLESS: Formal Specification and Verification of Behaviors for Embedded Systems with Software"],"prefix":"10.1007","author":[{"given":"Brian R.","family":"Larson","sequence":"first","affiliation":[]},{"given":"Patrice","family":"Chalin","sequence":"additional","affiliation":[]},{"given":"John","family":"Hatcliff","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"19_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-book: assigning programs to meanings","author":"J.-R. Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B-book: assigning programs to meanings. Cambridge University Press, New York (1996)"},{"key":"19_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"J.-R. Abrial","year":"2010","unstructured":"Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, New York (2010)"},{"issue":"6","key":"19_CR3","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"J.-R. Abrial","year":"2010","unstructured":"Abrial, J.-R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transf.\u00a012(6), 447\u2013466 (2010)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"19_CR4","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/s10270-004-0058-x","volume":"4","author":"W. Ahrendt","year":"2005","unstructured":"Ahrendt, W., Baar, T., Beckert, B., Bubel, R., Giese, M., H\u00e4hnle, R., Menzel, W., Mostowski, W., Roth, A., Schlager, S., Schmitt, P.H.: The KeY tool. Software and Systems Modeling\u00a04, 32\u201354 (2005)","journal-title":"Software and Systems Modeling"},{"key":"19_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"key":"19_CR6","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Verification of Object-Oriented Software. The KeY Approach","year":"2007","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol.\u00a04334. Springer, Heidelberg (2007)"},{"key":"19_CR7","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.\u00a05570, pp. 207\u2013221. Springer, Heidelberg (2009)"},{"issue":"3","key":"19_CR8","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","volume":"7","author":"L. Burdy","year":"2005","unstructured":"Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. Journal on Software Tools for Technology Transfer (STTT)\u00a07(3), 212\u2013232 (2005)","journal-title":"Journal on Software Tools for Technology Transfer (STTT)"},{"key":"19_CR9","unstructured":"Feiler, P.H., Hansson, J., de Niz, D., Wrage, L.: System architecture virtual integration: An industrial case study. Technical Report CMU\/SEI-2009-TR-017 (2009)"},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"Hatcliff, J., King, A., Lee, I., Fernandez, A., Goldman, J., McDonald, A., Robkin, M., Vasserman, E., Weininger, S.: Rationale and architecture principles for medical application platforms. In: Proceedings of the 2012 International Conference on Cyberphysical Systems (2012)","DOI":"10.1109\/ICCPS.2012.9"},{"issue":"3","key":"19_CR11","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2187671.2187678","volume":"44","author":"J. Hatcliff","year":"2012","unstructured":"Hatcliff, J., Leavens, G.T., Leino, K.R.M., M\u00fcller, P., Parkinson, M.: Behavioral interface specification languages. ACM Comput. Surv. 44(3), 16:1\u201316:58 (2012)","journal-title":"ACM Comput. Surv."},{"key":"19_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"833","DOI":"10.1007\/978-3-642-04772-5_107","volume-title":"Computer Aided Systems Theory - EUROCAST 2009","author":"V. Januzaj","year":"2009","unstructured":"Januzaj, V., Mauersberger, R., Biechele, F.: Performance modelling for avionics systems. In: Moreno-D\u00edaz, R., Pichler, F., Quesada-Arencibia, A. (eds.) EUROCAST 2009. LNCS, vol.\u00a05717, pp. 833\u2013840. Springer, Heidelberg (2009)"},{"key":"19_CR13","unstructured":"Larson, B.R.: Behavior Language for Embedded Systems with Software Annex Sublanguage for AADL (2012), Available at [24]"},{"key":"19_CR14","unstructured":"Larson, B.R., Chalin, P., Hatcliff, J.: BLESS: Formal specification and verification of behaviors for embedded systems with software. Technical Report SAnToS 2012-12-01, Kansas State University, Computing and Information Sc. Dept. (2012), Available at [24]"},{"key":"19_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/978-3-642-30885-7_17","volume-title":"Abstract State Machines, Alloy, B, VDM, and Z","author":"D. Mentr\u00e9","year":"2012","unstructured":"Mentr\u00e9, D., March\u00e9, C., Filli\u00e2tre, J.-C., Asuka, M.: Discharging proof obligations from Atelier B using multiple automated provers. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol.\u00a07316, pp. 238\u2013251. Springer, Heidelberg (2012)"},{"key":"19_CR16","volume-title":"Proceedings of the Workshop on Industrial Strength Formal Specification Techniques (WIFT)","author":"E. Mikk","year":"1998","unstructured":"Mikk, E., Lakhnech, Y., Siegel, M., Holzmann, G.J.: Implementing Statecharts in PROMELA\/SPIN. In: Proceedings of the Workshop on Industrial Strength Formal Specification Techniques (WIFT). IEEE Computer Society, Washington, DC (1998)"},{"key":"19_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-642-13464-7_5","volume-title":"Formal Techniques for Distributed Systems","author":"P.C. \u00d6lveczky","year":"2010","unstructured":"\u00d6lveczky, P.C., Boronat, A., Meseguer, J.: Formal semantics and analysis of behavioral AADL models in Real-Time Maude. In: Hatcliff, J., Zucca, E. (eds.) FMOODS\/FORTE 2010. LNCS, vol.\u00a06117, pp. 47\u201362. Springer, Heidelberg (2010)"},{"key":"19_CR18","unstructured":"Osate 2 web site (2012), \n                    \n                      wiki.sei.cmu.edu\/aadl\/index.php\/Osate_2"},{"key":"19_CR19","unstructured":"SAE International. SAE AS5506A. Architecture Analysis & Design Language (AADL) (2009)"},{"key":"19_CR20","unstructured":"SAE International. SAE AS5506\/2. Architecture Analysis & Design Language (AADL) Annex, vol. 2 (2011)"},{"key":"19_CR21","unstructured":"Boston Scientific. Pacemaker system specification (2007), \n                    \n                      sqrl.mcmaster.ca\/pacemaker.html"},{"key":"19_CR22","unstructured":"Thums, A., Balser, M.: Interactive verification of statecharts. Integration of Software Spec. Tech. (INT) (2002)"},{"key":"19_CR23","unstructured":"System Architecture Virtual Integration (SAVI) Initiative (2012), \n                    \n                      wiki.sei.cmu.edu\/aadl\/index.php\/Projects_and_Initiatives"},{"key":"19_CR24","unstructured":"SAnToS TR 2012-12-01 web site, \n                    \n                      info.santoslab.org\/research\/aadl\/bless"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38088-4_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,12]],"date-time":"2019-05-12T19:49:06Z","timestamp":1557690546000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38088-4_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642380877","9783642380884"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38088-4_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}