Artifacts

The following summaries are excerpted and adapted from the descriptions in the overview paper.

Operational Concepts (Formal Use Cases)

Operational concepts (system use cases presented in the style of Cockburn’s “Writing Effective Use Cases”) are presented in the REMH to support system scoping, requirements elicitation, and initial system design.

The Isolette artifacts supplement the REMH presentation with formalizations of the use cases in the jUCMNav use case modeling tool.

To edit/view the JUCMNAV artifacts, you need to have the JUCMNAV Eclpse plug-in installed (installation instructions). However, here is sneak peek at screen shots of the uses cases from the artifacts repo.

Requirements

The Isolette requirements are the heart of the content inherited from the REMH – system and component natural language requirements that are subsequently refined to other artifacts including formal specifications and formal architecture models in subsequent sections.

Formal Architecture Specification with Behavior Contracts

The informal designs from the REMH are formalized in as AADL models.

To edit/view the AADL artifacts, you need to have the OSATE Eclpse plug-in installed (installation instructions).
However, here is sneak peek at textual models in the artifacts repo.

The AADL architecture specifications form the basis of subsequent code generation, application code development, and integrated contracts in subsequent sections.

Architecture-compliant Component Application Code

Testing of Component Application Code to Contracts

Verification Component Application Code to Contracts with Logika (developer friendly SMT-based verification)