©2023 ANSYS, Inc. Unauthorized use, distribution, or duplication is prohibited.
SCADE Properties
• Design is unambiguous
‐ Each construct has a well-defined semantic
• Design is verifiable
‐ Semantic checks performed to verify that a SCADE model is semantically correct (defined later)
‐ The model can be simulated
• A SCADE model can be automatically translated to C or Ada language
• The obtained software:
‐ Has a deterministic behavior: a given set of inputs to the system will always produce the same outputs
‐ Its execution time is bounded
‐ Its memory usage is finite
14
