Rely/Guarantee Reasoning for Teleo-reactive Programs over Multiple Time Bands

  • Brijesh Dongol
  • Ian J. Hayes
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7321)


A complex real-time system consists of components at multiple time abstractions with varying notions of granularity and precision. Existing hybrid frameworks only allow reasoning at a single granularity and at an absolute level of precision, which can be problematic because the models that are developed can become unimplementable. In this paper, we develop a framework that incorporates time bands so that the behaviour of each component may be specified at a time granularity that is appropriate for the component and its properties. We implement our controllers using teleo-reactive programs, which are high-level programs that are well-suited to controlling reactive systems in dynamic environments. We develop rely/guarantee-style reasoning rules and as an example, prove properties of a well-known mine-pump system.


Hybrid Automaton Simple Program Time Granularity State Predicate Methane Level 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Broy, M.: Refinement of time. Theor. Comput. Sci. 253(1), 3–26 (2001)MathSciNetzbMATHCrossRefGoogle Scholar
  2. 2.
    Burns, A., Baxter, G.: Time bands in systems structure. In: Structure for Dependability, pp. 74–88. Springer (2006)Google Scholar
  3. 3.
    Burns, A., Hayes, I.J.: A timeband framework for modelling real-time systems. Real-Time Systems 45(1), 106–142 (2010)zbMATHCrossRefGoogle Scholar
  4. 4.
    Burns, A., Lister, A.M.: A framework for building dependable systems. Comput. J. 34(2), 173–181 (1991)CrossRefGoogle Scholar
  5. 5.
    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
  6. 6.
    Dongol, B., Hayes, I.J.: Deriving real-time action systems in a sampling logic. Sci. Comput. Program. (Special Issue of MPC 2010) (2012) (accepted October 17, 2011)Google Scholar
  7. 7.
    Dongol, B., Hayes, I.J., Robinson, P.J.: Reasoning about real-time teleo-reactive programs. Technical Report SSE-2010-01, The University of Queensland (2010)Google Scholar
  8. 8.
    Gargantini, A., Morzenti, A.: Automated deductive requirements analysis of critical systems. ACM Trans. Softw. Eng. Methodol. 10, 255–307 (2001)CrossRefGoogle Scholar
  9. 9.
    Gubisch, G., Steinbauer, G., Weiglhofer, M., Wotawa, F.: A Teleo-Reactive Architecture for Fast, Reactive and Robust Control of Mobile Robots. In: Nguyen, N.T., Borzemski, L., Grzech, A., Ali, M. (eds.) IEA/AIE 2008. LNCS (LNAI), vol. 5027, pp. 541–550. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  10. 10.
    Guelev, D.P., Hung, D.V.: Prefix and projection onto state in duration calculus. Electr. Notes Theor. Comput. Sci. 65(6), 101–119 (2002)CrossRefGoogle Scholar
  11. 11.
    Hayes, I.J., Burns, A., Dongol, B., Jones, C.: Comparing models of nondeterministic expression evaluation. Technical Report CS-TR-1273, Newcastle University (2011)Google Scholar
  12. 12.
    Henzinger, T.A.: The theory of hybrid automata. In: LICS 1996, pp. 278–292. IEEE Computer Society, Washington, DC (1996)Google Scholar
  13. 13.
    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)CrossRefGoogle Scholar
  14. 14.
    Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc., Boston (2002)Google Scholar
  15. 15.
    Manna, Z., Pnueli, A.: Temporal Verification of Reactive and Concurrent Systems: Specification. Springer-Verlag New York, Inc. (1992)Google Scholar
  16. 16.
    Montanari, A., Ratto, E., Corsetti, E., Morzenti, A.: Embedding time granularity in logical specifications of real-time systems. In: Euromicro 1991, pp. 88–97 (June 1991)Google Scholar
  17. 17.
    Moszkowski, B.C.: Compositional reasoning about projected and infinite time. In: ICECCS, pp. 238–245. IEEE Computer Society (1995)Google Scholar
  18. 18.
    Nilsson, N.J.: Teleo-reactive programs and the triple-tower architecture. Electronic Transactions on Artificial Intelligence 5, 99–110 (2001)Google Scholar
  19. 19.
    Rönkkö, M., Ravn, A.P., Sere, K.: Hybrid action systems. Theor. Comput. Sci. 290, 937–973 (2003)zbMATHCrossRefGoogle Scholar
  20. 20.
    Wei, K., Woodcock, J., Burns, A.: Formalising the timebands model in timed Circus. Technical report, University of York (June 2010)Google Scholar
  21. 21.
    Wulf, M., Doyen, L., Markey, N., Raskin, J.-F.: Robust safety of timed automata. Form. Methods Syst. Des. 33, 45–84 (2008)zbMATHCrossRefGoogle Scholar
  22. 22.
    Zhou, C., Hansen, M.R.: Duration Calculus: A Formal Approach to Real-Time Systems. EATCS: Monographs in Theoretical Computer Science. Springer (2004)Google Scholar
  23. 23.
    Zhou, C., Ravn, A.P., Hansen, M.R.: An Extended Duration Calculus for Hybrid Real-Time Systems. In: Grossman, R.L., Ravn, A.P., Rischel, H., Nerode, A. (eds.) HS 1991 and HS 1992. LNCS, vol. 736, pp. 36–59. Springer, Heidelberg (1993)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Brijesh Dongol
    • 1
    • 2
  • Ian J. Hayes
    • 1
  1. 1.School of Information Technology and Electrical EngineeringThe University of QueenslandAustralia
  2. 2.Department of Computer ScienceThe University of SheffieldUK

Personalised recommendations