Skip to main content
SpringerLink
Log in

Reasoning About Resources in the Embedded Systems Language Hume

  • Conference paper
  • First Online:
Foundational and Practical Aspects of Resource Analysis (FOPARA 2013)

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

  • 286 Accesses

Abstract

In this paper we present an instrumented program logic for the embedded systems language Hume, suitable to reason about resource consumption. Matching the structure of Hume programs, it integrates two logics, a VDM-style program logic for the functional language and a TLA-style logic for the coordination language of Hume. We present a soundness proof of the program logic, and demonstrate the usability of these logics by proving resource bounds for a Hume program. Both logics, the soundness proof and the example have been fully formalised in the Isabelle/HOL theorem prover.

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

Access this chapter

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 34.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 44.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

Institutional subscriptions

Notes

  1. 1.

    This is theorem soundness in the Isabelle/HOL theory GRUMPY.thy.

  2. 2.

    This is theorem vdmexe in Integrated.thy.

  3. 3.

    This example is theory ListCopy.thy of the Isabelle/HOL embedding.

  4. 4.

    These are theorems copy_resources_ok and fuse_resources_ok in ListCopy.thy.

  5. 5.

    This is the main theorem in the theory file ST.thy.

References

  1. Aspinall, D., Beringer, L., Hofmann, M., Loidl, H.-W., Momigliano, A.: A program logic for resources. Theoret. Comput. Sci. 389(3), 411–445 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  2. Baeten, J.C.M.: A brief history of process algebra. Theoret. Comput. Sci. 335(2–3), 131–146 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  3. Butler, M.J.: csp2B: a practical approach to combining CSP and B. Form. Asp. Comput. 12(3), 182–198 (2000)

    Article  MATH  Google Scholar 

  4. Filliâtre, J.-C.: Why: a multi-language multi-prover verification tool. Research report 1366, LRI, Université Paris Sud, March 2003

    Google Scholar 

  5. Fischer, C.: CSP-OZ: a combination of object-Z and CSP. In: Formal Methods for Open Object-Based Distributed Systems (FMOODS ’97), pp. 423–438 (1997)

    Google Scholar 

  6. Grov, G.: Reasoning about correctness properties of a coordination programming language. Ph.D. thesis, Heriot-Watt University (2009)

    Google Scholar 

  7. Grov, G., Michaelson, G., Ireland, A.: Formal verification of concurrent scheduling strategies using TLA. In: International Conference on Parallel and Distributed Systems (ICPADS’07), pp. 1–6. IEEE, Hsinchu, December 2007

    Google Scholar 

  8. Grov, G., Merz, S.: A Definitional Encoding of TLA* in Isabelle/Hol. Archive of Formal Proofs, Formal proof development, November 2011. http://afp.sf.net/entries/TLA

  9. Hammond, K., Michaelson, G.J.: Hume: a domain-specific language for real-time embedded systems. In: Pfenning, F., Macko, M. (eds.) GPCE 2003. LNCS, vol. 2830, pp. 37–56. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  10. Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)

    MATH  Google Scholar 

  11. Huisman, M., Jacobs, B.: Java program verification via a Hoare logic with abrupt termination. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol. 1783, p. 284. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  12. Jones, C.: Systematic Software Development Using VDM. Prentice Hall, Englewood Cliffs (1990)

    MATH  Google Scholar 

  13. Kleymann, T.: Hoare logic and VDM: machine-checked soundness and completeness proofs. Ph.D. thesis, LFCS, University of Edinburgh (1999)

    Google Scholar 

  14. Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16(3), 872–923 (1994)

    Article  Google Scholar 

  15. Longley, J., Pollack, R.: Reasoning about CBV functional programs in Isabelle/HOL. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 201–216. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  16. Marché, C., Paulin-Mohring, C., Urbain, X.: The krakatoa tool for certification of Java/JavaCard programs annotated in JML. J. Logic Algebraic Program. 58(1–2), 89–106 (2004)

    Article  MATH  Google Scholar 

  17. Müller, P., Meyer, J., Poetzsch-Heffter, A.: Programming and interface specification language of JIVE. Fernuniversität Hagen, Technical report (2000)

    Google Scholar 

  18. Nipkow, T.: Hoare logics for recursive procedures and unbounded nondeterminism. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol. 2471, p. 103. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  19. Poetzsch-Heffter, A., Müller, P.O.: A programming logic for sequential Java. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol. 1576, p. 162. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  20. Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: Symposium on Logic in Computer Science (LICS’02), pp. 55–74. IEEE Computer Society, Copenhagen, July 2002

    Google Scholar 

  21. Schneider, S., Treharne, H.: CSP theorems for communicating B machines. Form. Asp. Comput. Appl. Form. Methods 17(4), 390–422 (2005)

    Article  MATH  Google Scholar 

  22. von Oheimb, D.: Hoare logic for Java in Isabelle/HOL. Concurr. Comput. Pract. Exp. 13(13), 1173–1214 (2001)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Mathematical and Computer Sciences, Heriot-Watt University, EH14 4AS, Edinburgh, UK

    Hans-Wolfgang Loidl & Gudmund Grov

Authors
  1. Hans-Wolfgang Loidl
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Gudmund Grov
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Hans-Wolfgang Loidl .

Editor information

Editors and Affiliations

  1. Università di Bologna, Bologna, Italy

    Ugo Dal Lago

  2. Universidad Complutense de Madrid, Madrid, Spain

    Ricardo Peña

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Loidl, HW., Grov, G. (2014). Reasoning About Resources in the Embedded Systems Language Hume. In: Dal Lago, U., Peña, R. (eds) Foundational and Practical Aspects of Resource Analysis. FOPARA 2013. Lecture Notes in Computer Science(), vol 8552. Springer, Cham. https://doi.org/10.1007/978-3-319-12466-7_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-12466-7_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-12465-0

  • Online ISBN: 978-3-319-12466-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation