Project

General

Profile

Support #3509

rework OCRA refinement

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

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

0%

Estimated time:

Description

At present the verification using OCRA contracts works as follows:
1) For the atomic components the property is tested against the behaviour
2) for the composite components the property is tested for the refinement. The user in this case has to provide the list of refining contracts and the tool tries to prove the property using these contracts

This causes usability issues as the suer needs to define a lot of contracts, and also the contracts at lower levels mimic the behaviour.

For the tutorial and in the future we want to give an option to the user such that contracts at composite components can also be verified against the behaviour.

My approach to this issue is: if no refining contract is specified then verify the specification against the behaviour otherwise use the refinement.

History

#1 Updated by Anonymous about 2 years ago

  • Parent task set to #3489

#2 Updated by Anonymous about 2 years ago

  • Parent task deleted (#3489)

#3 Updated by Johannes Eder over 1 year ago

  • Target version changed from AF3 2.14 RC2 (Tested, Bug-free) to Backlog

Also available in: Atom PDF