uu.seUppsala University Publications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • 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
Extending a Real-Time Model-Checker to a Test-Case Generation Tool Using libCoverage
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology.
2008 (English)Independent thesis Advanced level (degree of Master (One Year)), 20 credits / 30 HE creditsStudent thesis
Abstract [en]

UPPAAL is a model-checker developed by the Department of Information Technology at Uppsala University in Sweden together with Aalborg University inDenmark. UPPAAL can be used to model, simulate, and verify timed automata. It has been used in many case studies since the first release in 1995.

libCoverage is a library developed at Uppsala University which can be used togenerate test-cases for real-time systems described as networks of timed automata. The test-cases are generated based upon a given coverage criteria, where the coverage criteria is specified by a parameterized observer automaton. The library is designed to extend model-checking tools, such as UPPAAL or SPIN.

The aim of this thesis is to extend UPPAAL 4.0 with libCoverage. For this purpose the grammar of the property file was extended to support libCoverage specific queries, and a modified reachability algorithm was presented which supports coverage exploration. We also extended each state with information about its current coverage, and implemented a wrapper which makes it possible for libCoverage to fetch information from UPPAAL about the system of timed automata.

In conclusion, we show that UPPAAL 4.0 can be extended with libCoverage tosupport test-case generation.

Place, publisher, year, edition, pages
2008.
Series
IT ; 08 005
Identifiers
URN: urn:nbn:se:uu:diva-89281OAI: oai:DiVA.org:uu-89281DiVA, id: diva2:159885
Presentation
(English)
Uppsok
Technology
Supervisors
Examiners
Available from: 2009-02-12 Created: 2009-02-10 Last updated: 2009-11-19Bibliographically approved

Open Access in DiVA

fulltext(6242 kB)449 downloads
File information
File name FULLTEXT01.pdfFile size 6242 kBChecksum SHA-512
fa63a6acfdf242d5c8c47e00b07ba63e803ed0f276f963864c0f5af897c8c6dbfa01f4c58ad48998ca0e81756a596ac5c362a4cac15f62a5559ad047a2be27fc
Type fulltextMimetype application/pdf

By organisation
Department of Information Technology

Search outside of DiVA

GoogleGoogle Scholar
Total: 449 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: 650 hits
CiteExportLink to record
Permanent link

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