Change search
ReferencesLink to record
Permanent link

Direct link
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
URN: urn:nbn:se:bth-3112Local ID: diva2:830411
+49 151 52966429Available from: 2015-04-22 Created: 2014-04-22 Last updated: 2015-06-30Bibliographically approved

Open Access in DiVA

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

By organisation
Department of Software Engineering
Information SystemsSoftware Engineering

Search outside of DiVA

GoogleGoogle Scholar
Total: 20 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: 30 hits
ReferencesLink to record
Permanent link

Direct link