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...

Full description

Saved in:
Bibliographic Details
Published in:International journal of computer mathematics 2011-03, Vol.88 (4), p.665-694
Main Authors: Mastroeni, Isabella, Giacobazzi, Roberto
Format: Article
Language:English
Subjects:
abstract interpretation
Cancellation
closure operators
Computer simulation
Construction
Mathematical analysis
Mathematical models
Monitors
Preserves
program verification
Safety
Semantics
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0020-7160
1029-0265
DOI:10.1080/00207161003703205