Analysis of Real Time Operating System Based Applications
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.
- 2.David, A.: Uppaal2k: Small Tutorial. Documentation to the verification tool Uppaal2k, http://www.docs.uu.se/docs/rtmv/uppaal/
- 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
- 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.Liu, J.W.S.: Real-time systems. Prentice-Hall, Inc., Upper Saddle River (2000) ISBN 0-13-099651-3Google Scholar
- 8.Shaw, A.: Reasoning about time in higher-level language software. IEEE Transactions on Software Engineering 15 (July 1989)Google Scholar