Project

General

Profile

Feature #2165

[Analysis] use counter-example to refine black box components guarantees

Added by Anonymous almost 6 years ago. Updated over 1 year ago.

Status:
Rejected
Priority:
Normal
Assignee:
-
Category:
-
Target version:
Start date:
11/25/2014
Due date:
% Done:

0%

Estimated time:

Description

  1. Open the attached project
  2. Open the component architecture
  3. Open the component named "Component"
  4. In the navigation tree, open "A/G, Contracts, Patterns"
  5. In the editor which just opened, click "Check selected"
  6. Observe that the specification is "FAIL"
  7. Observe that the Counterexample view opened on the right
  8. Observe that this counterexample involves the output of the subcomponent C (which should probably be equal to -1 in the counterexample)

Note: C is considered as a black box for verification in the model (which can be seen by clicking on it and observing the Properties section)

Now imagine the following situation: C should actually never output -1.
Since it is unimplemented, AF3 cannot know it, but the user (we) know it.
Now we would like to inform AF3 about this fact.

To do so, this issue is about adding the following:
  1. when the counterexample involves a blackbox component (in the example above: C) some GUI element (button, list, whatever -- to be discussed) should give the user the option to refine this blackbox component in order to avoid these cases
  2. when selected by the user, the corresponding specification should be added as a contract to the component (in the example above: Output != -1)

Any improvements to the counterexample GUI are welcomed...

AF3-Project.af3_23 (3.9 KB) AF3-Project.af3_23 Anonymous, 11/25/2014 12:49 PM
Issue.af3_23 (17.6 KB) Issue.af3_23 Anonymous, 12/01/2014 11:41 AM

Related issues

Related to Change Request #2141: [Analysis] XML support for NuSMVClosed10/09/2014

Related to Feature #2128: [Analyses/Simulation] Looping simulationsNew09/05/2014

History

#1 Updated by Anonymous almost 6 years ago

#2 Updated by Anonymous almost 6 years ago

  • Related to Feature #2128: [Analyses/Simulation] Looping simulations added

#3 Updated by Anonymous almost 6 years ago

Fixed the attached model

#4 Updated by Anonymous over 5 years ago

  • Target version changed from AF3 2.7 RC1 (features frozen) to AF3 2.8 RC1 (Feature Freeze)

#5 Updated by Anonymous about 5 years ago

  • Target version changed from AF3 2.8 RC1 (Feature Freeze) to AF3 2.8 RC2 (Tested & Bugfixed)

#6 Updated by Anonymous about 5 years ago

  • Target version changed from AF3 2.8 RC2 (Tested & Bugfixed) to AF3 2.9 RC1 (Features frozen)

#7 Updated by Anonymous over 4 years ago

  • Target version changed from AF3 2.9 RC1 (Features frozen) to AF3 2.10 Feature Freeze

#8 Updated by Johannes Eder about 4 years ago

  • Assignee set to Anonymous
  • Target version changed from AF3 2.10 Feature Freeze to AF3 2.10 Post-release

#9 Updated by Anonymous over 3 years ago

  • Target version changed from AF3 2.10 Post-release to AF3 2.12 RC1 (Feature Freeze)

#10 Updated by Anonymous over 2 years ago

  • Target version changed from AF3 2.12 RC1 (Feature Freeze) to AF3 2.13 RC1 (Feature Freeze)

#11 Updated by Anonymous over 2 years ago

  • Assignee changed from Anonymous to Anonymous

@Sudeep: Again a contract-related thing. I think it's nice but I doubt people now put that of a priority on contracts so we could reject.
Maybe there are some ideas to take for CBMD.

#12 Updated by Anonymous over 2 years ago

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

#13 Updated by Johannes Eder over 1 year ago

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

#14 Updated by Anonymous over 1 year ago

  • Assignee changed from Anonymous to Johannes Eder

Please reject.

#15 Updated by Johannes Eder over 1 year ago

  • Status changed from New to Rejected
  • Assignee deleted (Johannes Eder)

Also available in: Atom PDF