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