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
Proving liveness properties of concurrent programs using petri-nets
Umeå University, Faculty of Science and Technology, Department of Computing Science.
2014 (English)Independent thesis Basic level (degree of Bachelor), 10 credits / 15 HE creditsStudent thesis
Abstract [en]

With the increased scale of distributed computations the complexity of liveness proofs have increased. In this paper we endeavor to simplify the process of verifying a concurrent system using well know modeling techniques. The choice of modeling tool as well as the proof is based on future scalability and automation. We translate the formal proof to a petri-net representation and use this to verify basic algorithms. We show that the formal proof of liveness stated by Owiki and Lamport can be adapted to petri-nets. We also show a modification to petri-nets for increased granularity in loop modeling. This is used to clarify the translation of the original proof to our petri-net representation. With these results we discuss the usefulness of our approach and compare it to other methods of ensuring liveness.

Place, publisher, year, edition, pages
2014.
Series
UMNAD, 989
National Category
Engineering and Technology
Identifiers
URN: urn:nbn:se:umu:diva-92803OAI: oai:DiVA.org:umu-92803DiVA: diva2:743458
Educational program
Bachelor of Science Programme in Computing Science
Supervisors
Examiners
Available from: 2014-09-04 Created: 2014-09-04 Last updated: 2014-09-04Bibliographically approved

Open Access in DiVA

fulltext(268 kB)110 downloads
File information
File name FULLTEXT01.pdfFile size 268 kBChecksum SHA-512
1827b3586dd52c9506a5621f91a0096c16e4041a9a3ec5d4ebae0ed0d5d47674c4f59585534f7f81123cdfdb02e0de1135533ed45c4af0fe67b91183b0066a86
Type fulltextMimetype application/pdf

By organisation
Department of Computing Science
Engineering and Technology

Search outside of DiVA

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