Main Features

AF3 is a model based development tool for distributed, reactive, embedded software systems 

AF3 uses models in all development phases including requirements analysis, design of the logical architecture, design of the hardware architecture, implementation and deployment. Furthermore, AF3 features formal analyses and synthesis methods.

Requirements Specification and Analysis (MIRA)

  • Structure, analyze and verify requirements
  • Specify requirements in a rich model

Modeling and Simulation

  • Advanced and deeply integrated models for architecture, behaviour and platform
  • Simulation and on the fly consistency checks

Code Generation and Deployment

  • Flexible generation of C code, Java code, etc.
  • Deployment on different hardware platforms

Formal Verification

  • Out-of-the-box, easy to use analyses
  • Advanced verification support
  • Deep integration of NuSMV and Yices tools

Design Space Exploration

  • Solving mixed-criticality problems in AutoFOCUS3
  • Deployment or Scheduling Synthesis and Optimization


  • Specify test suite through coverage criteria or random input parameters
  • Automatic test-case generation
  • Easy simulation of the system by test-cases

Assurance cases

  • GSN edior for modular assurance cases

  • Assurance case patterns – creation, storage and instantiation