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, id: 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)114 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: 114 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: 215 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