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.
KeywordsConsistency enforcement Static invariant Consistent specialisation Abstract State Machine Compositionality
- 2.Börger, E., Schewe, K.-D.: A behavioural theory of recursive algorithms (2019). Submitted for publicationGoogle Scholar
- 4.Cai, C., Sun, J., Dobbie, G.: B-repair: repairing B-models using machine learning. In: 23rd International Conference on Engineering of Complex Computer Systems (ICECCS 2018), pp. 31–40. IEEE Computer Society (2018)Google Scholar
- 6.Ferrarotti, F., González, S., Schewe, K.-D., Turull-Torres, J.M.: Systematic refinement of abstract state machines with higher-order logic. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) ABZ 2018. LNCS, vol. 10817, pp. 204–218. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-91271-4_14CrossRefGoogle Scholar
- 8.Ferrarotti, F., Schewe, K.-D., Tec, L., Wang, Q.: A complete logic for database abstract state machines. Log. J. IGPL 25(5), 700–740 (2017)Google Scholar