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 implementation of model-checkers for networks of timed automata
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)
2000 (English)Licentiate thesis, monograph (Other academic)
Abstract [en]

Since real-time systems often operate in safety-critical environments it is extremely important that they function correctly. UPPAAL is a tool that can be used for validation and verification of real-time systems. The user models the system using networks of timed automata and uses a simple logic to express safety requirements that the modelled system must satisfy to guarantee its correct behaviour. UPPAAL then performs reachability analysis using constraint solving techniques to check if the model satisfies the given requirements. In addition, the tool is also able to provide the user with a sample execution that explains why a requirement is (or is not) satisfied by the model. The analysis is fully automated.

This thesis describes various techniques adopted when implementing UPPAAL. Some of the techniques have improved the performance of UPPAAL significantly. We have studied the techniques with performance measurements in several case-studies. One of the main contributions is the comparison of different strategies in implementing the basic data structures and searching algorithms. The measurements can be used as hints on what parts of the model-checker that are most important to optimise. Though the techniques are studied in the context of timed automata, we believe that they are applicable to the implementation of general software tools for automated analysis.

Place, publisher, year, edition, pages
Uppsala University, 2000.
Series
Information technology licentiate theses: Licentiate theses from the Department of Information Technology, ISSN 1404-5117 ; 2000-003
National Category
Computer Engineering
Research subject
Computer Systems
Identifiers
URN: urn:nbn:se:uu:diva-226511OAI: oai:DiVA.org:uu-226511DiVA, id: diva2:726158
Supervisors
Available from: 2000-05-30 Created: 2014-06-17 Last updated: 2018-01-11Bibliographically approved

Open Access in DiVA

fulltext(622 kB)104 downloads
File information
File name FULLTEXT01.pdfFile size 622 kBChecksum SHA-512
67cad30cafce24d00f46cbf2a44400d3c6e29002c9cff65121050fb6d7bb767a615bd3328bd4ff94c7a5e773ead9ceddcb178e65fcc6f1772f89a534024c7094
Type fulltextMimetype application/pdf

By organisation
Division of Computer SystemsComputer Systems
Computer Engineering

Search outside of DiVA

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