![Sample our Computer Science journals, sign in here to start your access, latest two full volumes FREE to you for 14 days]({"type":"image" , "src" : "/sda/5928/TOC-Subject-Sample-2021-Computer-Science.jpg"})
Abstract
In this paper, we describe safety semantics as abstract interpretation of a trace-based operational semantics of a transition system. Intuitively, a property is safety if ‘nothing bad will happen’. Formally this is described by saying that a property is safety if it is maximal with respect to a given set of allowed partial executions. We show that this can be specified in the standard Cousot's framework of abstract interpretation. In particular, we show that this semantics can be derived as fixpoint of a semantic operator. This construction provides a formal characterization of the constructive nature of safety properties, that can be enforced by means of execution monitors. By using the same construction, we show that while safety without stuttering preserves the constructive nature, safety properties allowing cancellation of states lose the constructive characterization. Finally, we characterize safety properties as the closed elements of a closure, and we show that in the abstract interpretation framework safety and liveness properties lose their complementary nature.
Acknowledgements
We thank the anonymous referees for the very helpful comments on the previous versions of this paper. We also thank Patrick Cousot for the useful discussions made about the ideas developed in this paper.
Notes
Note that and ℤ− is analogously defined.
Note that, as explained in Section 2.2, in order to obtain a Galois insertion, the abstraction has to be surjective and therefore, in this case, we have to restrict the co-domain of precisely to the set of its images.
α applied to infinite traces is the natural extension of the corresponding function defined in .
We wrote z {0, 1} since we do not know if k m >1.
Minimal here means that if we erase some other states then we cannot rebuild σ by using α.