Blast Model Checker 6l1m1d

BLAST MODEL CHECKER

COURSE NAME : FORMAL METHODS COURSE CODE : SIM 5104 GIRUBALANI D/O GARNARAJAN (GS35502) NURSAKINAH (GS39392) LECTURER : DR. PATHIAH ABDUL SAMAD  

WHAT

IS MODEL CHECHER? WHAT IS BLAST ? CONSTRAINS PROGRAM ANALYSIS WITH BLAST BLAST FEATURES ISSUE WITH BLAST

WHAT IS MODEL CHECHER • Model checking is about testing whether the given model of hardware or software meets specification • There are three essential steps in the model checking process:• Modeling • Specification • Verification

MODELING : Design of a system translated into a mathematical form.

SPECIFICATION : Properties of the system that we would like to check

model checking process

VERIFICATION : Checked for the specified properties

WHAT

IS MODEL CHECHER? WHAT IS BLAST ? CONSTRAINS BLAST FEATURES PROGRAM ANALYSIS WITH BLAST ISSUE WITH BLAST

WHAT IS BLAST ? The

Berkeley Lazy Abstraction Softwareverification Tool is a model checker that checks the safety properties of C programs.

“Automated,

precise and scalable” (so,

usable). The

first version of BLAST was developed at UC Berkeley by Ranjit Jhala, Rupak Majumdar, and Gregoire Sutre and was ed by the US National Science Foundation

WHAT IS BLAST ? It

is an automatic verification tool for checking temporal safety properties of C programs.

 Temporal

logics are an automatic verification technique commonly employed for finite state concurrent systems.

The

goal of BLAST is to be able to check that software satisfies behavioral properties of the interfaces it uses.

WHAT IS BLAST ? BLAST

uses counterexampledriven automatic abstraction refinement to construct an abstract model which is model checked for safety properties.

BLAST

is written in OCaml and uses CIL(C Intermediate Language) library to parse and preprocess the input source code.

WHAT

IS MODEL CHECHER? WHAT IS BLAST ? CONSTRAINS BLAST FEATURES PROGRAM ANALYSIS WITH BLAST ISSUE WITH BLAST

CONSTRAINS Only

tested it on Intel Pentium processors under Linux and Microsoft Windows with Cygwin Installing and making it work Predicate discovery not good enough Checking concurrent programs Eclipse plugin Checking recursive functions

WHAT

IS MODEL CHECHER? WHAT IS BLAST ? CONSTRAINS BLAST FEATURES PROGRAM ANALYSIS WITH BLAST ISSUE WITH BLAST

BLAST Features “

On the Fly” Abstraction Automatic Abstraction Smarter predicate discovery  safety properties, assertion violations Finding reachable program location Detecting dead code Reuse saved abstraction

WHAT

IS MODEL CHECHER? WHAT IS BLAST ? CONSTRAINS BLAST FEATURES PROGRAM ANALYSIS WITH BLAST ISSUE WITH BLAST

PROGRAM ANALYSIS WITH BLAST Build

an abstract model using predicate abstraction Check for reachability of specified label using the abstract model If no path to ERR node-system safe If path is feasible, output error trace Else use infeasibility of path to

PROGRAM ANALYSIS WITH BLAST The

BLAST toolkit can be used for many different analyses.

Blast

constructs, explores, and refines abstractions of the program state space based on lazy predicate abstraction and interpolation-based predicate discovery.

The

most common are

 Reachability Checking  Assertion Checking  Correct Locking

Reachability Checking verifies

whether the special label ERROR is reachable in the source code e.g.

Figure 1: Reachability Checking Example

Assertion Checking Reachability

analysis can be used for checking assertions statically in the source code. Can be verified with BLAST by using assert.h header that comes with the toolkit. E.g.

Figure 2: Assertion Checking as Reachability

Correct Locking  For

concurrent programs it is important to have shared resources protected from non synchronized access.  That is, when the thread will access a shared resource it must first acquire a lock.  After finishing with the resources the thread must release the lock.  Thus locking and unlocking actions should be done in an alternating sequence

FIGURE 3: Locking as Reachability

WHAT

IS MODEL CHECHER? WHAT IS BLAST ? CONSTRAINS BLAST FEATURES PROGRAM ANALYSIS WITH BLAST ISSUE WITH BLAST

ISSUE WITH BLAST Pointer

analysis capabilities are still not sophisticated enough Pointer analysis (alias analysis) is a rather expensive component of static analysis Pointer analysis capabilities are lacking for proving safety in many cases cryptic uninformative error messages required manual rewriting and simplification of the input source code until the tool accepted it

Conclusion The techniques of model checking are  cleverly employed in the BLAST program  analyzer which is a scalable and efficient  model checker for C language programs.