Skip to main content
SpringerLink
Log in

Deriving Real-Time Action Systems Controllers from Multiscale System Specifications

  • Conference paper
Book cover Mathematics of Program Construction (MPC 2012)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7342))

Included in the following conference series:

Abstract

This paper develops a method for deriving controllers for real-time systems in which the components of the system operate at different time granularities. To this end, we incorporate the theory of time bands into action systems, which allows one to structure a system into multiple abstractions of time. The framework includes a logic that facilitates reasoning about different types of sampling errors and transient properties (i.e., properties that only hold for a brief amount of time), and we develop theorems for simplifying proofs of hardware/software interaction. We formalise true concurrency and define refinement for the parallel composition of action systems. Our method of derivation builds on the verify-while-develop paradigm, where the action system code is developed side-by-side with its proof.

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 39.99
Price excludes VAT (USA)
  • Available as 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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Aichernig, B.K., Brandl, H., Krenn, W.: Qualitative Action Systems. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 206–225. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  2. Back, R.-J., Petre, L., Porres, I.: Generalizing Action Systems to Hybrid Systems. In: Joseph, M. (ed.) FTRTFT 2000. LNCS, vol. 1926, pp. 202–213. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  3. Back, R.-J.R., Sere, K.: Stepwise refinement of action systems. Structured Programming 12(1), 17–30 (1991)

    Google Scholar 

  4. Back, R.-J.R., von Wright, J.: Trace Refinement of Action Systems. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 367–384. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  5. Back, R.-J.R., von Wright, J.: Refinement Calculus: A Systematic Introduction. Springer-Verlag New York, Inc., Secaucus (1998)

    MATH  Google Scholar 

  6. Back, R.-J.R., von Wright, J.: Compositional action system refinement. Formal Asp. Comput. 15(2-3), 103–117 (2003)

    Article  MATH  Google Scholar 

  7. Broy, M.: Refinement of time. Theor. Comput. Sci. 253(1), 3–26 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  8. Burns, A., Baxter, G.: Time bands in systems structure. In: Structure for Dependability: Computer-Based Systems from an Interdisciplinary Perspective, pp. 74–88. Springer (2006)

    Google Scholar 

  9. Burns, A., Hayes, I.J.: A timeband framework for modelling real-time systems. Real-Time Systems 45(1), 106–142 (2010)

    Article  MATH  Google Scholar 

  10. Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley Longman Publishing Co., Inc. (1988)

    Google Scholar 

  11. Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453–457 (1975)

    Article  MathSciNet  MATH  Google Scholar 

  12. Dongol, B.: Progress-based verification and derivation of concurrent programs. PhD thesis, The University of Queensland (2009)

    Google Scholar 

  13. Dongol, B., Hayes, I.J.: Enforcing safety and progress properties: An approach to concurrent program derivation. In: 20th ASWEC, pp. 3–12. IEEE Computer Society (2009)

    Google Scholar 

  14. Dongol, B., Hayes, I.J.: Compositional Action System Derivation Using Enforced Properties. In: Bolduc, C., Desharnais, J., Ktari, B. (eds.) MPC 2010. LNCS, vol. 6120, pp. 119–139. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  15. Dongol, B., Hayes, I.J.: Reasoning about teleo-reactive programs under parallel composition. Technical Report SSE-2011-01, The University of Queensland (April 2011)

    Google Scholar 

  16. Dongol, B., Hayes, I.J.: Approximating idealised real-time specifications using time bands. In: AVoCS 2011. ECEASST, vol. 46, pp. 1–16. EASST (2012)

    Google Scholar 

  17. Dongol, B., Hayes, I.J.: Deriving real-time action systems in a sampling logic. Sci. Comput. Program. (2012); accepted October 17, 2011

    Google Scholar 

  18. Dongol, B., Mooij, A.J.: Streamlining progress-based derivations of concurrent programs. Formal Aspects of Computing 20(2), 141–160 (2008)

    Article  MATH  Google Scholar 

  19. Feijen, W.H.J., van Gasteren, A.J.M.: On a Method of Multiprogramming. Springer (1999)

    Google Scholar 

  20. Gargantini, A., Morzenti, A.: Automated deductive requirements analysis of critical systems. ACM Trans. Softw. Eng. Methodol. 10, 255–307 (2001)

    Article  Google Scholar 

  21. Guelev, D.P., Hung, D.V.: Prefix and projection onto state in duration calculus. Electr. Notes Theor. Comput. Sci. 65(6), 101–119 (2002)

    Article  Google Scholar 

  22. Gupta, V., Henzinger, T.A., Jagadeesan, R.: Robust Timed Automata. In: Maler, O. (ed.) HART 1997. LNCS, vol. 1201, pp. 331–345. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  23. Hayes, I.J., Burns, A., Dongol, B., Jones, C.B.: Comparing models of nondeterministic expression evaluation. Technical Report CS-TR-1273, Newcastle University (2011)

    Google Scholar 

  24. Henzinger, T.A.: The theory of hybrid automata. In: LICS 1996, pp. 278–292. IEEE Computer Society, Washington, DC (1996)

    Google Scholar 

  25. Henzinger, T.A., Qadeer, S., Rajamani, S.K.: Assume-Guarantee Refinement Between Different Time Scales. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 208–221. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  26. Manna, Z., Pnueli, A.: Temporal Verification of Reactive and Concurrent Systems: Specification. Springer-Verlag New York, Inc. (1992)

    Google Scholar 

  27. Meinicke, L.A., Hayes, I.J.: Continuous Action System Refinement. In: Yu, H.-J. (ed.) MPC 2006. LNCS, vol. 4014, pp. 316–337. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  28. Moszkowski, B.C.: Compositional reasoning about projected and infinite time. In: ICECCS, pp. 238–245. IEEE Computer Society (1995)

    Google Scholar 

  29. Moszkowski, B.C.: A complete axiomatization of interval temporal logic with infinite time. In: LICS, pp. 241–252 (2000)

    Google Scholar 

  30. Rönkkö, M., Ravn, A.P., Sere, K.: Hybrid action systems. Theoretical Computer Science 290(1), 937–973 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  31. Wulf, M., Doyen, L., Markey, N., Raskin, J.-F.: Robust safety of timed automata. Form. Methods Syst. Des. 33, 45–84 (2008)

    Article  MATH  Google Scholar 

  32. Zhou, C., Hansen, M.R.: Duration Calculus: A Formal Approach to Real-Time Systems. EATCS: Monographs in Theoretical Computer Science. Springer (2004)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Information Technology and Electrical Engineering, The University of Queensland, Australia

    Brijesh Dongol & Ian J. Hayes

  2. Department of Computer Science, The University of Sheffield, UK

    Brijesh Dongol

Authors
  1. Brijesh Dongol
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ian J. Hayes
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Oxford University, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK

    Jeremy Gibbons

  2. Facultad de Informática, Universidad Politécnica de Madrid, Campus de Montegancedo s/n, 28660, Boadilla del Monte, Madrid, Spain

    Pablo Nogueira

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Dongol, B., Hayes, I.J. (2012). Deriving Real-Time Action Systems Controllers from Multiscale System Specifications. In: Gibbons, J., Nogueira, P. (eds) Mathematics of Program Construction. MPC 2012. Lecture Notes in Computer Science, vol 7342. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31113-0_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-31113-0_7

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-31112-3

  • Online ISBN: 978-3-642-31113-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation