Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • 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
Algorithmic Analysis of Name-Bounded Programs: From Java programs to Petri Nets via π-calculus
Blekinge Institute of Technology, Faculty of Computing, Department of Software Engineering.
2014 (English)Independent thesis Advanced level (degree of Master (Two Years))Student thesis
Abstract [en]

Context. Name-bounded analysis is a type of static analysis that allows us to take a concurrent program, abstract away from it, and check for some interesting properties, such as deadlock-freedom, or watching the propagation of variables across different components or layers of the system. Objectives. In this study we investigate the difficulties of giving a representation of computer programs in a name-bounded variation of π-calculus. Methods. A preliminary literature review is conducted to assess the presence (or lack thereof) of other successful translations from real-world programming languages to π-calculus, as well for the presence of relevant prior art in the modelling of concurrent systems. Results. This thesis gives a novel translation going from a relevant subset of the Java programming language, to its corresponding name-bounded π-calculus equivalent. In particular, the strengths of our translation are being able to dispose of names representing inactive objects when there are no circular references, and a transparent handling of polymorphism and dynamic method resolution. The resulting processes can then be further transformed into their Petri-Net representation, enabling us to check for important properties, such as reachability and coverability of program states. Conclusions. We conclude that some important properties that are not, in general, easy to check for concurrent programs, can be in fact be feasibly determined by giving a more constrained model in π-calculus first, and as Petri Nets afterwards.

Place, publisher, year, edition, pages
2014. , 94 p.
Keyword [en]
pi-calculus, static verification, static analysis, concurrency, petri nets, name boundedness
National Category
Information Systems Software Engineering
Identifiers
URN: urn:nbn:se:bth-3112Local ID: oai:bth.se:arkivexF8AA4208B7D62312C1257CC2005ED3EBOAI: oai:DiVA.org:bth-3112DiVA: diva2:830411
Uppsok
Technology
Supervisors
Note
+49 151 52966429Available from: 2015-04-22 Created: 2014-04-22 Last updated: 2015-06-30Bibliographically approved

Open Access in DiVA

fulltext(479 kB)35 downloads
File information
File name FULLTEXT01.pdfFile size 479 kBChecksum SHA-512
138e49ec3345630f2e1cf2e56e5544092cc6d989229881cc3a17735a8d97dd12359907f50e64ed8295f27e9ae43e240da5cb522e5ab8da97000c00b07d66966b
Type fulltextMimetype application/pdf

By organisation
Department of Software Engineering
Information SystemsSoftware Engineering

Search outside of DiVA

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

Total: 32 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • 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