is Íslenska en English

Lokaverkefni (Meistara)

Háskólinn í Reykjavík > Tæknisvið / School of Technology > MSc Tölvunarfræðideild / Department of Computer Science >

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

Titill: 
  • Titill er á ensku Guided Search for Deadlocks in Actor-Based Models
  • Stýrð leit að sjálfheldum í gerandabundnum hugbúnaðarlíkönum
Námsstig: 
  • Meistara
Útdráttur: 
  • Útdráttur er á ensku

    The success of model checking is based on its ability to uncover errors in designs of software and protocols. Even a small reactive concurrent system can exhibit complex behavior. Such systems may have state-spaces larger than explicit state model checkers can verify. In practice, finding an error with a model checker is more useful than proving a property. Informed search algorithms use heuristic strategies with problem-specific knowledge to find solutions more efficiently than uninformed algorithms. Generally, such heuristics estimate the distance from a given state to a goal state. We present seven heuristics for guiding search algorithms through the state-space of actor-based models to a deadlock. Our methods can find a deadlock more efficiently than uninformed searches for some actor-based models. The A* search algorithm guarantees an optimal solution and returns the shortest counter-example. These methods are supported by a tool that performs directed model checking of the deadlock property. The objective is to detect difficult errors that might not be found by simulation or by conventional model checkers before reaching an upper bound or state-space explosion.

  • Árangur líkanaprófana liggur í hæfni þeirra til að sýna fram á villur í hönnun hugbúnaðar og samskiptastaðla. Jafnvel lítil gagnverkandi kerfi geta haft flókna hegðun. Sökum þess að vinnsluminni tölvunnar er takmarkað geta slík kerfi haft stöðurými sem er stærra en það sem mögulegt er að prófa. Þess vegna er ekki hægt að sannreyna réttmæti kerfisins með þeim hætti. Líkanaprófun kemur að mestu gagni þegar hún sýnir fram á áður óþekkta villu. Stýrðar leitaraðferðir nota brjóstvitsaðferðir til þess að stýra leitinni á hagkvæmari hátt en óstýrðar aðferðir gera. Almennt veita brjóstvitsaðferðir upplýsingar um fjarlægðina frá ákveðinni stöðu í þá markstöðu sem er næst henni. Við kynnum sjö brjóstvitsaðferðir sem geta stýrt leit, í gegnum leitartré gerandabundinna hugbúnaðarlíkana, að stöðu þar sem kerfið er í sjálfheldu. Leitir sem eru stýrðar af þessum aðferðum finna sjálfheldur fyrir sum líkön á hagkvæmari hátt en óstýrðar leitir. Með A* leit tryggjum við að ef lausn finnst þá er engin styttri lausn til í leitartrénu. Aðferðirnar eru útfærðar í hugbúnaði sem framkvæmir líkanaprófun fyrir sjálfheldur í gerandabundnum líkönum. Markmiðið er að finna erfiðar villur sem koma sjaldan upp og myndu hugsanlega ekki finnast með hermingu eða hefðbundnum líkana-\\prófunum áður en leitin nær efri mörkum vinnsluminnis.

Samþykkt: 
  • 16.6.2011
URI: 
  • http://hdl.handle.net/1946/9245


Skrár
Skráarnafn Stærð AðgangurLýsingSkráartegund 
MSc_Steinar_Hugi_Sigurdarson.pdf3.57 MBOpinnHeimildaskráPDFSkoða/Opna