A primary goal of the Open PCA Pump project is to provide realistic system development that are aligned and provide traceability across the development cycle.

Several important artifacts (in particular the presentation of use cases and requirements) were inspired by the FAA Requirements Engineering Management Handbook (REMH).

The following artifacts are currently available.

System Overview and Operational Concepts

The System Overview provides an high-level description of the pump device, its medical purpose, the care-giving context into which it is deployed, and its interactions with people and equipment in the context. The Operational Concepts presents detailed use cases and exception cases, derived from stakeholders’ interests and goals, following the methodology presented in the FAA’s REMH. The use cases describe normal operation in the different usage modes supported by the pump. Exception cases describe response to hazards or other deviations from expected operation.

Both use and exception cases were developed as use case maps – graphical depictions of use case actions, actors, and branches – using jUCMNav. Textual use and exception cases correspond to their use case maps.

To facilitate cross-referencing in Latex sources of the Systems Overview, Operational Concepts, and Requirements, these artifacts are all presented in the same file (see the PDF file linked below in the Requirements section).


The OpenPCA Pump Requirements provide an express the infusion functionality, information input/output over the operator interface (including alarm notifications), validation and safeguards of user-entered infusion settings, functionality of risk controls for system faults and exceptional circumstances.

  • Open PCA Pump System Overview, Use Cases, and Requirements (pdf)

Formal Architecture Specification with Behavior Contracts

The archiecture specification provides a hierarchical decomposition of subsystems and components into smaller, simpler components that interact solely through well-defined interfaces.
The OpenPCA Pump Project adopts a architecture-model-centric approach to critical system development and assurance that emphasizes the use of formally specified architectures as the ``scaffolding’’ through which many different development artifacts and activities are organized and synchronized. For example, the use-cases in the ConOps document present system interactions with users and its environment in terms of interaction points that are modeled in the architecture. The system requirements are allocated to components in the high-level, functional architecture model. Architecturally-oriented requirements, such as independence of the Open PCA Pump infusion control system and safety subsystem, are reflected in the architecture model.

Due its central role in linking the various artifacts, it’s crucial that the chosen architecture modeling framework provides a strong semantic interpretation for the modeling elements. For example, the architecture modeling language needs to adhere to a semantics for threading and inter-component communication to enable behavioral annotations such as the BLESS interface contracts and hazard analyses to have an interpretation that is correct with respect to the code that is generated from the architecture models. Moreover, the architecture language needs to include model elements representing common features of embedded systems including real-time threading that can be analyzed at the model level for schedulability and latency, non-blocking communication between components, and binding of logical software to physical processors and communication buses.

AADL was chosen as the architecture modeling language for the Open PCA Pump because it provides the capabilities described above, and because it’s annex mechanism allows extension of the language to support different forms of analysis and verification of embedded systems.

  • Open PCA Pump AADL Architecture Specification (zip)

Architecture-aligned Behavioral Specifications

Component requirements are refined to formal interface behavioral specifications in BLESS that are included the architecture model, and component behaviors are specified using BLESS state-transition machines.

BLESS specifications are included in the AADL architecture artifacts above.

Assurance Case

The OpenPCA Pump assurance case is presented using the NOR-STA assurance case tool.
The assurance case provides a structured argument that the system implementation performs the intended function defined by its requirements with acceptable safety. In the medical domain, as in other safety- and security-critical domains, manufacturers need to present evidence to certification bodies and/or regulatory agencies that their products meet their specifications and are safe and secure. Assurance cases are increasing being used as a means to convey to stakeholders outside the manufacturering organization the claims that are being made about a product’s functional, safety, and security properties along with the evidence that supports those claims.

Industry engineers can use the assurance case to understand how to develop an assurance case for a realistic product and link it to other development artifacts. Researchers can use the assurance as an example for comparing different assurance notations and techniques for providing semi-automated audits of assurance cases.

  • Open PCA Pump Assurance Case (pdf)