Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • 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
Verification of Heterogeneous Electronic Systems using Model Checking
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.
2000 (English)Report (Other academic)
Abstract [en]

The ever increasing complexity of heterogeneous electronic systems consisting of hardware and software components poses a challenge in verifying their correctness. The complexity of this kind of systems is such, that traditional validation methods, like simulation and testing, are not enough to verify their correctness. In consequence, new verification methods that over-come the limitations of traditional techniques and, at the same time, are suitable for heteroge-neous hardware/software systems are needed. In this report we formally define the semantics of PRES+, a Petri net based computational model aimed to represent embedded systems. We introduce an approach to formal verification of heterogeneous electronic systems: we make use of model checking to prove the correctness of such systems by determining the truth of CTL and TCTL formulas that specify required properties with respect to a PRES+ model. Thus verification with timing properties is possible. An ATM server illustrates the feasibility of this approach on practical applications. This work has been done in the frame of the SAVE project, which aims to study the specification and verification of heterogeneous electronic systems.

Place, publisher, year, edition, pages
Linköping, Sweden: IDA, Linköpings Universitet , 2000.
Series
SAVE Project Report
Keyword [en]
formal verification, model checking, PRES+, petri nets, hardware software co-design, heterogeneous embedded systems, real-time systems
National Category
Computer Science
Identifiers
URN: urn:nbn:se:liu:diva-23389Local ID: 2830OAI: oai:DiVA.org:liu-23389DiVA: diva2:243703
Available from: 2009-10-07 Created: 2009-10-07

Open Access in DiVA

No full text

Other links

http://www.ida.liu.se/labs/eslab/publications/pap/db/SAVE00.pdf

Search in DiVA

By author/editor
Cortes, Luis-AlejandroEles, Petru IonPeng, Zebo
By organisation
The Institute of TechnologyESLAB - Embedded Systems Laboratory
Computer Science

Search outside of DiVA

GoogleGoogle Scholar

urn-nbn

Altmetric score

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

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • 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