, Chap 1
1 Introduction to critical
. systems design
Different types of critical systems
1 .
Safety-critical : failure may endanger human life
2
. Security-critical :
failure means non-authorized access to /alteration
of sensitive info.
. Business-critical
3 ( quality critical)
= : cost of failure is
very high
2 means to attain dependability
Fault prevention
&
Dependability Security Fault toluance
Availability Reliability Safety Confidentiality Integrity Maintenability
Dependability >
- ability to deliver a service that can
justifiably be trusted
Security - absence of unauthorized access to ,
or
handling of , system state + service only available to authorized users
Fault- defect in hardware (HW) device/component or in software (SW) component >
-
bit-flip in memory/broken transistor
Error -
direct consequence of fault
Failure - system does not perform according to its requirements due to the presence
of one or more evors
. Validation
2 and Verification -
methods and practices Availability fraction of : time system
Check correctness --
use formal methods (notion of state & transition UML is operational
MTTF
>
- use formal verification A =
*
100 %
↳ MTTF + RTTR
algorithmic veif (model checking
↳
deductive reif (theorem proving MTTF >
- mean Time to Failure
↳
analytic techniques (schedulability analysis MTTR
+ mean time to repair
System correctness :
1
. Functional properties :
logic of the app is correct
2
. Non functional :
timing energy , ,
reliability evolutivity
...
,
No
verification method is all : automatic/powerfull/ round/complete/scalable
Validation >
-
System/component satisfies specified requirements
Verification - product of a
given development phase satisfy conditions imposed at the start
Certification >
- written
quarantee that a system or component complies with its specified requirements and is acceptable for
operational use
Design Assurance Levels (DAL) >
-
the
severity of a failure determines the DAL level of a function . Impose thresholds on
the probability of occurrence for each DAL lev.
el
TQ) = Tool Qualification Level from 1
(highest) to 5 /lowest
↳
impact of a tool in the software life cycle processes & combined with resultingnoftware level to define applicableTQL
, Common Means
of Verification & Validation,
Review / inspection by peers
·
Simulation : execute and monitor a model of the system
Formal methods : formal modeling + formal verification -
> proof of properties of the specification and possible proofs of correctness of
implementat
·
Risk analysis : hazards and causes , proba of occurring
...
·
Testing : test cases on
prototypes
Static analysis : defects by examining source code without execution
Fault
injection in HW & SW ,
simulation based
fault-injection
Testing vs
formal verification
Tests = check execution
according to some
coverage .
scheme
↳ when evas but don't prove no .
evors
·
Formal verification applies on models not at run-time
↳
help reduce nb
of tests & help generate sequence of tests to be performed
Warning -
model is abstraction >
- make
simplifying assumptions
Formal methods in critical systems
1
. Safety-critical - failure may endanger human life
.
2 Security-critical - failure means non-authorized access to sensitive info
. Business-critical
3 (quality critical) - cost failure is
high
Safety standards & crification - incentive for formal methods
standards fortransportations systems & medical devices -> formal methods.
Best practices of VOV
·
raif start as
early as possible
venf invisible to users ,
automated and integrated in Model-Driven Development flows
coss-validation between techniques/tools
models and assumptions should be questioned and checked against measurements
Formal method : theorem
puring (deductive veif (
System ->
set
of axioms
("things we assume are true")
properties on the specification >
-
theorems to prove
+ powerful and allow parametric reif
.
X complex
1 Introduction to critical
. systems design
Different types of critical systems
1 .
Safety-critical : failure may endanger human life
2
. Security-critical :
failure means non-authorized access to /alteration
of sensitive info.
. Business-critical
3 ( quality critical)
= : cost of failure is
very high
2 means to attain dependability
Fault prevention
&
Dependability Security Fault toluance
Availability Reliability Safety Confidentiality Integrity Maintenability
Dependability >
- ability to deliver a service that can
justifiably be trusted
Security - absence of unauthorized access to ,
or
handling of , system state + service only available to authorized users
Fault- defect in hardware (HW) device/component or in software (SW) component >
-
bit-flip in memory/broken transistor
Error -
direct consequence of fault
Failure - system does not perform according to its requirements due to the presence
of one or more evors
. Validation
2 and Verification -
methods and practices Availability fraction of : time system
Check correctness --
use formal methods (notion of state & transition UML is operational
MTTF
>
- use formal verification A =
*
100 %
↳ MTTF + RTTR
algorithmic veif (model checking
↳
deductive reif (theorem proving MTTF >
- mean Time to Failure
↳
analytic techniques (schedulability analysis MTTR
+ mean time to repair
System correctness :
1
. Functional properties :
logic of the app is correct
2
. Non functional :
timing energy , ,
reliability evolutivity
...
,
No
verification method is all : automatic/powerfull/ round/complete/scalable
Validation >
-
System/component satisfies specified requirements
Verification - product of a
given development phase satisfy conditions imposed at the start
Certification >
- written
quarantee that a system or component complies with its specified requirements and is acceptable for
operational use
Design Assurance Levels (DAL) >
-
the
severity of a failure determines the DAL level of a function . Impose thresholds on
the probability of occurrence for each DAL lev.
el
TQ) = Tool Qualification Level from 1
(highest) to 5 /lowest
↳
impact of a tool in the software life cycle processes & combined with resultingnoftware level to define applicableTQL
, Common Means
of Verification & Validation,
Review / inspection by peers
·
Simulation : execute and monitor a model of the system
Formal methods : formal modeling + formal verification -
> proof of properties of the specification and possible proofs of correctness of
implementat
·
Risk analysis : hazards and causes , proba of occurring
...
·
Testing : test cases on
prototypes
Static analysis : defects by examining source code without execution
Fault
injection in HW & SW ,
simulation based
fault-injection
Testing vs
formal verification
Tests = check execution
according to some
coverage .
scheme
↳ when evas but don't prove no .
evors
·
Formal verification applies on models not at run-time
↳
help reduce nb
of tests & help generate sequence of tests to be performed
Warning -
model is abstraction >
- make
simplifying assumptions
Formal methods in critical systems
1
. Safety-critical - failure may endanger human life
.
2 Security-critical - failure means non-authorized access to sensitive info
. Business-critical
3 (quality critical) - cost failure is
high
Safety standards & crification - incentive for formal methods
standards fortransportations systems & medical devices -> formal methods.
Best practices of VOV
·
raif start as
early as possible
venf invisible to users ,
automated and integrated in Model-Driven Development flows
coss-validation between techniques/tools
models and assumptions should be questioned and checked against measurements
Formal method : theorem
puring (deductive veif (
System ->
set
of axioms
("things we assume are true")
properties on the specification >
-
theorems to prove
+ powerful and allow parametric reif
.
X complex
