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
Efficient symbolic state exploration of timed systems: Theory and implementation
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems. (Embedded Systems)
2001 (English)Licentiate thesis, comprehensive summary (Other academic)
Abstract [en]

Timing aspects are important for the correctness of safety-critical systems. It is crucial that these aspects are carefully analysed in designing such systems. UPPAAL is a tool designed to automate the analysis process. In UPPAAL, a system under construction is described as a network of timed automata and the desired properties of the system can be specified using a query language. Then UPPAAL can be used to explore the state space of the system description to search for states violating (or satisfying) the properties. If such states are found, the tool provides diagnostic information, in form of executions leading to the states, to help the desginers, for example, to locate bugs in the design.

The major problem for UPPAAL and other tools for timed systems to deal with industrial-size applications is the state space explosion. This thesis studies the sources of the problem and develops techniques for real-time model checkers, such as UPPAAL, to attack the problem. As contributions, we have developed the notion of committed locations to model atomicity and local-time semantics for timed systems to allow partial order reductions, and a number of implementation techniques to reduce time and space consumption in state space exploration. The techniques are studied and compared by case studies. Our experiments demonstrate significant improvements on the performance of UPPAAL.

Place, publisher, year, edition, pages
Uppsala University, 2001.
Series
Information technology licentiate theses: Licentiate theses from the Department of Information Technology, ISSN 1404-5117 ; 2001-009
National Category
Computer Engineering
Research subject
Computer Systems
Identifiers
URN: urn:nbn:se:uu:diva-86016OAI: oai:DiVA.org:uu-86016DiVA, id: diva2:116825
Supervisors
Available from: 2001-05-22 Created: 2008-11-11 Last updated: 2018-01-13Bibliographically approved

Open Access in DiVA

fulltext(601 kB)160 downloads
File information
File name FULLTEXT01.pdfFile size 601 kBChecksum SHA-512
4dd685f0276775545b535e110607184b71eeb69f50dc32b5d30fb95ead96752b246ac6cb6ce841867bdba4d18ac8a8366ab0152150daea821943b16e7d4704a9
Type fulltextMimetype application/pdf

By organisation
Division of Computer SystemsComputer Systems
Computer Engineering

Search outside of DiVA

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

urn-nbn

Altmetric score

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