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)
|
Example Screen Capture
of the Graphical and
Disciplined English Views
|
Selected Publications
[an error occurred while processing this directive]
This site is maintained by the