uu.seUppsala universitets publikasjoner
Endre søk
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association
  • 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
Zone-Based Reachability Analysis of Dense-Timed Pushdown Automata
Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi.
2012 (engelsk)Independent thesis Basic level (degree of Bachelor), 10 poäng / 15 hpOppgave
Abstract [en]

Proving that programs behave correctly is a matter of both great theoretical interest as well as practical use. One way to do this is by analyzing a model of the system in question in order to determine if it meets a given specification. Real-time recursive systems can be modeled by dense-timed pushdown automata, a model which combines the behaviours of classical timed automata and pushdown automata. The problem of reachability has been proven to be decidable for this model. The algorithm that solves this problem relies on constructing a classical pushdown automaton that mimics the behaviour of a given timed pushdown automaton by means of an abstraction that uses regions as a symbolic representation  of states. The drawback of this approach is that the untimed automaton produced generally contains a very large number of states. This report  proposes a method of generalizing this abstraction by using zones instead of regions, in order to minimize the number of states in the untimed automaton.

sted, utgiver, år, opplag, sider
2012.
Serie
IT ; 12 034
HSV kategori
Identifikatorer
URN: urn:nbn:se:uu:diva-179802OAI: oai:DiVA.org:uu-179802DiVA, id: diva2:546296
Utdanningsprogram
Bachelor Programme in Computer Science
Uppsök
Technology
Veileder
Examiner
Tilgjengelig fra: 2012-08-23 Laget: 2012-08-23 Sist oppdatert: 2012-08-23bibliografisk kontrollert

Open Access i DiVA

fulltext(749 kB)440 nedlastinger
Filinformasjon
Fil FULLTEXT01.pdfFilstørrelse 749 kBChecksum SHA-512
ec4dc5024e91e852007f2c612633ed143f1885aa34750075f14addaa70f3d8c9299c7076c786d16568c5a1c8c64ce8e1b35c975cd998ed0e95fda9fd0ae03788
Type fulltextMimetype application/pdf

Av organisasjonen

Søk utenfor DiVA

GoogleGoogle Scholar
Totalt: 440 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: 756 treff
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association
  • 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