onr:"swepub:oai:DiVA.org:liu-5751"
Sökning: onr:"swepub:oai:DiVA.org:liu-5751" > A Petri Net based M...
- 1 av 1
- Föregående post
- Nästa post
- Till träfflistan
A Petri Net based Modeling and Verification Technique for Real-Time Embedded Systems
-
- Cortés, Luis Alejandro, 1971- (författare)
- Linköpings universitet,ESLAB - Laboratoriet för inbyggda system,Tekniska högskolan
-
- Peng, Zebo, Professor (preses)
- Linköpings universitet,ESLAB - Laboratoriet för inbyggda system,Tekniska högskolan
-
- Eles, Petru, Professor (preses)
- Linköpings universitet,ESLAB - Laboratoriet för inbyggda system,Tekniska högskolan
- (creator_code:org_t)
- ISBN 9173732281
- Institutionen för datavetenskap, 2001
- Engelska 115 s.
- Serie: Linköping Studies in Science and Technology. Thesis, 0280-7971 ; 919
- Licentiatavhandling (övrigt vetenskapligt/konstnärligt)
Abstract
Ämnesord
Stäng
- 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.
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Nyckelord
- Embedded systems
- Computer systems
- Real-time embedded systems
- Petri nets
- Semantics
- Computer science
- Datavetenskap
Publikations- och innehållstyp
- vet (ämneskategori)
- lic (ämneskategori)
Hitta via bibliotek
- A Petri Net based Modeling and Verification Technique for Real-Time Embedded Sys... (Sök publikationen i LIBRIS)
Till lärosätets databas
- 1 av 1
- Föregående post
- Nästa post
- Till träfflistan
Hitta mer i SwePub
- Av författaren/redakt...
- Cortés, Luis Ale ...
- Peng, Zebo, Prof ...
- Eles, Petru, Pro ...
- Om ämnet
-
- NATURVETENSKAP
- NATURVETENSKAP
- och Data och informa ...
- och Datavetenskap
- Delar i serien
- Linköping Studie ...
- Av lärosätet
- Linköpings universitet
Sök utanför SwePub
- Sök vidare i:
- Google Book Search
- Google Scholar
Kungliga biblioteket hanterar dina personuppgifter i enlighet med EU:s dataskyddsförordning (2018), GDPR. Läs mer om hur det funkar här.
Så här hanterar KB dina uppgifter vid användning av denna tjänst.
- Copyright © LIBRIS - Nationella bibliotekssystem
- LIBRIS.kb.se
