[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

The Isolette System: Illustrating End-to-End Artifacts for Rigorous Model-Based Engineering

  • Chapter
  • First Online:
The Combined Power of Research, Education, and Dissemination

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 15240))

  • 63 Accesses

Abstract

Margaria and colleagues have emphasized a paradigm for system construction and assurance in which development is organized around building and refining one comprehensive model of the system (referred to as the “One Thing Approach” (OTA)). In this paper, we connect to several key OTA ideas by presenting an integrated collection of development artifacts for a simple safety-critical system (an Infant Incubator example called the Isolette). Our illustration uses AADL for defining system models, the HAMR model-driven development tool, the GUMBO model-based component contract language for specifying constraints, and the Slang/Logika framework for code-level automated property-based testing and verificationl. The artifacts illustrate a rigorous process, moving end-to-end from the concepts of operations and requirements to assurance cases and deployment on the formally verified seL4 microkernel. We describe pedagogical resources and tutorials that have been used to introduce both students and industry teams to formal-methods integrated with model based development.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
GBP 19.95
Price includes VAT (United Kingdom)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
GBP 49.99
Price includes VAT (United Kingdom)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
GBP 59.99
Price includes VAT (United Kingdom)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    The artifacts also include a version of system models in SysMLv2, as the AADL community is currently transitioning AADL concepts into SysMLv2 libraries to support future work within the AADL community.

  2. 2.

    These collaborations including teaming with Collins Aerospace and Galois on a number of US defense-related projects, including projects funded by DARPA, US Army, US Airforce, and US Department of Homeland Security.

  3. 3.

    As with any testing/code-level formal method, I/O and interactions with physical devices or stateful services may need to be supported by manually crafted stubs.

References

  1. Amyot, D.: Jucmnav - eclipse plugin for the user requirements notation (2018). http://jucmnav.softwareengineering.ca/foswiki/ProjetSEG/WebHome

  2. Amyot, D., Mussbacher, G.: User requirements notation: the first ten years, the next ten years (invited paper). J. Softw. 6, 747–768 (2011). https://doi.org/10.4304/jsw.6.5.747-768

  3. Bakera, M., Margaria, T., Renner, C., Steffen, B.: Tool-supported enhancement of diagnosis in model-driven verification. Innov. Syst. Softw. Eng. 5, 211–228 (2009)

    Google Scholar 

  4. 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–442. Springer, Cham (2022). https://doi.org/10.1007/978-3-030-99524-9_24

  5. Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) Computer Aided Verification. CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Berlin, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_14

  6. 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–25 April 1997, pp. 91–106. Practical Application Company Ltd. (1997)

    Google Scholar 

  7. 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–364. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30985-5_20

  8. Burdy, L., et al.: An overview of JML tools and applications. Int. J. Softw. Tools Technol. Transf. 7(3), 212–232 (2005)

    Google Scholar 

  9. Cockburn, A.: Writing Effective Use Cases. Addison-Wesley, Boston, MA (2001)

    Google Scholar 

  10. Conchon, S., Coquereau, A., Iguernlala, M., Mebsout, A.: Alt-ergo 2.2. In: SMT Workshop: International Workshop on Satisfiability Modulo Theories (2018)

    Google Scholar 

  11. Ericson II, C.A.: Hazard Analysis Techniques for System Safety. John Wiley & Sons, Hoboken (2005)

    Google Scholar 

  12. 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–64. Springer, Cham (2024). https://doi.org/10.1007/978-3-031-52183-6_3

  13. Hallerstede, S., Hatcliff, J., Robby: teaching with logika: conceiving and constructing correct software. In: Formal Methods Teaching Workshop (FMTEA 2024) (2024), to appear

    Google Scholar 

  14. HARDENS: high assurance rigorous digital engineering for nuclear safety (artifacts repository). https://github.com/GaloisInc/HARDENS

  15. 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–295. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-89159-6_18

  16. 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–426. Springer, Cham (2024). https://doi.org/10.1007/978-3-031-60698-4_25

  17. 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)

    Google Scholar 

  18. Hatcliff, J., Belt, J., Robby, Legg, J., Stewart, D., Carpenter, T.: Automated property-based testing from AADL component contracts. Submitted for journal publication. (2024)

    Google Scholar 

  19. 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)

    Google Scholar 

  20. 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–13 (2019)

    Google Scholar 

  21. 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 ’22 (2022)

    Google Scholar 

  22. 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–14 (2018)

    Google Scholar 

  23. 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–200 (2014). https://doi.org/10.1145/2593882.2593895

  24. 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. 1–6 (2019)

    Google Scholar 

  25. Jörges, S., Lamprecht, A.L., Margaria, T., Schaefer, I., Steffen, B.: A constraint-based variability modeling framework. Int. J. Softw. Tools Technol. Transf. 14 (2012)

    Google Scholar 

  26. Lattuada, A., et al.: Verus: verifying Rust programs using linear ghost types. Proc. ACM Program. Lang. 7(OOPSLA1), 286–315 (2023)

    Google Scholar 

  27. Lempia, D., Miller, S.: DOT/FAA/AR-08/32. Requirements engineering management handbook. Federal Aviation Administration (2009)

    Google Scholar 

  28. Leveson, N.G.: Engineering a Safer World: Systems Thinking Applied to Safety. Engineering Systems, The MIT Press, Cambridge (2012)

    Google Scholar 

  29. Sireum logika (2022). https://logika.sireum.org

  30. 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–407. Springer, Berlin, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04930-9_25

  31. 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

    Google Scholar 

  32. 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–340. Springer, Berlin, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24

  33. 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–248, April 2001

    Google Scholar 

  34. 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–20. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-46412-1_1

  35. 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–273. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-89159-6_17

  36. Robby, Hatcliff, J., Belt, J.: Logika: the sireum verification framework. In: Formal Methods for Industrial Critical Systems (FMICS 2024) (2024)

    Google Scholar 

  37. SAnToS Laboratory: HAMR/HARDENS nuclear reactor trip system artifacts showcase (2024). https://github.com/santoslab/rts-showcase

  38. SAnToS Laboratory: Isolette artifacts website – illustrating rigorous model-based development with integrated formal methods (2024). https://isolette.santoslab.org

  39. SAnToS Laboratory: Open PCA Project website (2024). https://openpcapump.santoslab.org

  40. Steffen, B., et al.: Language-driven engineering: an interdisciplinary software development paradigm (2024). (to appear)

    Google Scholar 

  41. Steffen, B., Margaria, T., Braun, V., Kalt, N.: Hierarchical service definition. Annu. Rev. Commun. 51, 847–856 (1997)

    Google Scholar 

  42. 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–108. Springer, Berlin, Heidelberg (2007). https://doi.org/10.1007/978-3-540-70889-6_7

Download references

Author information

Authors and Affiliations

  1. Kansas State University, Manhattan, KS, 66506, USA

    John Hatcliff & Jason Belt

Authors
  1. John Hatcliff
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jason Belt
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to John Hatcliff .

Editor information

Editors and Affiliations

  1. University of Limerick, Limerick, Ireland

    Mike Hinchey

  2. TU Dortmund, Dortmund, Germany

    Bernhard Steffen

Rights and permissions

Reprints and permissions

Copyright information

© 2025 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Hatcliff, J., Belt, J. (2025). The Isolette System: Illustrating End-to-End Artifacts for Rigorous Model-Based Engineering. In: Hinchey, M., Steffen, B. (eds) The Combined Power of Research, Education, and Dissemination. Lecture Notes in Computer Science, vol 15240. Springer, Cham. https://doi.org/10.1007/978-3-031-73887-6_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-73887-6_9

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-73886-9

  • Online ISBN: 978-3-031-73887-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation