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
Glossary
Requirement Sources
Requirements
Message Sequence Charts
Contracts Specification
Safety Integrity Level Specification

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



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

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
Efficient Deployment and Scheduling
Manual Deployment
Multi-Core Architecture Synthesis

  • 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

 

 

For more details see our screencasts