is Íslenska en English

Lokaverkefni (Meistara) Háskólinn í Reykjavík > Tölvunarfræðideild > MSc verkefni >

Vinsamlegast notið þetta auðkenni þegar þið vitnið til verksins eða tengið í það: http://hdl.handle.net/1946/17446

Titill: 
  • Titill er á ensku Towards model checking BSV in Uppaal
  • Skilgreiningamál sem net tímaháðra stöðuvéla
Námsstig: 
  • Meistara
Leiðbeinandi: 
Útdráttur: 
  • Útdráttur er á ensku

    In recent years the complexity of hardware design for parallel processes has increased considerably. Despite advances in structural abstractions of description languages none has the ability to simulate reactive systems and model check in a graphical manner. In this thesis we argue for the viability of translating between two seemingly different languages, the high level hardware description language Bluespec SystemVerilog and the modelling language of Uppaal, an integrated environment for validating and verifying real time systems. We propose a scheme for mapping constructs between the two languages and provide a prototype of a translator from a shallow version of BSV to Uppaal.

  • Hönnun smárása hefur á síðari árum orðið sífellt flóknari. Líkön fyrir samsíða keyrslur hafa reynst sérlega erfið viðureignar og hönnunargalla hefur oftar en ekki fyrst orðið vart á framleiðslustigi rása eða við notkun þeirra. Þrátt fyrir framfarir í gerð skilgreiningamála gefur ekkert þeirra færi á myndrænni framsetningu við að greina líkön. Í þessari ritgerð leiðum við rök að því að þýða megi á milli skilgreiningamálsins Bluespec SystemVerilog (BSV) og Uppaal, sem er tæki til að sannreyna magþráða kerfi á myndrænan hátt og finna veikleika í hönnun þeirra. Sýnt er fram á að þýða megi milli þessara mála og sett er fram frumgerð að þýðanda sem þýðir úr einfaldaðri útgáfu af BSV yfir í líkanamál Uppaal.

Samþykkt: 
  • 11.3.2014
URI: 
  • http://hdl.handle.net/1946/17446


Skrár
Skráarnafn Stærð AðgangurLýsingSkráartegund 
MScThesis.pdf1.08 MBOpinnHeildartextiPDFSkoða/Opna