ComFoRT Reasoning Framework

What is ComFoRT?

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

To get ComFoRT, download the PACC Starter Kit

Feel free to email us at comfort-feedback [at] sei.cmu.edu with any questions or comments.