Abstract
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.
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.
References
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)
David, A.: Uppaal2k: Small Tutorial. Documentation to the verification tool Uppaal2k, http://www.docs.uu.se/docs/rtmv/uppaal/
Buttazzo, G.C.: Hard Real-Time Computing Systems: Predictable Scheduling Algorithms and Applications. Kluwer Academic Publishers, Boston (1997)
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)
Graham, R.L.: Bounds on multiprocessing timing anomalies. SIAM Journal on Applied Mathematics 17, 416–429 (1969)
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)
Liu, J.W.S.: Real-time systems. Prentice-Hall, Inc., Upper Saddle River (2000) ISBN 0-13-099651-3
Shaw, A.: Reasoning about time in higher-level language software. IEEE Transactions on Software Engineering 15 (July 1989)
Corbett, J.C.: Timing analysis of Ada tasking programs. IEEE Transactions on Software Engineering 22(7), 461–483 (1996)
Cassez, F., Larsen, K.: The Impressive Power of Stopwatches. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, p. 138. Springer, Heidelberg (2000)
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)
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)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Waszniowski, L., Hanzalek, Z. (2004). Analysis of Real Time Operating System Based Applications. In: Larsen, K.G., Niebert, P. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2003. Lecture Notes in Computer Science, vol 2791. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-40903-8_18
Download citation
DOI: https://doi.org/10.1007/978-3-540-40903-8_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21671-1
Online ISBN: 978-3-540-40903-8
eBook Packages: Springer Book Archive