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
Modeling and formal verification of embedded systems based on a Petri net representation
Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
2003 (English)In: Journal of systems architecture, ISSN 1383-7621, E-ISSN 1873-6165, Vol. 49, no 12-15, 571-598 p.Article in journal (Refereed) Published
Abstract [en]

In this paper we concentrate on aspects related to modeling and formal verification of embedded systems. First, we define a formal model of computation for embedded systems based on Petri nets that can capture important features of such systems and allows their representation at different levels of granularity. Our modeling formalism has a well-defined 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 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 tools. We propose two strategies for improving the verification efficiency, the first by applying correctness-preserving transformations and the second by exploring the degree of parallelism characteristic to the system. Some examples, including a realistic industrial case, demonstrate the efficiency of our approach on practical applications. © 2003 Elsevier B.V. All rights reserved.

Place, publisher, year, edition, pages
2003. Vol. 49, no 12-15, 571-598 p.
Keyword [en]
Embedded systems, Formal verification, Model checking, Modeling, Petri nets
National Category
Engineering and Technology
Identifiers
URN: urn:nbn:se:liu:diva-46395DOI: 10.1016/S1383-7621(03)00096-1OAI: oai:DiVA.org:liu-46395DiVA: diva2:267291
Available from: 2009-10-11 Created: 2009-10-11 Last updated: 2017-12-13

Open Access in DiVA

No full text

Other links

Publisher's full textLink to full-text

Authority records BETA

Cortes, Luis-AlejandroEles, Petru IonPeng, Zebo

Search in DiVA

By author/editor
Cortes, Luis-AlejandroEles, Petru IonPeng, Zebo
By organisation
The Institute of TechnologyESLAB - Embedded Systems Laboratory
In the same journal
Journal of systems architecture
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 133 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