Software & Tools

  • CARTS (Compositional Analysis of Real-Time Systems)
  • Architecture aware analysis of concurrent software (Checkfence)
  • We partner with Fremont Associates to provide tool support for analysis of embedded systems architectures expressed in the AADL modeling language. Formal schedulability analysis algorithms are implemented in the Furness toolset.
    • An industrial case study is starting in collaboration with Honeywell, which aims at the modeling and analysis of wireless architectures.
  • Automated symbolic compositional verification by learning assumptions, JIST (Interfaces for Java classes using abstraction and games)
  • Specification, Analysis, and Testing of Scenario-based Requirements
  • HERMES (Model Checking of Hierarchical State Machines)
  • Mocha (Model checking of open systems using ATL)
  • CHARON (Hybrid systems: modeling and verification)
  • Timed and hybrid automata