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
A Petri Net based Modeling and Verification Technique for Real-Time Embedded Systems
Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory. Linköping University, The Institute of Technology.
2001 (English)Licentiate thesis, monograph (Other academic)
Abstract [en]

Embedded systems are used in a wide spectrum of applications ranging from home appliances and mobile devices to medical equipment and vehicle controllers. They are typically characterized by their real-time behavior and many of them must fulfill strict requirements on reliability and correctness.

In this thesis, we concentrate on aspects related to modeling and formal verification of realtime embedded systems.

First, we define a formal model of computation for real-time embedded systems based on Petri nets. Our model can capture important features of such systems and allows their representations at different levels of granularity. Our modeling formalism has a welldefined semantics so that it supports a precise representation of the system, the use of formal methods to verify its correctness, and the automation of different tasks along the design process.

Second, we propose an approach to the problem of formal verification of real-time embedded systems represented in our modeling formalism. We make use of model checking to prove whether certain properties, expressed as temporal logic formulas, hold with respect to the system model. We introduce a systematic procedure to translate our model into timed automata so that it is possible to use available model checking ools. Various examples, including a realistic industrial case, demonstrate the feasibility of our approach on practical applications.

Place, publisher, year, edition, pages
Institutionen för datavetenskap , 2001. , 115 p.
Series
Linköping Studies in Science and Technology. Thesis, ISSN 0280-7971 ; 919
Keyword [en]
Embedded systems, computer systems, real-time embedde systems, Petri nets, semantics
National Category
Computer Science
Identifiers
URN: urn:nbn:se:liu:diva-5751Local ID: LiU-Tek-Lic-2001:56ISBN: 91-7373-228-1 (print)OAI: oai:DiVA.org:liu-5751DiVA: diva2:21501
Presentation
(English)
Supervisors
Available from: 2002-10-17 Created: 2002-10-17 Last updated: 2009-11-25Bibliographically approved

Open Access in DiVA

fulltext(973 kB)2209 downloads
File information
File name FULLTEXT01.pdfFile size 973 kBChecksum MD5
3782f3418f39cad1aa1f91823d4b1051c72f4e150ea4ac215a2049fcb0b189b02aece4eb
Type fulltextMimetype application/pdf

Authority records BETA

Cortés, Luis Alejandro

Search in DiVA

By author/editor
Cortés, Luis Alejandro
By organisation
ESLAB - Embedded Systems LaboratoryThe Institute of Technology
Computer Science

Search outside of DiVA

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

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 464 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