Elementi di Software Dependability - Software Safety

Software safety - DEF-STAN 00-55

• “Where safety is dependent on the safety related

software (SRS) fully meeting its requirements,

demonstrating safety is equivalent to

demonstrating correctness with respect to the

Software Requirement”.

Ultimate problems addressable by model

checking

• Checking correctness of the code running on the application

- Two main approaches:

(Software Model Checking)

– Code Model Checking

– Model Based Development

• Checking safety of the system (the system never runs into

an unsafe state)

– Concentrating on safety properties on a Model of the system

– Opening to probabilistic safety

Software Model Checking

• Although the early papers on model checking

focused on software, not many applications to prove

the correctness of code, until 1997

• Until 1997 most work was on software designs

– Finding bugs early is more cost-effective

– Reality is that people write code first, rather than design

• Only later the harder problem of analyzing actual

source code was first attempted

• Pioneering work at NASA

Software Model Checking

Most model checkers cannot directly deal with the

features of modern programming languages

• Bringing programs to model checking

– Translation to a standard Model Checker

• Bringing model checking to programs

– Ad hoc model checkers that directly deal with programs as

input

In both cases, need of Abstraction.

• © Willem Visser 2002

Abstraction

Model Checker

Program Input

void add(Object o) {

buffer[head] = o;

head = (head+1)%size;

}

Object take() {

…

tail=(tail+1)%size;

return buffer[tail];

}

Possibly infinite state Finite state

Abstraction

• Model checkers don’t take real programs as input

• Model checkers typically work on finite state systems

Abstraction cuts the state space size to something

• manageable

• Abstraction eliminates details irrelevant to the property

• Disadvantage: Loss of Precision: False positives/negatives

• Abstraction comes in three flavors

more behaviors

– Over-approximations, i.e. are added to the

abstracted system than are present in the original

less behaviors

– Under-approximations, i.e. are present in the

abstracted system than are present in the original

the same behaviors

– Precise abstractions, i.e. are present in the

abstracted and original program

Under-Approximation

“Meat-Axe” Abstraction

• Remove parts of the program considered “irrelevant” for the

property being checked, e.g.

– Limit input values to 0..10 rather than all integer values

– Queue size 3 instead of unbounded, etc.

• The abstraction of choice in the early applications of

software model checking

• Used during the translation of code to a model checker’s

input language

• Typically manual, no guarantee that only the irrelevant

behaviors are removed.

Precise abstraction © Willem Visser 2002

• Precise abstraction, w.r.t. the property being checked, may be obtained if

the behaviors being removed are indeed not influencing the property

slicing

– Program is an example of an automated under-approximation that

will to a precise abstraction w.r.t. the property being checked

lead Property-directed Slicing

indirectly

relevant Slice

mentioned Source program Resulting slice

in property

• slicing criterion generated automatically from observables mentioned in the property

• backwards slicing automatically finds all components that might influence the observables.

Over-Approximations

Abstract Interpretation

• Maps sets of states in the concrete program to

one state in the abstract program

– Reduces the number of states, but increases the number

of possible transitions, and hence the number of

behaviors

– Can in rare cases lead to a precise a