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

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
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
Identifiers
URN: urn:nbn:se:liu:diva-9861ISRN: LITH-IDA/DS-EX-ING--07/004--SEOAI: oai:DiVA.org:liu-9861DiVA: diva2:24198
Uppsok
teknik
Examiners
Available from: 2007-10-09 Created: 2007-10-09

Open Access in DiVA

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

By organisation
Department of Computer and Information Science
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 1901 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

urn-nbn

Altmetric score

urn-nbn
Total: 319 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf