Overview

The SAnToS Lab Open PCA Pump Artifacts provide an end-to-end example of model-based development (with integrated formal methods) of the software for an “at scale” medical device.

The artifacts were developed in cooperation with US FDA and medical device industry engineers to illustrate best practices in rigorous engineering for medical devices.

The artifacts include operational concepts (formal use cases), requirements, formal architecture models, formal behavioral contracts in models and code, testing and formal verification, and an assurance case.

Formal specifications and verification tools/concepts illustrated include:

• formal use cases in the jUCMNav tool
• formal architectural models in AADL
• verified behavioral specifications in BLESS
• component contracts in the GUMBO contract language
• model-based code generation using the HAMR model-driven development tool
• verification of code to contracts in Slang/Logika
• randomized property-based testing against GUMBO contracts