Model Checking with Verification Patterns

  • Model-checking support for a broad subset of AutoFOCUS3
  • Easy to write verification conditions (via patterns or sequence diagrams)
  • Modular verification of system, sub-systems or components

Simulatable Counterexample

  • Counter-examples provided in case of non-verified conditions
  • Simulate the counterexample using the AutoFOCUS3 simulator

Assume/Guarantee Reasoning

  • Black-box specification with assumptions and guarantees
  • Check if the guarantees of neighboring components fulfill the assumptions of a component

MSC Feasibility Checks

  • Verify if the application realizes a scenario
  • Check that bad scenarios are impossible

Checking for Non-determinism

  • Light-weighted analyses for possible non-determinism in state automata
  • In case when non-determinism is found, an evidence is given

One-click Reachability Analyses

  • Reachability analysis both at the system and component level

Advanced Tuning of Analyses

  • Specify bounds for individual ports or variables with integer type
  • Define a time-budget for performing analyses by setting timeouts

Model Proximity

  • Double-click on an analysis result and the relevant model parts will be opened in the editor


Sudeep Kanav

Sudeep Kanav

+49 89 3603522 35