SEI Component Formal Reasoning Technology (ComFoRT) Reasoning Framework 2.0 Available
Version 2.0 of ComFoRT is an Eclipse-based integrated development environment (IDE), which includes a syntax highlighting editor, a counterexample viewer, and integrated help and tutorials to simplify use.
What is ComFoRT? (From the SEI Site)
The Component Formal Reasoning Technology (ComFoRT) is a reasoning framework for predicting whether a system will satisfy its safety, reliability, and security requirements. In ComFoRT, these requirements are encoded as behavioral assertions that are verified automatically.
To determine whether these assertions hold for a system, ComFoRT uses model checking technology—a collection of algorithms that verify whether a model of a system satisfies such assertions in all possible executions. The exhaustive nature of model checking provides a higher degree of confidence than is typically possible using conventional testing-based approaches. Moreover, whenever an assertion fails to hold, a counterexample is generated that details an execution trace violating the assertion.
ComFoRT can be applied to different development artifacts and is intended for use with a development approach that is based on prediction-enabled component technology (PECT).
Our current focus is on application to design specifications expressed in CCL. CCL specifications capture structural information such as component topologies and arbitrarily detailed descriptions of component behavior that are expressed in a subset of UML statechart notation. However, the Copper model checker used in ComFoRT also permits application to a restricted form of C source code.
What is ComFoRT? (From the SEI Site)
The Component Formal Reasoning Technology (ComFoRT) is a reasoning framework for predicting whether a system will satisfy its safety, reliability, and security requirements. In ComFoRT, these requirements are encoded as behavioral assertions that are verified automatically.
To determine whether these assertions hold for a system, ComFoRT uses model checking technology—a collection of algorithms that verify whether a model of a system satisfies such assertions in all possible executions. The exhaustive nature of model checking provides a higher degree of confidence than is typically possible using conventional testing-based approaches. Moreover, whenever an assertion fails to hold, a counterexample is generated that details an execution trace violating the assertion.
ComFoRT can be applied to different development artifacts and is intended for use with a development approach that is based on prediction-enabled component technology (PECT).
Our current focus is on application to design specifications expressed in CCL. CCL specifications capture structural information such as component topologies and arbitrarily detailed descriptions of component behavior that are expressed in a subset of UML statechart notation. However, the Copper model checker used in ComFoRT also permits application to a restricted form of C source code.
This flexibility facilitates analysis at different stages of development:
- verification of early design decisions that are difficult to change late in the development process; for example, gross system coordination policies
- verification of whether detailed design specifications satisfy requirements prior to component implementation or generation
- assessment of whether acquired components are compatible with the existing system design or already implemented components
Learn more about ComFoRT (From the SEI Site)
A short overview of ComFoRT
A more thorough description of ComFoRT
_
posted by tadanderson at 11:12 AM
0 Comments:
Post a Comment
<< Home