Main Features:

Requirements Engineering (MIRA)

Modeling and simulation

  • Structure, analyze and validate requirements
  • Specify requirements in a rich model
  • Deeply integrate requirements with the architecture



What is MIRA
Requirements Analysis
Graph view
Glossary
Requirement Sources
Requirements
Message Sequence Charts
Contracts Specification

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



Model Element Attributes
System Architecture Modeling
Data Modeling
Behaviour Modeling:
      - Code Specifications
      - State Automata
      - Mode Automata
      - Tabular Specifications
Hardware Architecture Modeling
Simulation
Cosimulation
Operator Panels
Library of Components, Functions and Types
Refinement
Refactoring

Code generation and deployment

Testing and formal verification

  • Flexible generation of C, Java, etc code
  • Deployment on different hardware platforms
  • Generation of platform specific code



Code Generation
Code Generation for PikeOS
Manual Deployment
Efficient Architecture Synthesis
Efficient Deployment Synthesis
Efficient Scheduling Synthesis
DSE Perspective (experimental)New in 2.9.0!

  • Deep integration of the NuSMV model-checker
    and Yices SMT solver
  • Both out-of-the-box and customizable analyses



On the Fly Constraints Checking
Model Checking
Model Checking (using CProver)
Nondeterminism Analysis
Model Based Testing
Refinement Testing
Assume/Guarantee Reasoning
MSC Conformity Checking

Safety Case Modelling

...next big thing...

  • Modelling (complex) Safety Cases
  • Describe Safety Arguments using GSNs
  • Integrate Safety Cases with the architecture



Safety Cases in AF3

 

 

For more details see our screencasts