Skip to main content
SpringerLink
Log in
Book cover

International Conference on Formal Engineering Methods

ICFEM 2019: Formal Methods and Software Engineering pp 219–235Cite as

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

  • Conference paper
  • First Online:

  • 861 Accesses

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11852))

Abstract

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.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

References

  1. Abrial, J.-R.: The B-Book - Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)

    MATH  Google Scholar 

  2. Börger, E., Schewe, K.-D.: A behavioural theory of recursive algorithms (2019). Submitted for publication

    Google Scholar 

  3. Börger, E., Stärk, R.: Abstract State Machines. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-642-18216-7

    Book  MATH  Google 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 

  5. Dijkstra, E.W., Scholten, C.S.: Predicate Calculus and Program Semantics. Texts and Monographs in Computer Science. Springer, New York (1990). https://doi.org/10.1007/978-1-4612-3228-5

    Book  MATH  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_14

    Chapter  Google Scholar 

  7. Ferrarotti, F., Schewe, K.-D., Tec, L., Wang, Q.: A new thesis concerning synchronised parallel computing - simplified parallel ASM thesis. Theor. Comput. Sci. 649, 25–53 (2016)

    Article  MathSciNet  Google 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 

  9. Ferrarotti, F., Schewe, K.-D., Tec, L., Wang, Q.: A unifying logic for non-deterministic, parallel and concurrent abstract state machines. Ann. Math. Artif. Intell. 83(3–4), 321–349 (2018)

    Article  MathSciNet  Google Scholar 

  10. Gurevich, Y.: Sequential abstract state machines capture sequential algorithms. ACM Trans. Comput. Logic 1(1), 77–111 (2000)

    Article  MathSciNet  Google Scholar 

  11. Link, S., Schewe, K.-D.: Towards an arithmetic theory of consistency enforcement based on preservation of delta-constraints. Electr. Notes Theor. Comput. Sci. 61, 64–83 (2002)

    Article  Google Scholar 

  12. Nelson, G.: A generalization of Dijkstra’s calculus. ACM Trans. Program. Lang. Syst. 11(4), 517–561 (1989)

    Article  Google Scholar 

  13. Schewe, K.-D.: Consistency enforcement in Entity-Relationship and object-oriented models. Data Knowl. Eng. 28(1), 121–140 (1998)

    Article  Google Scholar 

  14. Schewe, K.-D., Thalheim, B.: Limitations of rule triggering systems for integrity maintenance in the context of transition specifications. Acta Cybern. 13(3), 277–304 (1998)

    MathSciNet  MATH  Google Scholar 

  15. Schewe, K.-D., Thalheim, B.: Towards a theory of consistency enforcement. Acta Inf. 36(2), 97–141 (1999)

    Article  MathSciNet  Google Scholar 

  16. Schmidt, J., Krings, S., Leuschel, M.: Repair and generation of formal models using synthesis. In: Furia, C.A., Winter, K. (eds.) IFM 2018. LNCS, vol. 11023, pp. 346–366. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-98938-9_20

    Chapter  Google Scholar 

  17. Thalheim, B.: Dependencies in Relational Databases. Springer, Wiesbaden (1991). https://doi.org/10.1007/978-3-663-12018-6

    Book  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Zhejiang University, UIUC Institute, Haining, China

    Klaus-Dieter Schewe

Authors
  1. Klaus-Dieter Schewe
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Klaus-Dieter Schewe .

Editor information

Editors and Affiliations

  1. IRIT/INPT - ENSEEIHT, Toulouse, France

    Yamine Ait-Ameur

  2. Teesside University, Middlesbrough, UK

    Shengchao Qin

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Schewe, KD. (2019). Consistency Enforcement for Static First-Order Invariants in Sequential Abstract State Machines. In: Ait-Ameur, Y., Qin, S. (eds) Formal Methods and Software Engineering. ICFEM 2019. Lecture Notes in Computer Science(), vol 11852. Springer, Cham. https://doi.org/10.1007/978-3-030-32409-4_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-32409-4_14

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-32408-7

  • Online ISBN: 978-3-030-32409-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation