Formal verification of multitasking applications based on timed automata model

• Alur R, Dill DL (1994) A theory of timed automata. Theor Comput Sci 126:183–235

  Article  MATH  MathSciNet  Google Scholar 

• Alur R, Henzinger TA, Vardi MY (1993) Parametric real-time reasoning. In: Proceedings of the 25th ACM symposium on theory of computing, pp 592–601

• Alvarez JM, Diaz M, Lopis L, Pimentel E, Troya JM (2003) Integrating schedulability analysis and design techniques in SDL. Real-Time Syst 24:267–302

  Article  MATH  Google Scholar 

• Bailey CM, Burns A, Wellings AJ, Forsyth CH (1995) A performance analysis of a hard real-time system. Control Eng Pract 3(4):447–464

  Article  Google Scholar 

• Berard B, Bidoit M, Finkel A, Laroussinie F, Petit A, Petrucci L, Schnoebelen P, McKenzie P (2001) Systems and software verification: model-checking techniques and tools. Springer, New York

  MATH  Google Scholar 

• Bucci G, Fedeli A, Sassoli L, Vicario E (2004) Timed state space analysis of real-time preemptive systems. IEEE Trans Softw Eng 30(2):97–111

  Article  Google Scholar 

• Buttazzo G (1997) Hard real-time computing systems: predictable scheduling algorithms and applications. Kluwer Academic, Boston

  MATH  Google Scholar 

• Campos S, Clarke E (1999) Analysis and verification of real-time systems using quantitative symbolic algorithms. J Softw Tools Technol Transf 2(3):260–269

  Article  MATH  MathSciNet  Google Scholar 

• Corbett JC (1996) Timing analysis of Ada tasking programs. IEEE Trans Softw Eng 22(7):461–483

  Article  Google Scholar 

• Daws C, Olivero A, Tripakis S, Yovine S (1996) The tool kronos. In: Proceedings of hybrid systems III, verification and control. Lecture notes in computer science, vol 1066. Springer, New York, pp 208–219

  Google Scholar 

• Fersman E, Pettersson P, Yi W (2002) Timed automata with asynchronous processes: schedulability and decidability. In: Proceedings of 8th international conference on tools and algorithms for the construction and analysis of systems, TACAS 2002. Lecture notes in computer science, vol 2280. Springer, New York, pp 67–82

  Chapter  Google Scholar 

• Fersman E, Pettersson P, Yi W (2003) Schedulability analysis using two clocks. In: Proceedings of TACAS’03. Lecture notes in computer science, vol 2619. Springer, New York, pp 224–239

  Google Scholar 

• Fredette AN, Cleaveland R (1993) RTSL: a language for real-time schedulability analysis. In: Proceedings of the real-time systems symposium. IEEE Computer Society Press, pp 274–283

• González Harbour M, Gutiérrez García JJ, Palencia Gutiérrez JC, Drake Moyano JM (2001) MAST: modeling and analysis suite for real time applications. In: Proceedings of 13th euromicro conference on real-time systems, Delft, The Netherlands. IEEE Computer Society Press, pp 125–134, June

• Henzinger T, Kopke P, Puri A, Varaiya P (1998) What’s decidable about hybrid automata? J Comput Syst Sci 57:94–124

  Article  MATH  MathSciNet  Google Scholar 

• Klein M, Ralya T, Pollak B, Obenza R, Harbour MG (1993) A practitioner’s handbook for real-time systems analysis. Kluwer Academic, Dordrecht

  Google Scholar 

• Krákora J, Waszniowski L, Píša P, Hanzálek Z (2004) Timed automata approach to real time distributed system verification. In: Proceedings of 5th IEEE international workshop on factory communication systems, WFCS, Vienna, September 22–24, 2004, pp 407–410

• Krčál P, Yi W (2004) Decidable and undecidable problems in schedulability analysis using timed automata. In: Proceedings of TACAS’04. Lecture notes in computer science, vol 2988. Springer, New York, pp 236–250

  Google Scholar 

• Larsen KG, Pettersson P, Yi W (1995) Model-checking for real-time systems. In: Proceedings of the 10th international conference on fundamentals of computation theory. Lecture notes in computer science, vol 965. Springer, New York, pp 62–88

  Google Scholar 

• Larsen KG, Petterson P, Yi W (1997) UPPAAL in a nutshell. Int J Softw Tools Technol Transf 1(1/2):134–152

  MATH  Google Scholar 

• Larsen KG, Larson F, Pettersson P, Yi W (2003) Compact data structures and state-space reduction for model-checking real-time systems. Real-Time Syst 25:255–275

  Article  MATH  Google Scholar 

• Lime D, Roux OH (2004) A translation based method for the timed analysis of scheduling extended time Petri nets. In: Proceedings of the 25th IEEE international real-time systems symposium, December 2004, Lisbon, Portugal, pp 187–196

• Liu JWS (2000) Real-time systems. Prentice-Hall, Upper Saddle River

  Google Scholar 

• Lundqvist K, Asplund L (2003) A ravenscar-compliant run-time kernel for safety-critical systems. Real-Time Syst J 24(1):29–54

  Article  MATH  Google Scholar 

• OSEK (2005) OSEK/VDX operating system specification 2.2.3, http://www.osek-vdx.org/

• Palencia JC, Harbour G (1998) Schedulability analysis for tasks with static and dynamic offsets. In: Proceedings of the 19th IEEE real-time systems symposium. IEEE Computer Society Press, p 26

• Sha L, Klein M, Goodenough J (1991) Rate monotonic analysis for real-time systems. In: Foundations of real-time computing: scheduling and resource management. Kluwer Academic, Boston, pp 129–155

  Google Scholar 

• Tindell K, Clark J (1994) Holistic schedulability analysis for distributed hard real-time systems. Microprocess Microprogram 50(2–3):117–134

  Article  Google Scholar 

• Wang S, Tsai G (2004) Specification and timing analysis of real-time systems. Real-Time Syst 28:69–90

  Article  MATH  Google Scholar 

• Waszniowski L, Hanzálek Z (2005) Over-approximate model of multitasking application based on timed automata using only one clock. In: Proceedings 19th IEEE international parallel and distributed processing symposium IPDPS 2005 (Workshop 2: parallel and distributed real-time systems). IEEE Computer Society, p 128

Download references