Subject: safety and liveness definitions
From: Anthony McIsaac (anthony.mcisaac@st.com)
Date: Thu Sep 26 2002 - 08:11:17 PDT
I was asked to suggest alternative "more formal" definitions if I
could improve on those in the text, with "any sequence" replaced by "any finite path",
and "sequence" by "path".
On reflection, the definition of safety properties seems to me nearly correct.
I won't pursue the line I was taking at the meeting, but have got a different point.
I believe that safety properties are commonly identified with closed, prefix-closed
sets of paths. The definition as it stands covers the prefix-closed aspect, so the only
gap concerns closure. This crops up with properties like "eventually! (always !a)"
(there are only finitely many occurrences of a), which isn't violated on any finite
path, so satisfies the definition as it stands, but isn't a safety property.
If we want the definition to cover this, I suggest
"A safety property is a property such that if any path violates the property, then
it has a finite subpath such that every extension of the subpath violates the property."
As for liveness properties, as far as I know there isn't a formal definition; it's
more of an informal notion (perhaps the academics on the committee will correct me
on this). So it probably doesn't matter if the "more formal" definition isn't
quite accurate, and I'm not going to propose an alternative. I would just mention
that, according to the definition given, "there are more occurrences of a than b"
is a liveness property.
Anthony
-- Anthony McIsaacSTMicroelectronics Limited 1000 Aztec West Almondsbury Bristol BS32 4SQ
Tel: ++44 (0)1454 462466 Fax: ++44 (0)1454 617910
Email: Anthony.McIsaac@st.com
This archive was generated by hypermail 2b28 : Thu Sep 26 2002 - 08:12:56 PDT