Rigorous Specification: Methods and Tools

Economical production of highly dependable software requires defect prevention via mathematically rigorous specification methods. The methods must be both constructive and accessible. Systematic, constructive engineering methods prevent defects through production of

  • Consistent and complete requirements,
  • Correct specifications based on traceability to those requirements, and
  • Software generated directly from correct specifications.

To enable and encourage widespread use, the methods must be easily applied by both software engineers and domain experts. This web site describes methods and supporting tools that enable routine practical production of high assurance software for mission critical applications.

Methods

Tools

Sequence Based Specification

The basic SBS process involves four steps:

  1. System boundary and interface definition,
  2. Itemizing stimuli and responses,
  3. Sequence enumeration,
  4. State machine construction.

See this tutorial for details.

REAL

REAL provides a GUI interface to describe/create a sequence-based specification in tabular format, save/read specifications to/from disk, analyze canonical sequences, and generate state box specifications based on the sequence enumeration.

The major components of a sequence based Specification (stimuli, responses, etc.) are all edited on separate tabs in the editor. Details are provided in the REAL User Guide.

 

 

 

 

 

 

 

 

 

 

 

 
 

 

 

 

This Web Page Created with PageBreeze Free HTML Editor