Interpretation of the GenericPropertiesVerdict.xml values

Go down

Interpretation of the GenericPropertiesVerdict.xml values

Post by amparore on Fri 13 Apr - 11:29

Dear MCC organizers,
   I was wondering whether the values stored in the GenericPropertiesVerdict.xml file should
be considered trustable, i.e. when a model is declared SAFE or LIVE, it is surely this way,
or if instead this is only an hint. There is no mention of the trustability of these values in the
Tool Submission Manual.

   This is an important issue, since:
- if I remember correctly, a few years ago some of these values were incorrect for some models;
- if a tool "trusts" these values, it could use some feature that would not work correctly if the
 property was wrongly declared;
- what happens if a MCC model declares a wrong property value, making a tool mis-compute a result?

Also, the property list contains a DEADLOCK property. What is the purpose of having a ReachabilityDeadlock
examination when the response value is already stored in the xml file? Should we just return this value
instead of doing any computation?

Regards
--Elvio

amparore

Posts : 6
Join date : 2016-11-30

View user profile

Back to top Go down

Re: Interpretation of the GenericPropertiesVerdict.xml values

Post by lhillah on Sat 14 Apr - 3:21

Dear Elvio,

These values should be trusted as much as those exposed in the model forms. They are extracted from there. Values of such properties in the model forms are provided by the submitter. They are quickly checked by the model board but not to such a full extent (checking time is limited to 1 mn) to guarantee 100% correctness. Large instances of many models typically have not been fully checked (and it is often reported as footnotes in the model forms).

For instance, Bernard reported the case of RwMutex where all previous editions of the MCC showed that all its instances are safe, but the model form was still displaying 'unknown' for that property. In such cases only we update the model form, and subsequently the GenericPropertiesVerdict.xml. The values stated in that file (and the model form where they come from) are therefore not even strictly instance-based. This is a first imperfect attempt to make that information readable for tools, as a hint from the model form. More work is needed in the future to exploit the actual results of the MCC to (perfectly) relate those properties values to the actual instances the values correspond to (true, false, unknown according to data drawn from the examination results).

About the deadlock property, it is listed in a model form and therefore extracted as the others into the GenericPropertiesVerdict file. So, w.r.t. what I said earlier, you should not take it as 100% correct across all instances of the model.

Kind regards,
Lom




lhillah

Posts : 9
Join date : 2017-01-04

View user profile

Back to top Go down

Re: Interpretation of the GenericPropertiesVerdict.xml values

Post by amparore on Mon 16 Apr - 9:35

Sorry Lom,
but I don't fully understand your response. Are non-trivial properties (like SAFE) just declared by the model submitters, or are they checked by some/multiple tools? From the descriptions in the xml, it appears that some values are "confirmed" by tools. Is this a manual process?
For new (surprise) models, the value that will appear has been tested (even with 1min time bound), or is just what the model submitter sent?
In that case, wouldn't it be better if the value is simply "unknown" if it is not confirmed yet by any tool?
Otherwise, I think that the usefulness of these values is very limited, if there is no strict guarantee on their correctness.

Regards
--Elvio

amparore

Posts : 6
Join date : 2016-11-30

View user profile

Back to top Go down

Re: Interpretation of the GenericPropertiesVerdict.xml values

Post by Sponsored content


Sponsored content


Back to top Go down

Back to top

- Similar topics

 
Permissions in this forum:
You cannot reply to topics in this forum