Model based design

Model based design
Slides di riferimento
“MODEL BASED DEVELOPMENT”
Ambienti di specifica e verifica commerciali
•
•
•
•
IAR Visualstate
Ilogix Statemate
Matlab Stateflow
SCADE
Model checker: Design Verifier
(Prover Technologies)
basati sui formalismi
Generatore di codice certificato
SIL4 secondo EN 50128
Statecharts e Lustre (+ Statecharts)
Strumenti con funzionalità di simulazione e (parzialmente) di verifica formale,
nonchè di generazione del codice
Tendenza all’uso degli State Diagrams di UML, ma ancora non sono disponibili
strumenti commerciali di verifica
Rhapsody (IBM) è lo strumento più avanzato tra gli strumenti di supporto a UML
per la definizione, simulazione e generazione di codice da State Diagrams
UML.
Statecharts (D. Harel)
Stateflow model of a track circuit
SCADE model of a track circuit
Rhapsody
Rhapsody
Rhapsody
Verification by
Design Verifier
Verification by
Design Verifier
Verification by
Design Verifier
Verification by
Design Verifier
© Copyright 2008 Rockwell Collins, Inc.
ADGS-2100 Adaptive Display & Guidance System
Modeled in Simulink
Translated to NuSMV
4,295 Subsystems
16,117 Simulink Blocks
Over 1037 Reachable States
Example Requirement:
Drive the Maximum Number of Display Units
Given the Available Graphics Processors
Counterexample Found in 5 Seconds
Checked 573 Properties Found and Corrected 98 Errors
in Early Design Models
© Copyright 2008 Rockwell Collins, Inc.
CerTA FCS Phase I – Errors Found
Errors Found in Redundancy
Manager
Triplex Voter
Model Checking
Testing
0
Failure Processing
5
3
Reset Manager
4
0
12
0
Total
0
• Model-Checking Found 12 Errors that Testing Missed
• Spent More Time on Testing than Model-Checking
– 60% of total on testing vs. 40% on model-checking
Model-checking was more cost effective
than testing at finding design errors.
Example of Model Based development
(including Model Based Testing and Static
analysis by Abstract Interpretation)

Download Report