| Summary: | Software verification is a field of computer science dedicated to guar- antee that a program runs according to a formalized specification. Of various kinds of verification techniques model checking tries all possi- ble states of a program and makes sure each state satisfies a set of for- malized properties. Java Pathfinder (JPF) is a tool that automatically model checks Java bytecode. This report studies general configuration patterns for JPF that leads it to either terminate without errors or ter- minate with found concurrency bugs for different types of programs. The types considered are solutions to producer-consumer problems, barber shop problems, reader-writer problems and programs falling under the type server-client systems. The main part of the method is first a search for these types of programs using cloud-based revision control systems. Second, these programs are verified with the help of the JPF documentation, articles on the subject and online discus- sion groups. The results are configurations that lead to no errors, con- currency bugs and native method errors depending on the program verified. An important limitation of the report is the absence of large programs that challenge JPF’s state space handling. The resulting gen- eral configuration patterns found are applicable to small programs not using native methods. A pattern is also found for programs with na- tive methods, but here it is possible that the user must modify a model class in JPF. === Programverifikation är ett datalogiskt fält som säkerställer att pro- gram fungerar enligt en formaliserad specifikation. Modellkontroll är ett delområde i programverifikation som testar alla möjliga tillstånd i ett program för att se om de uppfyller en mängd formaliserade egen- skaper. Java Pathfinder (JPF) är ett verktyg som automatiskt kontrolle- rar bytekod i Java. Syftet med den här rapporten är att undersöka vil- ka generella konfigurationsmönster som finns för särskilda program- typer som leder till att JPF antingen terminerar utan fel eller med ett funnet samverkningsfel. Programtyperna som undersöks är lösningar till producer/consumer-problem, barber shop-problem, reader/wri- ter-problem och program som faller under typen server/klient-pro- gram. Metoden består i huvudsak först av sökning efter program i molnbaserade versionshanteringssystem. Sedan följer programkontroll med hjälp av JPF-dokumentation, artiklar om ämnet och diskussions- grupper online. Resultatet är ett antal konfigurationer som leder till inga fel, fel på grund av samtidig trådkörning och fel på grund av di- rekt körbar kod, beroende på det verifierade programmet. En viktig begränsning med rapporten är frånvaron av stora program som tes- tar JPFs hantering av stora tillståndsrymder. De funna generella kon- figurationerna är tillämpbara på små program som inte använder di- rekt körbar kod. En generell konfiguration hittades även för program som använder direkt körbar kod, men här måste användaren eventu- ellt skriva om en modellklass i JPF.
|
|---|
