Project

General

Profile

Support #3411

rethink bounds check design

Added by Anonymous over 2 years ago. Updated over 1 year ago.

Status:
New
Priority:
Normal
Assignee:
-
Category:
-
Target version:
Start date:
05/17/2018
Due date:
% Done:

0%

Estimated time:

Description

This information is written here because here it would be available to anyone wanting to change the specification of bounds check.

We use NuSMV to check the bounds. Outputs of a component map to "DEFINE" in NuSMV which is just a name for an expression, i.e., it is not a variable. This "DEFINE" can not be used in a property
specification because of language limitations in NuSMV.

So, as a result we generate the following specification for each transition t:
"actions in t do not violate the bound"
This approach generates too many specifications but there is no other way out.


Related issues

Related to Feature #3024: [Constraint] port boundNew08/04/2017

Related to Bug #3412: bounds check fails for strongly causal componentNew05/17/2018

History

#1 Updated by Anonymous over 2 years ago

#2 Updated by Anonymous over 2 years ago

  • Related to Bug #3412: bounds check fails for strongly causal component added

#3 Updated by Johannes Eder over 1 year ago

  • Target version changed from AF3 2.14 RC1 (Feature Freeze) to Backlog

Also available in: Atom PDF