Towards an Arithmetic Theory of Consistency Enforcement based on Preservation of delta-constraints

Show simple item record Link, Sebastian en Schewe, KD en 2012-12-04T03:42:04Z en 2002-01 en
dc.identifier.citation Electronic Notes in Theoretical Computer Science 61:64-83 Jan 2002 en
dc.identifier.issn 1571-0661 en
dc.identifier.uri en
dc.description.abstract Consistency Enforcement provides an alternative theory to common verification techniques within formal specification languages. We consider specifications in the form of guarded commands. The basic idea is then to replace a program specification S by its greatest consistent specialization (GCS) S_I which is provably consistent with respect to a given static constraint I, preserves the effects of S according to a specialization order and is maximal with these properties. The theory has been shown to provide several strengths. In particular, the enforcement process for a huge class of complex specifications can be reduced to its basic components. Moreover, the result can be obtained sequentially and is independent from the order of the given constraints. In addition, arithmetic logic has been used to show that GCSs can be efficiently computed for a reasonably large class of program specifications and invariants. However, all results have been achieved with respect to the underlying specialization order. The simplicity of this order reveals some obvious weaknesses. In this paper, we show how the specialization order can be replaced by the notion of δ-constraints. Specialization of a program specification S turns out to be equivalent to the preservation of all δ-constraints on the underlying state space of S. Obviously, this enables us to weaken the specialization order towards the preservation of certain δ-constraints. We define maximal consistent effect preservers (MCEs), show that these are closely related to GCSs and prove that MCEs can be obtained sequentially and independently from the order of a given set of static constraints. This backs up the conjecture that the notion of MCEs leads towards a tailored theory of consistency enforcement. en
dc.publisher Elsevier en
dc.relation.ispartofseries Electronic Notes in Theoretical Computer Science en
dc.rights Items in ResearchSpace are protected by copyright, with all rights reserved, unless otherwise indicated. Previously published items are made available in accordance with the copyright policy of the publisher. Details obtained from en
dc.rights.uri en
dc.subject Formal specification en
dc.subject Guarded commands en
dc.subject Arithmetic logic en
dc.subject Constraint en
dc.subject Consistency en
dc.title Towards an Arithmetic Theory of Consistency Enforcement based on Preservation of delta-constraints en
dc.type Journal Article en
dc.identifier.doi 10.1016/S1571-0661(04)00306-8 en
pubs.begin-page 64 en
pubs.volume 61 en
dc.rights.holder Copyright: Elsevier B.V. en
pubs.end-page 83 en
dc.rights.accessrights en
pubs.subtype Article en
pubs.elements-id 365859 en Science en School of Computer Science en
pubs.record-created-at-source-date 2012-11-30 en

Files in this item

There are no files associated with this item.

Find Full text

This item appears in the following Collection(s)

Show simple item record


Search ResearchSpace