Endre søk
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Algorithmic Analysis of Name-Bounded Programs: From Java programs to Petri Nets via π-calculus
Blekinge Tekniska Högskola, Fakulteten för datavetenskaper, Institutionen för programvaruteknik.
2014 (engelsk)Independent thesis Advanced level (degree of Master (Two Years))Oppgave
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.

sted, utgiver, år, opplag, sider
2014. , s. 94
Emneord [en]
pi-calculus, static verification, static analysis, concurrency, petri nets, name boundedness
HSV kategori
Identifikatorer
URN: urn:nbn:se:bth-3112Lokal ID: oai:bth.se:arkivexF8AA4208B7D62312C1257CC2005ED3EBOAI: oai:DiVA.org:bth-3112DiVA, id: diva2:830411
Uppsök
Technology
Veileder
Merknad
+49 151 52966429Tilgjengelig fra: 2015-04-22 Laget: 2014-04-22 Sist oppdatert: 2018-01-11bibliografisk kontrollert

Open Access i DiVA

fulltekst(479 kB)75 nedlastinger
Filinformasjon
Fil FULLTEXT01.pdfFilstørrelse 479 kBChecksum SHA-512
138e49ec3345630f2e1cf2e56e5544092cc6d989229881cc3a17735a8d97dd12359907f50e64ed8295f27e9ae43e240da5cb522e5ab8da97000c00b07d66966b
Type fulltextMimetype application/pdf

Av organisasjonen

Søk utenfor DiVA

GoogleGoogle Scholar
Totalt: 75 nedlastinger
Antall nedlastinger er summen av alle nedlastinger av alle fulltekster. Det kan for eksempel være tidligere versjoner som er ikke lenger tilgjengelige

urn-nbn

Altmetric

urn-nbn
Totalt: 65 treff
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf