An Abstract Interpretation-based Model for Safety Semantics

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.