Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Broy, M.: Refinement of time. Theor. Comput. Sci. 253(1), 3–26 (2001)
Burns, A., Baxter, G.: Time bands in systems structure. In: Structure for Dependability, pp. 74–88. Springer (2006)
Burns, A., Hayes, I.J.: A timeband framework for modelling real-time systems. Real-Time Systems 45(1), 106–142 (2010)
Burns, A., Lister, A.M.: A framework for building dependable systems. Comput. J. 34(2), 173–181 (1991)
Dongol, B., Hayes, I.J.: Approximating idealised real-time specifications using time bands. In: AVoCS 2011. ECEASST, vol. 46, pp. 1–16. EASST (2012)
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)
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)
Gargantini, A., Morzenti, A.: Automated deductive requirements analysis of critical systems. ACM Trans. Softw. Eng. Methodol. 10, 255–307 (2001)
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)
Guelev, D.P., Hung, D.V.: Prefix and projection onto state in duration calculus. Electr. Notes Theor. Comput. Sci. 65(6), 101–119 (2002)
Hayes, I.J., Burns, A., Dongol, B., Jones, C.: Comparing models of nondeterministic expression evaluation. Technical Report CS-TR-1273, Newcastle University (2011)
Henzinger, T.A.: The theory of hybrid automata. In: LICS 1996, pp. 278–292. IEEE Computer Society, Washington, DC (1996)
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)
Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc., Boston (2002)
Manna, Z., Pnueli, A.: Temporal Verification of Reactive and Concurrent Systems: Specification. Springer-Verlag New York, Inc. (1992)
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)
Moszkowski, B.C.: Compositional reasoning about projected and infinite time. In: ICECCS, pp. 238–245. IEEE Computer Society (1995)
Nilsson, N.J.: Teleo-reactive programs and the triple-tower architecture. Electronic Transactions on Artificial Intelligence 5, 99–110 (2001)
Rönkkö, M., Ravn, A.P., Sere, K.: Hybrid action systems. Theor. Comput. Sci. 290, 937–973 (2003)
Wei, K., Woodcock, J., Burns, A.: Formalising the timebands model in timed Circus. Technical report, University of York (June 2010)
Wulf, M., Doyen, L., Markey, N., Raskin, J.-F.: Robust safety of timed automata. Form. Methods Syst. Des. 33, 45–84 (2008)
Zhou, C., Hansen, M.R.: Duration Calculus: A Formal Approach to Real-Time Systems. EATCS: Monographs in Theoretical Computer Science. Springer (2004)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dongol, B., Hayes, I.J. (2012). Rely/Guarantee Reasoning for Teleo-reactive Programs over Multiple Time Bands. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds) Integrated Formal Methods. IFM 2012. Lecture Notes in Computer Science, vol 7321. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-30729-4_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-30729-4_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-30728-7
Online ISBN: 978-3-642-30729-4
eBook Packages: Computer ScienceComputer Science (R0)