[PDF] Formal Methods for Java - Lecture 8: Java Pathfinder

View - Download Formal Methods for Java - Lecture 8: Java Pathfinder

Previous PDF

Next PDF

Formal Methods for Java

Lecture 8: Java Pathnder

Jochen HoenickeSoftware Engineering

Albert-Ludwigs-University Freiburg

Nov 16, 2012

Jochen Hoenicke (Software Engineering)FM4JNov 16, 2012 1 / 21 Runtime checking vs. Model checking vs. Verication

Runtime CheckingJML Tools

VericationESC/Java2

KeY Jahob

Model CheckingJPF

Jochen Hoenicke (Software Engineering)FM4JNov 16, 2012 2 / 21

Java Pathnder (JPF)

Developed at NASA Ames Research Center

One tool { many dierent usage patterns

Highly extensible core

Core implements explicit state model checking on top of a Java VM

Key concepts:

Execution choices as transition breakers

State matching

Backtracking (restoring previous state)

Listeners, Properties, and Publishers

Jochen Hoenicke (Software Engineering)FM4JNov 16, 2012 3 / 21

History of JPF

1999

Sta rtas front end fo rthe Spin mo delcheck er.

.......................................................................2000Reimplementation as virtual machine

2003

Extension interfaces

2005

Op ensourced on Sourcefo rge

since 2008

P articipationin Go ogleSumme rof Co de

since 2009 Project, extensions, and wiki hosted on NASA servers (still open source) Jochen Hoenicke (Software Engineering)FM4JNov 16, 2012 4 / 21

Obtaining and Building JPF

Download fromhttp://babelfish.arc.nasa.gov/trac/jpfBinary builds not recommended since tool still evolves

Recommendation: use Mercurial repositories

> hg clone http://babelfish.arc.nasa.gov/hg/jpf/jpf-coreRepository contains everything needed to build jpf-core

> bin/antInstructions for Eclipse or NetBeans can be found in the JPF wiki Jochen Hoenicke (Software Engineering)FM4JNov 16, 2012 5 / 21

What We Got

Jochen Hoenicke (Software Engineering)FM4JNov 16, 2012 6 / 21

VM Inside a VM?

JPF is written in Java=)runs on a JVMJPF interprets Java Bytecode=)acts as a JVMJPF operates dierently:

Bytecode of System under Test (SUT) and

SUT-specic Conguration produce

a report and (possibly) some other artefacts (e.g., test cases) JPF might terminate the application if a property is violated Jochen Hoenicke (Software Engineering)FM4JNov 16, 2012 7 / 21

How to Congure JPF

JPF Conguration

Jochen Hoenicke (Software Engineering)FM4JNov 16, 2012 9 / 21

JPF Conguration Files

Basically Java properties les:

key=valueassignsvaluetokey# This is a comment

Extensions:

${x}expands to current value of variablexkey+=valueappendsvalueto the value ofkey

(No space betweenkeyand+=)+key=valueprependvalueto the value ofkey${config_path}expands to the directory of the currently parsed le${config}expands to the lename of the currently parsed le@using=loads projectproject-namefrom location

dened insite.propertieswith line =... Shortcut for class names: package prexgov.nasa.jpfcan be omittedConguration of JPF can be dicult Jochen Hoenicke (Software Engineering)FM4JNov 16, 2012 10 / 21

Conguring Our Compiled Version

Switch to your home directory

Create folder.jpfCreate le.jpf/site.properties

jpf.home = jpf-core = ${jpf.home}/jpf-core extensions = ${jpf-core}This creates the basic conguration

Add linejpf-proj = pathtosite.propertiesfor every

additional project you download Jochen Hoenicke (Software Engineering)FM4JNov 16, 2012 11 / 21

Conguring SuTs

Create conguration le (typically ends with.jpf)Content:

Some@usingdirectives (optionally)One linetarget = Optional arguments in a linetarget_args = Additional JPF and related project conguration (optional)

Optionalclasspathentry to locate the.classleOptionalsourcepathentry to locate the.javaleJochen Hoenicke (Software Engineering)FM4JNov 16, 2012 12 / 21

Demo Jochen Hoenicke (Software Engineering)FM4JNov 16, 2012 13 / 21

Insights into JPF

JPF Components

Jochen Hoenicke (Software Engineering)FM4JNov 16, 2012 15 / 21

JPF Core Architecture

Jochen Hoenicke (Software Engineering)FM4JNov 16, 2012 16 / 21

Explicit State Model Checking and JPF (1/3)

JVM Unies states, produces successor states, backtracks

Congurations:

vm.class

VM implementation

vm.insnfactoryinstruction facto ry vm.por apply pa rtialo rderreduction vm.por.syncdetectiondetect elds p rotectedb ylo cks vm.gc run ga rbagecollection vm.maxallocgcmaximal numb erof allo cationsb eforega rbage collection vm.treeoutputgenerate output fo rall e xploredpaths vm.pathoutputgenerate p rogramtrace output and many ,many mo re Jochen Hoenicke (Software Engineering)FM4JNov 16, 2012 17 / 21

Explicit State Model Checking and JPF (2/3)

Search

Selects next state to explore.

Congurations:

search.class sea rchimplementation search.depthlimitmaximal pa thlength search.matchdepthonly unify if depth fo rrevisit is lo werthan kno wn depth search.multipleerrorsdo not stop sea rchingat rst p ropertyviolation search.properties which p ropertiesto chec kduring sea rch further options fo reach se arch Jochen Hoenicke (Software Engineering)FM4JNov 16, 2012 18 / 21

Explicit State Model Checking and JPF (3/3)

Listener

Evaluate states against properties.

Listeners can in

uence current transition while properties cannot. Listener can monitor search and instruction execution. Own listener can be set with thelistenerconguration option.http://babelsh.arc.nasa.gov/trac/jpf/wiki Jochen Hoenicke (Software Engineering)FM4JNov 16, 2012 19 / 21

States

Collection ofthread state (current instruction, stack), global variables, heap references, and trail (path to the state) Jochen Hoenicke (Software Engineering)FM4JNov 16, 2012 20 / 21

Transitions

Sequence of instructions

End of transition determined by

Multiple successor states (choices)

Enforced by listeners (vm.breakTransition();)Reached maximal length (congurationvm.max_transition_length)End or blocking of current thread

Jochen Hoenicke (Software Engineering)FM4JNov 16, 2012 21 / 21quotesdbs_dbs45.pdfusesText_45

[PDF] séparation d'avec quelqu'un

[PDF] d'avec synonyme

[PDF] séparation d'avec ou avec

[PDF] divorce d'avec

[PDF] séparation amoureuse

[PDF] la séparation film

[PDF] séparation comment faire

[PDF] separation couple

[PDF] separation difficile

[PDF] séparation église état france

[PDF] examen algorithme 1ere année

[PDF] introduction générale sur l informatique

[PDF] informatique s4 smp pdf

[PDF] qcm langage c corrigé pdf

[PDF] informatique s4 pdf