Consistency Enforcement for Static First-Order Invariants in Sequential Abstract State Machines

摘要

Given a program specification P and a first-order static invariant I the problem of consistency enforcement is to determine a modified program specification P_I that is consistent with respect to I, i.e. whenever I holds in a state S it also holds in the successor states determined by P_I, and at the same time only minimally deviates from P. We formalise this problem by the notion of the greatest consistent specialisation (GCS) adapting and generalising this 20 year old concept to sequential Abstract State Machines (ASMs) with emphasis on bounded parallelism. In a state satisfying I such that P is repairable the notion of consistent specialisation will require an enlargement of the update set, which defines a partial order with respect to which a GCS is defined. We show that GCSs are compositional in two respects: (1) the GCS of an ASM with a complex rule can be obtained from the GCSs of the involved assignments, and (2) the GCS with respect to a set of invariants can be built using the GCSs for the individual invariants in the set.