Analysis of Real Time Operating System Based Applications

  • Libor Waszniowski
  • Zdenek Hanzalek
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2791)


This text is dedicated to modelling of real-time applications running under multitasking operating system. Theoretical background is based on timed automata by Alur and Dill. As this approach is not suited for modelling pre-emption we focus on cooperative scheduling. In the addition, interrupt service routines are considered, and their enabling/disabling is controlled by interrupt server considering the specified server capacity. The server capacity has influence on the margins of the computation times in the application processes. Such systems, used in practical real-time applications, can be modelled by timed automata and further verified since their reachability problem and model checking of TCTL problem is decidable. Use of this methodology is demonstrated on the case study.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    David, A.: Uppaal2k: Small Tutorial. Documentation to the verification tool Uppaal2k,
  3. 3.
    Buttazzo, G.C.: Hard Real-Time Computing Systems: Predictable Scheduling Algorithms and Applications. Kluwer Academic Publishers, Boston (1997)zbMATHGoogle Scholar
  4. 4.
    Sha, L., Klein, M., Goodenough, J.: Rate Monotonic Analysis for Real-Time Systems. In: Foundations of Real-Time Computing: Scheduling and Resource Management, pp. 129–155. Kluwer Academic Publishers, Boston (1991)Google Scholar
  5. 5.
    Graham, R.L.: Bounds on multiprocessing timing anomalies. SIAM Journal on Applied Mathematics 17, 416–429 (1969)zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    Larsen, K.G., Pettersson, P., Yi, W.: Model-Checking for Real-Time Systems. In: Reichel, H. (ed.) FCT 1995. LNCS, vol. 965, pp. 62–88. Springer, Heidelberg (1995)Google Scholar
  7. 7.
    Liu, J.W.S.: Real-time systems. Prentice-Hall, Inc., Upper Saddle River (2000) ISBN 0-13-099651-3Google Scholar
  8. 8.
    Shaw, A.: Reasoning about time in higher-level language software. IEEE Transactions on Software Engineering 15 (July 1989)Google Scholar
  9. 9.
    Corbett, J.C.: Timing analysis of Ada tasking programs. IEEE Transactions on Software Engineering 22(7), 461–483 (1996)CrossRefGoogle Scholar
  10. 10.
    Cassez, F., Larsen, K.: The Impressive Power of Stopwatches. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, p. 138. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  11. 11.
    Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? Journal of Computer and System Sciences 57, 94–124 (1998)zbMATHCrossRefMathSciNetGoogle Scholar
  12. 12.
    Bouyer, P., Dufourd, C., Fleury, E., Petit, A.: Are Timed Automata Updatable? In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 464–479. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  13. 13.
    Fersman, E., Pettersson, P., Yi, W.: Timed Automata with Asynchronous Processes: Schedulability and Decidability. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 67–82. Springer, Heidelberg (2002)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Libor Waszniowski
    • 1
  • Zdenek Hanzalek
    • 1
  1. 1.Department of Control EngineeringCzech Technical University Centre for Applied CyberneticsPrague 2Czech Republic

Personalised recommendations