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

Direct link
Instrumentation of timed automata for formal verification of timed properties
Linköping University, Department of Computer and Information Science.
2007 (English)Independent thesis Basic level (professional degree), 10 points / 15 hpStudent thesis
Abstract [en]

Embedded systems are used in many technical products of today. The tendency also points to the fact that they are in many ways becoming more and more complex as technology advances. Systems like advanced avionics, air bags, ABS brakes or any real-time embedded system requires reliability, correctness and timeliness. This puts hard pressure on designers, analyzers and developers. The need for high performance and non failing systems has therefore led to a growing interest in modeling and verification of component-based embedded systems in order to reduce costs and simplify design and development. The solution proposed by the Embedded Systems Lab at Linköping University is the modeling language PRES+, Petri Net based Representation for Embedded Systems.

PRES+ models are then translated into timed automata, TA, which is used by the UPPAAL verification tool. To be able to verify timing properties the translated TA model must be instrumented with certain timers, called clocks. These clocks must be reset in a manner reflected by the property to be verified.

This thesis will provide a solution to the problem and also give the reader necessary information in order to understand the theoretical background needed. The thesis will also show the reader the importance of modeling and time verification in the development of embedded systems. A simple example is used to describe and visualize the benefit regarding real-time embedded systems as well as the importance of the ability to verify these systems.

The conclusion drawn stresses the fact that high development costs, possible gain of human lives and the problems in developing complex systems only emphasize the need for easy to handle and intuitive verification methods.

Place, publisher, year, edition, pages
Institutionen för datavetenskap , 2007. , 33 p.
Keyword [en]
Embedded systems, formal verification, Petri Net, PRES+, Timed Automata
National Category
Computer Science
URN: urn:nbn:se:liu:diva-9861ISRN: LITH-IDA/DS-EX-ING--07/004--SEOAI: diva2:24198
Available from: 2007-10-09 Created: 2007-10-09

Open Access in DiVA

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

By organisation
Department of Computer and Information Science
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 1728 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: 299 hits
ReferencesLink to record
Permanent link

Direct link