Home > Static Analysis > Propel
Static Analysis
FLAVERS
PROPEL »
Finite-State Verification
Property Specification
Fault-Tree Analysis
Failure Mode and Effect Analysis
MPI Verification
INCA
Experimentation
Publications
Additional Information
All PROPEL Publications
Licensed Software
Related Research
A Specification Pattern System

Propel

One aspect of Requirements Engineering (RE) involves describing important properties about a software system. Such properties are often described with English phrases, such as:

Between the time an elevator is called at a floor and the time it opens its doors at that floor, the elevator can arrive at that floor at most twice.

Since English is often imprecise and ambiguous, these phrases are often imprecise and ambiguous. As an alternative, mathematical formalisms such as temporal logic have been proposed, but these are difficult even for experts to write and understand. For instance, the example above would be represented in Linear Time Logic as:

[]((call ⋀ <>open) →
   ((¬atfloor ⋀ ¬open) ⋃
      (open ⋁ ((atfloor ⋀ ¬open) ⋃
          (open ⋁ ((atfloor ⋀ ¬open) ⋃
             (open ⋁ ((atfloor ⋀ ¬open) ⋃
                (open ⋁ (¬atfloor ⋃ open))))))))))

No matter what notation is used, however, there are often subtle, but important, details that need to be considered.

The Propel approach provides templates that explicitly capture these details for property patterns that commonly occur in the properties that are created for model checking and other types of analysis. With Propel, users are shown the evolving property specification in both "disciplined" English sentences and graphical finite-state automata (FSA), allowing the specifier to easily move between these two views as they develop their properties.

Toolset Features

  • Property templates for some of the most commonly-occurring properties
  • Multiple views of the developing property, including graphical and textual views
  • User guidance through posing questions about the desired property
  • Support for organizing multiple properties in a single project
  • Summary views from multiple perspectives on the project structure
  • Support for exporting property FSAs

Available Property Views

  • Graphical View — an extended Finite State Automata (FSA) notation
  • Disciplined English View — a restricted subset of English
  • Question Tree View — an interactive question-answering view
  • Scope Timeline View — a graphical time interval view
  • Planned for the Future:
    • Linear Temporal Logic (LTL)
    • Computation Tree Logic (CTL)


Screen Shot
Example Screen Capture of the Graphical and
Disciplined English Views

Selected Publications

 2006

User Guidance for Creating Precise and Accessible Property Specifications
Rachel L. Cobleigh, George S. Avrunin, Lori A. Clarke, ACM SIGSOFT 14th International Symposium on Foundations of Software Engineering (FSE14), Portland, OR, pp. 208-218, November 2006. (UM-CS-2006-27)

This is an updated version originally dated April 2006.

[ ACM ] [ PDF ] [ Slides ]

 2003

From Natural Language Requirements to Rigorous Property Specifications
Rachel L. Smith, George S. Avrunin, Lori A. Clarke, Monterey Workshop 2003 (Workshop on Software Engineering for Embedded Systems (SEES 2003) From Requirements to Implementation, Chicago, IL, pp. 40-46, September 2003 . (UM-CS-2004-019)

[ PDF ] [ Slides ]

 2002

PROPEL: An Approach Supporting Property Elucidation
Rachel L. Smith, George S. Avrunin, Lori A. Clarke, Leon J. Osterweil, 24th International Conference on Software Engineering (ICSE 2002), Orlando, FL, pp. 11-21, May 2002. (UM-CS-2001-046)

[ PostScript ] [ PDF ]

 

This site is maintained by the Laboratory for Advanced Software Engineering Research.
© 2006 University of Massachusetts AmherstSite Policies