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
Formal Coverification of Embedded 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)In: 26th Euromicro Conference Digital Systems Design,2000, Maastricht, The Netherlands: IEEE Computer Society Press , 2000, 106-113 vol.1 p.Conference paper, Published paper (Refereed)
Abstract [en]

The complexity of embedded systems is increasing rapidly. In consequence, new verification techniques that overcome the limitations of traditional methods and are suitable for hardware/software systems are needed. In this paper we introduce a computational model for embedded systems based on Petri nets, called PRES. We present an approach to coverification of both the hardware and software parts of an embedded system represented by PRES. We use symbolic model checking to prove the correctness of such systems, specifying properties in CTL and verifying whether they are satisfied. This coverification method permits to reason formally about design properties as well as timing requirements. A medical monitoring system illustrates the feasibility of our approach on practical applications.

Place, publisher, year, edition, pages
Maastricht, The Netherlands: IEEE Computer Society Press , 2000. 106-113 vol.1 p.
Keyword [en]
formal verification, PRES, petri nets, modeling, hardware software co-design
National Category
Computer Science
Identifiers
URN: urn:nbn:se:liu:diva-23387DOI: 10.1109/EURMIC.2000.874622Local ID: 2827ISBN: 0-7695-0780-8 (print)OAI: oai:DiVA.org:liu-23387DiVA: diva2:243701
Conference
26th Euromicro Conference, 05-07 September 2000, Maastricht, Netherlands
Note

vol. I proceeding

Available from: 2009-10-07 Created: 2009-10-07 Last updated: 2015-01-22

Open Access in DiVA

No full text

Other links

Publisher's full texthttp://www.ida.liu.se/labs/eslab/publications/pap/db/EUROMICRO00.pdf

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
Computer Science

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

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