John Hatcliff

Overview

The SAnToS Isolette Artifacts provide an end-to-end example of model-based development with integrated formal methods.

The Isolette system is based on requirements and design introduced in the FAA Requirements Engineering Management Handbook (note that Appendix A contains a summary of Isolette requirements).

The available artifacts include:

  • System use cases formalized using the use case map notation in the JUCMNav tool.
  • Natural langauge requirements and informal designs.
  • Formal system architecture specifications in the AADL and SysMLv2 modeling languages.
  • Developer-friendly component behavioral specifications integrated with system models using the GUMBO contract language.
  • Automated code generation in Slang (a safety-critical subset of Scala) and C, integrated with run-time libraries for threading and communication compliant with the AADL standard.
  • Slang component implementations with integrated behavioral contracts. Slang code is verified to conform to the contracts (auto-generated from the GUMBO model-level contracts) using the Logika verification tool.
  • Conventional unit tests and automated property-based testing against executable contracts automatically derived from GUMBO model-level contracts.

The Isolette Artifacts have been used in graduate courses on software engineering and formal verification as well as in industry training materials. The artifacts are publicly available in a github repository. See the Artifacts page for an overview, then subsequent detailed summaries.

A variety of pedogical materials are available including lecture slides, lecture videos, tutorials, and suggested assignments/projects.

To refer to this work, please cite the following paper, which provides goals, rationale, and an overview of the artifacts:

John Hatcliff, Jason Belt. “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