{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,17]],"date-time":"2026-08-17T15:02:04Z","timestamp":1786978924553,"version":"build-2736575974"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031738869","type":"print"},{"value":"9783031738876","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T00:00:00Z","timestamp":1729641600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T00:00:00Z","timestamp":1729641600000},"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":[[2025]]},"DOI":"10.1007\/978-3-031-73887-6_9","type":"book-chapter","created":{"date-parts":[[2024,10,22]],"date-time":"2024-10-22T19:02:38Z","timestamp":1729623758000},"page":"93-117","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["The Isolette System: Illustrating End-to-End Artifacts for Rigorous Model-Based Engineering"],"prefix":"10.1007","author":[{"given":"John","family":"Hatcliff","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jason","family":"Belt","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,10,23]]},"reference":[{"key":"9_CR1","unstructured":"Amyot, D.: Jucmnav - eclipse plugin for the user requirements notation (2018). http:\/\/jucmnav.softwareengineering.ca\/foswiki\/ProjetSEG\/WebHome"},{"key":"9_CR2","doi-asserted-by":"publisher","unstructured":"Amyot, D., Mussbacher, G.: User requirements notation: the first ten years, the next ten years (invited paper). J. Softw. 6, 747\u2013768 (2011). https:\/\/doi.org\/10.4304\/jsw.6.5.747-768","DOI":"10.4304\/jsw.6.5.747-768"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Bakera, M., Margaria, T., Renner, C., Steffen, B.: Tool-supported enhancement of diagnosis in model-driven verification. Innov. Syst. Softw. Eng. 5, 211\u2013228 (2009)","DOI":"10.1007\/s11334-009-0091-6"},{"key":"9_CR4","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et al.: CVC5: a versatile and industrial-strength SMT solver. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2022. LNCS, vol. 13243, pp. 415\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"9_CR5","doi-asserted-by":"publisher","unstructured":"Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) Computer Aided Verification. CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Berlin, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"9_CR6","unstructured":"Braun, V., Margaria, T., Steffen, B., Bruhns, F.: Service definition for intelligent networks: experience in a leading-edge technological project based on constraint techniques. In: Wallace, M. (ed.) Proceedings of the Third International Conference on the Practical Application of Constraint Technology, PACT 1997, Westminster Central Hall, London, UK, 23\u201325 April 1997, pp. 91\u2013106. Practical Application Company Ltd. (1997)"},{"key":"9_CR7","doi-asserted-by":"publisher","unstructured":"Breathnach, C., Ibrahim, N.M., Clancy, S., Margaria, T.: Towards model checking product lines in the digital humanities: an application to historical data. In: ter Beek, M., Fantechi, A., Semini, L. (eds.) From Software Engineering to Formal Methods and Tools, and Back. LNCS, vol. 11865, pp. 338\u2013364. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30985-5_20","DOI":"10.1007\/978-3-030-30985-5_20"},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"Burdy, L., et al.: An overview of JML tools and applications. Int. J. Softw. Tools Technol. Transf. 7(3), 212\u2013232 (2005)","DOI":"10.1007\/s10009-004-0167-4"},{"key":"9_CR9","volume-title":"Writing Effective Use Cases","author":"A Cockburn","year":"2001","unstructured":"Cockburn, A.: Writing Effective Use Cases. Addison-Wesley, Boston, MA (2001)"},{"key":"9_CR10","unstructured":"Conchon, S., Coquereau, A., Iguernlala, M., Mebsout, A.: Alt-ergo 2.2. In: SMT Workshop: International Workshop on Satisfiability Modulo Theories (2018)"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"Ericson\u00a0II, C.A.: Hazard Analysis Techniques for System Safety. John Wiley & Sons, Hoboken (2005)","DOI":"10.1002\/0471739421"},{"key":"9_CR12","doi-asserted-by":"publisher","unstructured":"Hallerstede, S., Hatcliff, J.: A mechanized semantics for component-based systems in the HAMR AADL runtime. In: Camara, J., Jongmans, S.S. (eds.) Formal Aspects of Component Software. FACS 2023. LNCS, vol. 14485, pp. 45\u201364. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-52183-6_3","DOI":"10.1007\/978-3-031-52183-6_3"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Hallerstede, S., Hatcliff, J., Robby: teaching with logika: conceiving and constructing correct software. In: Formal Methods Teaching Workshop (FMTEA 2024) (2024), to appear","DOI":"10.1007\/978-3-031-71379-8_7"},{"key":"9_CR14","unstructured":"HARDENS: high assurance rigorous digital engineering for nuclear safety (artifacts repository). https:\/\/github.com\/GaloisInc\/HARDENS"},{"key":"9_CR15","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.) Leveraging Applications of Formal Methods, Verification and Validation. 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":"9_CR16","doi-asserted-by":"publisher","unstructured":"Hatcliff, J., Belt, J., Robby, Hardin, D.: Integrated contract-based unit and system testing for component-based systems. In: Benz, N., Gopinath, D., Shi, N. (eds.) NASA Formal Methods. NFM 2024. LNCS, vol. 14627, pp. 406\u2013426. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-60698-4_25","DOI":"10.1007\/978-3-031-60698-4_25"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Hatcliff, J., Belt, J., Robby, Legg, J., Stewart, D., Carpenter, T.: Automated property-based testing from AADL component contracts. In: Cimatti, A., Titolo, L. (eds.) Formal Methods for Industrial Critical Systems (2023)","DOI":"10.1007\/978-3-031-43681-9_8"},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"Hatcliff, J., Belt, J., Robby, Legg, J., Stewart, D., Carpenter, T.: Automated property-based testing from AADL component contracts. Submitted for journal publication. (2024)","DOI":"10.1007\/978-3-031-43681-9_8"},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Hatcliff, J., Hugues, J., Stewart, D., Wrage, L.: Formalization of the AADL run-time services. In: Leveraging Applications of Formal Methods, Verification and Validation - 11th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2022, Rhodes, Greece (2022)","DOI":"10.1007\/978-3-031-19756-7_7"},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"Hatcliff, J., Larson, B.R., Carpenter, T., Jones, P.L., Zhang, Y., Jorgens, J.: The open PCA pump project: an exemplar open source medical device as a community resource. SIGBED Rev. 16(2), 8\u201313 (2019)","DOI":"10.1145\/3357495.3357496"},{"key":"9_CR21","unstructured":"Hatcliff, J., Stewart, D., Belt, J., Robby, Schwerdfeger, A.: An AADL contract language supporting integrated model- and code-level verification. In: Proceedings of the 2022 ACM Workshop on High Integrity Language Technology. HILT \u201922 (2022)"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Hatcliff, J., Vasserman, E.Y., Carpenter, T., Whillock, R.: Challenges of distributed risk management for medical application platforms. In: 2018 IEEE Symposium on Product Compliance Engineering (ISPCE), pp. 1\u201314 (2018)","DOI":"10.1109\/ISPCE.2018.8379270"},{"key":"9_CR23","doi-asserted-by":"publisher","unstructured":"Hatcliff, J., Wassyng, A., Kelly, T., Comar, C., Jones, P.L.: Certifiably safe software-dependent systems: challenges and directions. In: Proceedings of the on Future of Software Engineering (ICSE FOSE), pp. 182\u2013200 (2014). https:\/\/doi.org\/10.1145\/2593882.2593895","DOI":"10.1145\/2593882.2593895"},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"Hatcliff, J., Zhang, Y., Goldman, J.M.: Risk management objectives for distributed development of interoperable medical products. In: 2019 IEEE Symposium on Product Compliance Engineering (SPCE Austin), pp.\u00a01\u20136 (2019)","DOI":"10.1109\/SPCE47297.2019.8950764"},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"J\u00f6rges, S., Lamprecht, A.L., Margaria, T., Schaefer, I., Steffen, B.: A constraint-based variability modeling framework. Int. J. Softw. Tools Technol. Transf. 14 (2012)","DOI":"10.1007\/s10009-012-0254-x"},{"key":"9_CR26","doi-asserted-by":"crossref","unstructured":"Lattuada, A., et al.: Verus: verifying Rust programs using linear ghost types. Proc. ACM Program. Lang. 7(OOPSLA1), 286\u2013315 (2023)","DOI":"10.1145\/3586037"},{"key":"9_CR27","unstructured":"Lempia, D., Miller, S.: DOT\/FAA\/AR-08\/32. Requirements engineering management handbook. Federal Aviation Administration (2009)"},{"key":"9_CR28","doi-asserted-by":"crossref","unstructured":"Leveson, N.G.: Engineering a Safer World: Systems Thinking Applied to Safety. Engineering Systems, The MIT Press, Cambridge (2012)","DOI":"10.7551\/mitpress\/8179.001.0001"},{"key":"9_CR29","unstructured":"Sireum logika (2022). https:\/\/logika.sireum.org"},{"key":"9_CR30","doi-asserted-by":"publisher","unstructured":"Margaria, T., Meyer, D., Kubczak, C., Isberner, M., Steffen, B.: Synthesizing semantic web service compositions with jMosel and Golog. In: Bernstein, A., et al. (eds.) The Semantic Web - ISWC 2009. ISWC 2009. LNCS, vol. 5823, pp. 392\u2013407. Springer, Berlin, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04930-9_25","DOI":"10.1007\/978-3-642-04930-9_25"},{"key":"9_CR31","doi-asserted-by":"crossref","unstructured":"Margaria, T., Steffen, B.: Chapter i business process modelling in the jabc: the one-thing-approach. In: Handbook of Research on Business Process Modeling, January 2009","DOI":"10.4018\/978-1-60566-288-6.ch001"},{"key":"9_CR32","doi-asserted-by":"publisher","unstructured":"de Moura, L., Bjorner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Berlin, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9_CR33","doi-asserted-by":"crossref","unstructured":"Niese, O., Steffen, B., Margaria, T., Hagerer, A., Brune, G., Ide, H.D.: Library-based design and consistency checking of system-level industrial test cases. In: Fundamental Approaches to Software Engineering, pp. 233\u2013248, April 2001","DOI":"10.1007\/3-540-45314-8_17"},{"key":"9_CR34","doi-asserted-by":"publisher","unstructured":"Rasche, C., Margaria, T., Floyd, B.D.: Service model innovation in hospitals: beyond expert organizations. In: Pfannstiel, M., Rasche, C. (eds.) Service Business Model Innovation in Healthcare and Hospital Management, pp. 1\u201320. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-46412-1_1","DOI":"10.1007\/978-3-319-46412-1_1"},{"key":"9_CR35","doi-asserted-by":"publisher","unstructured":"Robby, Hatcliff, J.: Slang: the sireum programming language. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation. 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":"9_CR36","doi-asserted-by":"crossref","unstructured":"Robby, Hatcliff, J., Belt, J.: Logika: the sireum verification framework. In: Formal Methods for Industrial Critical Systems (FMICS 2024) (2024)","DOI":"10.1007\/978-3-031-68150-9_6"},{"key":"9_CR37","unstructured":"SAnToS Laboratory: HAMR\/HARDENS nuclear reactor trip system artifacts showcase (2024). https:\/\/github.com\/santoslab\/rts-showcase"},{"key":"9_CR38","unstructured":"SAnToS Laboratory: Isolette artifacts website \u2013 illustrating rigorous model-based development with integrated formal methods (2024). https:\/\/isolette.santoslab.org"},{"key":"9_CR39","unstructured":"SAnToS Laboratory: Open PCA Project website (2024). https:\/\/openpcapump.santoslab.org"},{"key":"9_CR40","unstructured":"Steffen, B., et al.: Language-driven engineering: an interdisciplinary software development paradigm (2024). (to appear)"},{"key":"9_CR41","unstructured":"Steffen, B., Margaria, T., Braun, V., Kalt, N.: Hierarchical service definition. Annu. Rev. Commun. 51, 847\u2013856 (1997)"},{"key":"9_CR42","doi-asserted-by":"publisher","unstructured":"Steffen, B., Margaria, T., Nagel, R., Jorges, S., Kubczak, C.: Model-driven development with the jABC. In: Bin, E., Ziv, A., Ur, S. (eds.) Hardware and Software, Verification and Testing. HVC 2006. LNCS, vol. 4383, pp. 92\u2013108. Springer, Berlin, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-70889-6_7","DOI":"10.1007\/978-3-540-70889-6_7"}],"container-title":["Lecture Notes in Computer Science","The Combined Power of Research, Education, and Dissemination"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-73887-6_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,30]],"date-time":"2025-01-30T06:15:25Z","timestamp":1738217725000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-73887-6_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,23]]},"ISBN":["9783031738869","9783031738876"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-73887-6_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,23]]},"assertion":[{"value":"23 October 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}