Che materia stai cercando?

Elementi di Software Dependability - Software Safety

Appunti di Elementi di Software Dependability - Software Safety. Nello specifico gli argomenti trattati sono i seguenti: Ultimate problems addressable by model checking, Checking correctness of the code running on the application, Checking safety of the system, ecc.

Esame di Elementi di Software Dependability docente Prof. U. Monile

Anteprima

ESTRATTO DOCUMENTO

© Willem Visser 2002

Predicate Abstraction

Replace predicates in the program by boolean variables, and replace each

instruction that modifies the predicate with a corresponding instruction

that modifies the boolean.

T F

Abstract EQ = T EQ := F EQ = F

int int bool

" : # EQ (x = y)

EQ (x = y) $

$

Concrete x y x y

= ! y++

x = 0 x = 0

y = 0 y = 1

Mapping of a concrete system to an abstract system, whose states

• correspond to truth values of a set of predicate

• Create abstract state-graph during model checking, or,

• Create an abstract transition system before model checking

How do we Abstract Behaviors?

• Abstract domain A

– Abstract concrete values to those in A

• Then compute transitions in the abstract

domain

– Over-approximations: Add extra behaviors

– Under-approximations: Remove actual behaviors

Underlying model: Kripke Structures

• M = (S,s ,%>,L) on AP

0

S: Set of States

! s : Initial State

! 0 Transition Relation

! ->:

L: S 2 , Labeling on States

AP

! ->

Simulations on Kripke Structures

M = (S, s , L)

->,

0

M’ = (S’, s’ , L’)

->’,

0

Definition: R S S’ is a simulation relation

& #

M M’

between and iff

(s,s’) R implies

'

1. L(s) = L’(s’)

2. for all t s.t. s t ,

(

exists t’ s.t. s’ t’ and

(’

(t,t’) R.

'

M’ simulates M (M M’) iff (s , t ) R

~ '

0 0

M

Intuitively, every transition in can be matched by some

M’

transition in

Preservation of properties by the

Abstraction

• M concrete model, M’ abstract model

Strong Preservation:

• – M’ P iff M P

|= |=

Weak Preservation:

• – M’ P M P

|= => |=

Simulation

• preserves ACTL* properties

– If M M’ then M’ AG p M AG p

~ |= => |=

Abstraction Homomorphisms

• Concrete States S, Abstract states S’

• Abstraction function (Homomorphism)

– h: S S’

->

– Induces a partition on S equal to size of S’

• Existential Abstraction - Over-Approximation

– Make a transition from an abstract state if at least one

corresponding concrete state has the transition.

– Abstract model M’ simulates concrete model M

• Universal Abstraction - Under-Approximation

– Make a transition from an abstract state if all the

corresponding concrete states have the transition.

Existential Abstraction -

Preservation

Let be a Universally quantified formula (es, an ACTL*

)

property)

M’ existentially abstracts M, so M ~ M’

Preservation Theorem

M’ M

) ( )

|= |=

Converse does not hold

M’ M

|= |=

) )

(

counterexample may be spurious

M’ :

|= )

NOTE: ACTL* is the universal fragment of CTL*

Universal Abstraction -

Preservation

Let be a existential-quantified property (i.e., expressed in

)

ECTL*) and M simulates M’

Preservation Theorem

M’ M

|= ) ( |= )

Converse does not hold

M M’

|= f |= f

(

NOTE: ECTL* is the universal fragment of CTL*

Model Checking (safety)

I AG ~ unsafe (true property)

= unsafe state

Abstraction:

Under-Approximation

I

AG ~ unsafe true (but it is not preserved)

Abstraction:

Over-Approximation

I It is not a path in the

concrete system

spurious

AG ~ unsafe false counterexample

Refinement of the abstraction :

I

Separate states that are the reason of AG ~ unsafe true

the spurious counterexample

Automated Abstraction/Refinement

• Counterexample-Guided AR (CEGAR) M’:= abstract(M)

– Build an abstract model M’

– Model check property P, M’ P?

|= No Bug

T

M’ |= P

– If M’ P, then M P by Preservation

|= |=

Theorem F

– Otherwise, check if Counterexample (CE) F

spurious(CE) Bug

is spurious T

– Refine abstract state space using CE M’:= refine(M’)

analysis results

– Repeat Hand-Translation

© Willem Visser 2002

Early applications at NASA

• Remote Agent – Havelund,Penix,Lowry 1997

– http://ase.arc.nasa.gov/havelund

– Translation from Lisp to Promela (most effort)

– Heavy abstraction

– 3 man months et al.

• DEOS – Penix, Visser, 1998/1999

– http://ase.arc.nasa.gov/visser

– C++ to Promela (most effort in environment generation)

– Limited abstraction - programmers produced sliced system

– 3 man months

© Willem Visser 2002

Semi-Automatic Translation

• Table-driven translation and abstraction

– Feaver system by Gerard Holzmann

– User specifies code fragments in C and how to translate them

to Promela (SPIN)

– Translation is then automatic

– Found 75 errors in Lucent’s PathStar system

– http://cm.bell-labs.com/cm/cs/who/gerard/

• Advantages

– Can be reused when program changes

– Works well for programs with long development and only local

changes

© Willem Visser 2002

Fully Automatic Translation

• Advantage

– No human intervention required

• Disadvantage

– Limited by capabilities of target system

• Examples

– Java PathFinder 1- http://ase.arc.nasa.gov/havelund/jpf.html

• Translates from Java to Promela (Spin)

– JCAT - http://www.dai-arc.polito.it/dai-arc/auto/tools/tool6.shtml

• Translates from Java to Promela (or dSpin)

– Bandera - http://www.cis.ksu.edu/santos/bandera/

• Translates from Java bytecode to Promela, SMV or dSpin

Bringing Model Checking to Programs

• Allow model checkers to take programming languages as

input, (or notations of similar expressive power)

• Major problem: how to encode the state of the system

efficiently

• Alternatively state-less model checking

– No state encoding or storing

On the fly

– model checking

• Almost exclusively explicit-state model checking

• Abstraction can still be used as well

– Source to source abstractions

Custom-made Model Checkers

• Translation based

– dSpin

• Spin extended with dynamic constructs

• Essentially a C model checker

• Source-2-source abstractions can be supported

• http://www.dai-arc.polito.it/dai-arc/auto/tools/tool7.shtml

– SPIN Version 4

• PROMELA language augmented with C code

• Table-driven abstractions

– Bandera

• Translated Bandera Intermediate Language (BIR) to a

number of back-end model checkers, but, a new BIR custom-

made model checker is under development

• Supports source-2-source abstractions as well as property-

specific slicing

• http://www.cis.ksu.edu/santos/bandera/


PAGINE

20

PESO

421.57 KB

AUTORE

Sara F

PUBBLICATO

+1 anno fa


DETTAGLI
Corso di laurea: Corso di laurea in ingegneria informatica
SSD:
Università: Firenze - Unifi
A.A.: 2013-2014

I contenuti di questa pagina costituiscono rielaborazioni personali del Publisher Sara F di informazioni apprese con la frequenza delle lezioni di Elementi di Software Dependability e studio autonomo di eventuali libri di riferimento in preparazione dell'esame finale o della tesi. Non devono intendersi come materiale ufficiale dell'università Firenze - Unifi o del prof Monile Umberto.

Acquista con carta o conto PayPal

Scarica il file tutte le volte che vuoi

Paga con un conto PayPal per usufruire della garanzia Soddisfatto o rimborsato

Recensioni
Ti è piaciuto questo appunto? Valutalo!

Altri appunti di Elementi di software dependability

Elementi di Software Dependability
Appunto
Elementi di Software Dependability -Interpretazione Astratta
Appunto
Elementi di Software Dependability -Interpretazione Astratta – Verifica codice
Dispensa
Elementi di Software Dependability - Formal Methods in Practice
Dispensa