liu.seSearch for publications in DiVA
Change search
ReferencesLink to record
Permanent link

Direct link
Verification and Scheduling Techniques for Real-Time Embedded Systems
Linköping University, Department of Computer and Information Science, ESLAB. Linköping University, The Institute of Technology.
2005 (English)Doctoral thesis, monograph (Other academic)
Abstract [en]

Embedded computer systems have become ubiquitous. They are used in a wide spectrum of applications, ranging from household appliances and mobile devices to vehicle controllers and medical equipment. This dissertation deals with design and verification of embedded systems, with a special emphasis on the real-time facet of such systems, where the time at which the results of the computations are produced is as important as the logical values of these results. Within the class of real-time systems two categories, namely hard real-time systems and soft real-time systems, are distinguished and studied in this thesis.

First, we propose modeling and verification techniques targeted towards hard real-time systems, where correctness, both logical and temporal, is of prime importance. A model of computation based on Petri nets is defined. The model can capture explicit timing information, allows tokens to carry data, and supports the concept of hierarchy. Also, an approach to the formal verification of systems represented in our modeling formalism is introduced, in which model checking is used to prove whether the system model satisfies its required properties expressed as temporal logic formulas. Several strategies for improving verification efficiency are presented and evaluated.

Second, we present scheduling approaches for mixed hard/soft real-time systems. We study systems that have both hard and soft real-time tasks and for which the quality of results (in the form of utilities) depends on the completion time of soft tasks. Also, we study systems for which the quality of results (in the form of rewards) depends on the amount of computation allotted to tasks. We introduce quasi-static techniques, which are able to exploit at low cost the dynamic slack caused by variations in actual execution times, for maximizing utilities/rewards and for minimizing energy.

Numerous experiments, based on synthetic benchmarks and realistic case studies, have been conducted in order to evaluate the proposed approaches. The experimental results show the merits and worthiness of the techniques introduced in this thesis and demonstrate that they are applicable on real-life examples.

Place, publisher, year, edition, pages
Institutionen för datavetenskap , 2005. , 213 p.
Linköping Studies in Science and Technology. Dissertations, ISSN 0345-7524 ; 920
Keyword [en]
Computer systems, Embedded computer systems, real-time systems
National Category
Computer Science
URN: urn:nbn:se:liu:diva-5023ISBN: 91-85297-21-6OAI: diva2:20956
Public defence
2005-03-02, Visionen, Hus B, Campus Valla, Linköpings universitet, Linköping, 10:15 (English)
Available from: 2005-03-23 Created: 2005-03-23

Open Access in DiVA

fulltext(1581 kB)1120 downloads
File information
File name FULLTEXT01.pdfFile size 1581 kBChecksum MD5
Type fulltextMimetype application/pdf

Search in DiVA

By author/editor
Cortés, Luis Alejandro
By organisation
ESLABThe Institute of Technology
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 1120 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 1046 hits
ReferencesLink to record
Permanent link

Direct link