Spinroot

awesan

Member

Registered: 2011-04-30

Posts: 45

Questions on property-based slicing in SPIN

Q-1:
As I was reading property-based slicing and experimenting the same with SPIN, the following question arose in my mind (though I have not run into this situation). If SPIN reports the same lines of source code as redundant for all the LTL properties that are intended to be verified in the model, does that imply that those lines of source code are "completely provably irrelevant" in the model and thus the model can be simplified by removing those lines? If the answer is "no", then I assume that the user has to pay close attention to the lines of source code reported as "redundant" by SPIN and see logically whether they don't make any sense in the model and remove them, if it would be appropriate to do so. What led me asking this question is the following text in page-232 (Chapter-10) of the SPIN book : [quote] [b] Although, this method (property-based slicing) can be shown to preserve both logical soundness and logical completeness of the correctness properties that are used in deriving the abstraction, it does not necessarily have these desirable properties for some other types of correctness requirements that cannot be expressed in assertions or in LTL formulae. An example of such a property is "absence of deadlock". Note that the introduction of extra behavior in a model can result in the disappearance of system deadlocks.[/quote] [/b]

Q-2:
From the above text quoted from the book in Q-1, this question follows : "If a simplified model (simplified by removing the lines of code and variables based on the redundancies reported by SPIN's property-based slicing) is verified for the corresponding LTL properties (and assertions) and also the "safety" properties, could the original model suffer from "deadlocks" even if the simplified model does not report any "deadlocked states"?

Q-3:
SPIN reports the message "spin: no redundancies found (for given property)" only once for a model that has multiple LTL properties defined in the model. Does SPIN apply the property-based slicing algorithm for each LTL property separately or does it apply for all the LTL properties together? The reason I ask this is that it reports only once but the message says "for given property".

Last edited by awesan (2012-01-16 04:09:53)

spinroot

forum

Registered: 2010-11-18

Posts: 702

Website

Re: Questions on property-based slicing in SPIN

you raise an important question.
when the property based slicing algorithm was introduced, spin supported the definition of only a single never claim or ltl property.
in the latest version 6 spin added support for the definition of inline ltl properties, and multiple properties, although during the verification still only a single ltl property is checked at a time
i believe, but this would need to be checked more thoroughly, that when the slicing algorithm checks for redundancies it has seen all ltl properties and therefore the verdict "no redundancies" would apply to all properties.  removing a property could then alter the verdict.
(so it does not say 'property' intentionally -- the phrasing of the message simply wasn't adjusted when the specification of multiple properties became possible).
and yes, removing parts of the model that may be considered redundant can alter other behavior that may also be of interest, such as cycling and deadlocking behavior...