Model Checking of Multitasking Real-Time Applications Based on the Timed Automata Model Using One Clock

View Sample PDF

Author(s): Libor Wasziwoski (Czech Technical University, Czech Republic)and Zdenek Hanzalek (Czech Technical University, Czech Republic)
Copyright: 2010
Pages: 25
Source title: Behavioral Modeling for Embedded Systems and Technologies: Applications for Design and Implementation
Source Author(s)/Editor(s): Luís Gomes (Universidade Nova de Lisboa, Portugal)and João M. Fernandes (Universidade do Minho, Portugal)
DOI: 10.4018/978-1-60566-750-8.ch008

Keywords: Computer Science & IT / Information Science Reference / Systems & Software Design / Systems and Software Engineering

Purchase

View Model Checking of Multitasking Real-Time Applications Based on the Timed Automata Model Using One Clock on the publisher's website for pricing and purchasing information.

Abstract

The aim of this chapter is to show how a multitasking real-time application running under a real-time operating system can be modeled by timed automata. The application under consideration consists of several preemptive tasks and interrupts service routines that can be synchronized by events and can share resources. A real-time operating system compliant with an OSEK/VDX standard is considered for demonstration. A model checking tool UPPAAL is used to verify time and logical properties of the proposed model. Since the complexity of the model-checking verification exponentially grows with the number of clocks used in a model, the proposed model uses only one clock for measuring execution time of all modeled tasks.

The IRMA Community

Research IRM

Model Checking of Multitasking Real-Time Applications Based on the Timed Automata Model Using One Clock

Purchase

Abstract

Related Content

IRMA Sponsors