Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
The Many Faces of Complexity in Software Design Read chapter Read first chapter

2012 | OriginalPaper | Chapter

13. Modelling Temporal Behaviour in Complex Systems with Timebands

Authors : Kun Wei, Jim Woodcock, Alan Burns

Published in: Conquering Complexity

Publisher: Springer London

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

Complex real-time systems exhibit dynamic behaviours on many different time levels. To cope with the wide range of time scales and produce more dependable computer-based systems, we develop a timebands model that can explicitly recognise a finite set of distinct time bands in which temporal properties and associated behaviours are described. We formalise the timebands model by using the semantics of TCSP M to guarantee soundness of each operator and maintain consistency and coordination between different time bands. By means of a complicated example, we demonstrate how significantly the timebands model contributes to describing complex real-time systems with multiple time scales.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Conquering Complexity via Seamless Integration of Design-Time and Run-Time Verification
next chapter Software and System Modeling: Structured Multi-view Modeling, Specification, Design and Implementation
Footnotes
1
Σ denotes the universal set of events.
 
2
These laws have been formally proved and the reader is referred to [31].
 
3
One of the approaches to model-check a timed CSP process is to translate it into an untimed CSP one in the form of timewise refinement [27]. This idea is quite powerful, but at the cost of dropping all WAIT d terms [24] because of the complexity of synchronising clock-tick events in parallel. However, the mechanism of local timers in our model does not require the synchronisation of all clock-tick events so as to avoid an unnecessary deadlock.
 
4
The clock-tick events are not directly given in this figure, whereas the reader can easily find out where these events should be placed by the description of the system.
 
Literature
1.
Roscoe A.W.: Model-checking CSP. In: A Classical Mind: Essays in Honour of C.A.R. Hoare. Prentice Hall, New York (1994). Chap. 21
2.
3.
Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking for real-time systems. In: LICS, pp. 414–425 (1990)
4.
Bettini, C., Dyreson, C.E., Evans, W.S., Snodgrass, R.T., Wang, X.S.: A glossary of time granularity concepts. In: Temporal Databases, Dagstuhl, pp. 406–413 (1997)
5.
Burns, A., Hayes, I.J.: A timeband framework for modelling real-time systems. Real-Time Syst. 45(1–2), 106–142 (2010) CrossRefMATH
6.
Burns, A., Lister, A.M.: A framework for building dependable systems. Comput. J. 34(2), 173–181 (1991) CrossRef
7.
Ciapessoni, E., Corsetti, E., Montanari, A., San Pietro, P.: Embedding time granularity in a logical specification language for synchronous real-time systems. In: 6IWSSD: Selected Papers of the Sixth International Workshop on Software Specification and Design, pp. 141–171. Elsevier, Amsterdam (1993)
8.
Clifford, J., Rao, A.: A simple, general structure for temporal domains. In: Temporal Aspects in Information Systems, pp. 23–30. AFCET, Paris (1987)
9.
Combi, C., Franceschet, M., Peron, A.: Representing and reasoning about temporal granularities. J. Log. Comput. 14(1), 51–77 (2004) CrossRefMATHMathSciNet
10.
Corsetti, E., Montanari, A., Ratto, E.: Time granularity in logical specifications. In: Proceedings of the 6th Italian Conference on Logic Programming, Pisa, Italy (1991)
11.
Dong, J.S., Hao, P., Qin, S., Sun, J., Yi, W.: Timed automata patterns. IEEE Trans. Softw. Eng. 34, 844–859 (2008) CrossRef
12.
Franceschet, M., Montanari, A.: Temporalized logics and automata for time granularity. Theory Pract. Log. Program. 4(5–6), 621–658 (2004) CrossRefMATHMathSciNet
13.
Group, T.R.L.: The RAISE Specification Language. Prentice Hall, Upper Saddle River (1993)
14.
Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall International, Englewood Cliffs (1985) MATH
15.
Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming. Prentice Hall International, Englewood Cliffs (1998)
16.
Hobbs, J.: Granularity. In: Proceedings of the Ninth International Joint Conference on Artificial Intelligence, Los Angeles, California, pp. 432–435 (1985)
17.
Holzmann, G.: Spin Model Checker, the Primer and Reference Manual. Addison-Wesley, Reading (2003)
18.
19.
Jifeng, H.: From CSP to hybrid systems. In: A Classical Mind: Essays in Honour of C.A.R. Hoare, pp. 171–189. Prentice Hall International, Hertfordshire (1994)
20.
Kramer, J., Magee, J., Sloman, M., Lister, A.: CONIC: an integrated approach to distributed computer control systems. IEE Proc. E, Comput. Digit. Tech. 130(1), 1–10 (1983) CrossRef
21.
Cardellini, V., Casalicchio, E., Grassi, V., Lo Presti, F., Mirandola, R.: Uppaal—a tool suite for automatic verification of real-time systems. In: Hybrid Systems III. LNCS, vol. 1066, pp. 232–243. Springer, Berlin (1995)
22.
Lynch, N., Vaandrager, F.: Action transducers and timed automata. In: Formal Aspects of Computing, pp. 436–455. Springer, Berlin (1992)
23.
Montanari, A., Ratto, E., Corsetti, E., Morzenti, A.: Embedding time granularity in logical specifications of real-time systems. In: Proceedings of the Third Euromicro Workshop on Real-Time Systems, Paris, France (1991)
24.
Ouaknine, J., Schneider, S.: Timed CSP: a retrospective. Electron. Notes Theor. Comput. Sci. 162, 273–276 (2006) CrossRef
25.
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall International, Englewood Cliffs (1998)
26.
Sampaio, A., Woodcock, J., Cavalcanti, A.: Refinement in Circus. In: FME ’02, pp. 451–470. Springer, London (2002)
27.
Schneider, S.: Timewise refinement for communicating processes. Sci. Comput. Program. 28, 43–90 (1997) CrossRefMATH
28.
Schneider, S.A.: Concurrent and Real-Time Systems: The CSP Approach. Wiley, New York (1999)
29.
Sherif, A., He, J.: Towards a time model for Circus. In: ICFEM ’02: Proceedings of the 4th International Conference on Formal Engineering Methods, pp. 613–624. Springer, London (2002)
30.
31.
32.
Wei, K., Woodcock, J., Burns, A.: A timed model of Circus with the reactive design miracle. In: 8th International Conference on Software Engineering and Formal Methods (SEFM), pp. 315–319, IEEE Comput. Soc., Pisa (2010). CrossRef
33.
Woodcock, J., Cavalcanti, A.: The semantics of Circus. In: ZB ’02: Proceedings of the 2nd International Conference of B and Z Users on Formal Specification and Development in Z and B, pp. 184–203. Springer, London (2002) CrossRef
34.
Woodcock, J., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice Hall, Upper Saddle River (1996) MATH
35.
Yong, X., George, C.: An operational semantics for timed RAISE. In: FM ’99: Proceedings of the Wold Congress on Formal Methods in the Development of Computing Systems—Volume II, pp. 1008–1027. Springer, London (1999)
36.
Zeyda, F., Cavalcanti, A.: Mechanical reasoning about families of UTP theories. Electron. Notes Theor. Comput. Sci. 240, 239–257 (2009) CrossRef
Metadata
Title
Modelling Temporal Behaviour in Complex Systems with Timebands
Authors
Kun Wei
Jim Woodcock
Alan Burns
Copyright Year
2012
Publisher
Springer London
Book
Conquering Complexity

Print ISBN: 978-1-4471-2296-8

Electronic ISBN: 978-1-4471-2297-5

Copyright Year: 2012

DOI
https://doi.org/10.1007/978-1-4471-2297-5_13

Premium Partner

    Image Credits