ComFoRT: A Reasoning Framework
for Formal Analysis of Component-based Software

Project Overview. Component technologies are gaining acceptance in the software community as effective tools for quickly assembling increasingly complex systems from components. Most of the current component technologies, however, fail to help developers predict important software qualities like security, safety, and reliability. Model checking is an automated approach for exhaustively analyzing whether systems satisfy specific behavioral claims that can be used to characterize safety and reliability requirements. A Component Formal Reasoning Technology (ComFoRT) packages quality specific model checking analyses and the means to apply them to component-based systems.

The following concepts define the ComFoRT framework:


     Model Checking

     Automated Predicate Abstraction

     Automated Abstraction Refinement (also known as a CEGAR: CounterExample-Guided Abstraction Refinement loop)

     Compositional Reasoning

     Automated Component Substitutability Analysis

     Hybrid State/Event System Modeling and Specification (state/event LTL and ACTL)

     SAT-based Predicate Abstraction Loop

---

Publications.


1. The ComFoRT Overview:
      Overview of ComFoRT, A Model Checking Reasoning Framework
2. Overview of the ComFoRT abstraction and compositional reasoning techniques
- using decision procedures based on integer domain:
      Efficient Verification of Sequential and Concurrent C Programs
- using SAT solvers to treat bit-vector overflow and pointer arithmetic constructs:
      Predicate Abstraction of ANSI-C Programs using SAT
3. State/Event-based formalism for modeling both the data and communication aspects of software
      State/Event-based Software Model Checking
      An Expressive Verification Framework for State/Event Systems
      Automated, compositional and iterative deadlock detection
4. Component Substitutability Analysis
      Automated Component Substitutability Analysis


---

Tool support. The ComFoRT framework is being developed as part of the Predictable Assembly from Certifiable Components (PACC) initiative at CMU SEI. The model checking engine of ComFoRT is built on the top of the MAGIC tool developed at CMU.

---

People.

The core team:
     Sagar Chaki, CMU, SEI
     James Ivers, CMU, SEI
     Natasha Sharygina, CMU, SEI and School of Computer Science
     Kurt Wallnau, CMU, SEI
Collaborators:
     Edmund Clarke, CMU, School of Computer Science
     Daniel Kroening, ETH
Students:
     Nishant Sinha, CMU, EE