Sciweavers

Share
ATVA
2015
Springer

Spanning the Spectrum from Safety to Liveness

3 years 5 months ago
Spanning the Spectrum from Safety to Liveness
Of special interest in formal verification are safety specifications, which assert that the system stays within some allowed region, in which nothing “bad” happens. Equivalently, a computation violates a safety specification if it has a “bad prefix” – a prefix all whose extensions violate the specification. The theoretical properties of safety specifications as well as their practical advantages with respect to general specifications have been widely studied. Safety is binary: a specification is either safety or not safety. We introduce a quantitative measure for safety. Intuitively, the safety level of a language L measures the fraction of words not in L that have a bad prefix. In particular, a safety language has safety level 1 and a liveness language has safety level 0. Thus, our study spans the spectrum between traditional safety and liveness. The formal definition of safety level is based on probability and measures the probability of a random word not in L to...
Rachel Faran, Orna Kupferman
Added 16 Apr 2016
Updated 16 Apr 2016
Type Journal
Year 2015
Where ATVA
Authors Rachel Faran, Orna Kupferman
Comments (0)
books