Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
The Many Faces of Complexity in Software Design Kapitel lesen Erstes Kapitel lesen

2012 | OriginalPaper | Buchkapitel

13. Modelling Temporal Behaviour in Complex Systems with Timebands

verfasst von : Kun Wei, Jim Woodcock, Alan Burns

Erschienen in: Conquering Complexity

Verlag: Springer London

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Vorheriges Kapitel Conquering Complexity via Seamless Integration of Design-Time and Run-Time Verification
Nächstes Kapitel Software and System Modeling: Structured Multi-view Modeling, Specification, Design and Implementation
Fußnoten
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.
 
Literatur
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
Metadaten
Titel
Modelling Temporal Behaviour in Complex Systems with Timebands
verfasst von
Kun Wei
Jim Woodcock
Alan Burns
Copyright-Jahr
2012
Verlag
Springer London
Buch
Conquering Complexity

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

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

Copyright-Jahr: 2012

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

Premium Partner

    Bildnachweise