Overview
Using data flow analysis techniques, FLAVERS can very quickly compute
an approximate solution to a verification query. If the results are
inconclusive, we have developed an approach for incrementally and selectively
improving the precision until the property is proven or a counter example
is described. Thus, we have been exploring the hypothesis that with
fine grained control over precision and with a highly optimized program
model and data flow based reasoning engine, finite state verification
can be applied to large, complex distributed systems. The FLAVERS prototype
has successfully been used on some industrial demonstration projects
and is currently being extended to evaluate Java programs.
FLAVERS is a flexible, powerful system for automatically guaranteeing
the absence or detecting the presence of a wide range of user-specified
properties or behaviors in both sequential and concurrent systems.
FLAVERS complements traditional testing approaches, which only demonstrate
the presence or absence of errors for the specific test cases that
have been executed. It also complements formal verification methods,
which employ more comprehensive analysis, but require extensive expertise
on the part of the user.
FLAVERS is built using the FLAVERS toolkit, a flexible architecture
and component library that facilitates the development of FLAVERS analyzers.
The toolkit allows FLAVERS to be extended with additional specialized
data flow analyzers and to be applied to a wide range of languages
and systems. FLAVERS has been applied to the analysis of Ada and C++
and Java is underway. It has also been used for the analysis of network
protocols and architecture specifications.
Features
- User-definable properties and models
- Comprehensive API supports application to a wide range of domains
and languages
- Visualization tools aid in understanding concurrent system behavior
- FLAVERS analyses can improve the quality of a system throughout
its lifecycle
- During design to verify:
- that the architecture meets the requirements
- that the design is consistent with the architecture
- During testing to generalize test cases to all executions
- During debugging to:
- identify the cause of a fault
- confirm that the fault has been removed
Selected Publications
[an error occurred while processing this directive]
This site is maintained by the