Model checking is a technique used to verify whether a model meets a given specification by exhaustively and automatically checking each reachable state in the model. It is a well-developed technique, but it suffers from some issues, perhaps most importantly the state space explosion problem. Models may contain so many states that must be checked means that the model checking procedure may be intractable. In this thesis we investigate whether procedure summaries can be used to improve the performance of model checking. Procedure summaries are concise representations of parts of a program, such as a function or method. We present a design and an implementation of dynamically generated summaries as an extension of Java PathFinder, a virtual machine executing Java bytecode that is able to model check programs written in Java by backtracking execution, to explore different schedulings etc. We find that our summaries incur an overhead that outweighs the benefits in most cases, but the approach shows promise in certain cases, in particular when stateless model checking is used. We also provide some statistics related to cases when our summaries are applicable that could provide guidance for future work within this field. / Model checking, eller modellkontroll, är en välkänd teknik inom programverifikation som används för att verifiera att en modell, ofta av ett program, uppfyller en given specifikation genom att undersöka alla nåbara tillstånd i modellen. Det är en välutvecklad teknik som lider av några brister, en av de viktigaste är det så kallade state space explosion-problemet. Modellerna kan bestå av så många olika tillstånd att \textit{model checking} inte går att använda. I den här rapporten undersöker vi om vi kan tillämpa så kallade procedur-sammanfattningar för att förbättra prestandan av model checking. Procedur-sammanfattningar är representationer av delar av program, till exempel metoder eller funktioner. Vi presenterar en design och implementation av dynamiskt genererade sammanfattningar i form av ett tillägg till Java PathFinder, en virtuell maskin som exekverar Java bytecode som kan utföra model checking genom att backa körningar för att till exempel utforska olika schemaläggningar. Våra procedur-sammanfattningar har i många fall en negativ effekt på körtid, men visar på lovande resultat i vissa fall, i synnerhet när så kallad stateless model checking används. Vi presenterar också resultat kopplat till fall när våra sammanfattningar är applicerbara som kan leda vägen för fortsatt arbete inom området.
| Identifer | oai:union.ndltd.org:UPSALLA1/oai:DiVA.org:kth-231433 |
| Date | January 2018 |
| Creators | Berglund, Lasse |
| Publisher | KTH, Teoretisk datalogi, TCS |
| Source Sets | DiVA Archive at Upsalla University |
| Language | English |
| Detected Language | Swedish |
| Type | Student thesis, info:eu-repo/semantics/bachelorThesis, text |
| Format | application/pdf |
| Rights | info:eu-repo/semantics/openAccess |
| Relation | TRITA-EECS-EX ; 2018:323 |
Page generated in 0.0077 seconds