Äîêóìåíò âçÿò èç êýøà ïîèñêîâîé ìàøèíû. Àäðåñ îðèãèíàëüíîãî äîêóìåíòà : http://savenkov.lvk.cs.msu.su/mc/lect01.pdf Äàòà èçìåíåíèÿ: Fri Feb 24 01:31:01 2012 Äàòà èíäåêñèðîâàíèÿ: Sat Apr 9 22:23:16 2016 Êîäèðîâêà:

()



· · · · ·



Unit System







· ­ · ­ · :
­ ,

building the wrong system,
­ ,

building the system wrong.



·
­ , , ­ , .

·

, NB:



· · · · ·



· :
­ , ­ , ­ .



· (Safetycritical) · :
­ ­ ­ ­ , .


: Ariane-5
· 1996 , 40 . , · ­ $500 ( ­ $7 .), · ­ 64bit float -> 16bit int.


: Patriot
· 1991 , Patriot Scud, · ­ 28 , >100 , · ­ - 24bit fixed, Scud 500.


: Sleipner A
· 1991 , , Sleipner A , · ­ $700 , 3 , · ­ .


- (2010)
· : Toyota Prius ( ABS), Chrysler ( , ) · UK ( 25 ) · ( 64- ) · McAfee ( Windows , ) · Skype ( , P2P ) · NYSE Euronext (S&P 10%) · 88 Android Froyo ( )



· , ! · ,
­ ( ) ­ ( , -) ­ (augmented reality)

· - , .



· · · · ·



« , » () .









Reminder

., , , , etc



« , , »

· · :
­ ­ ­ -



· · · · · · «»



· , · « » () - , · « » () - .


:
· , , · () , · .


:
· , · .

­


:
· :
­ : , ­ : ­ , ­ : , ­ . ­ : , ­ : 100% , ­ : .



· :
­ 1014 , ­ 18 , ­ 50 200 .



if (B1) { S1; } if (B1) { S1; } if (B2) { S2; }

-

-

...exp...



int x = 1; if (x == 1) { std::cout << "Okay" << std::endl; } else { std::cout << "Error" << std::endl; }

--


­
int strlen(const char* p) { int len = 0; do { ++len; } while (*p++); return len; }

«», «bbb» -- ,


:
· ­ , , · ­ , , · ­ , · ­ .


-
· , - ; , RTCA/DO-178B (); · , ­ ; · ­ MC/DC ( http://techreports.larc.nasa.gov/ltrs/PDF/2001/tm/ NASA-2001-tm210876.pdf); · RTCA/DO-178C (2011) model-driven development


:


· :
­ , ­ «/», ­ ;

· :
­ ­ ­ ­ ­ , , «/», ( ), .


:


· · · · , , ­ . :

· , ,



: · , · , · , · ...


:


· ­ , · , · .



· · · · · · «»



· ­ · · ·



· :

A= c·a·B B = b· A

a ·c? · : · :

S1 = a1 · S2 S2 = a2 · S3 s1 · s2 s2 · s3 , S1 = a1 · a2 · S3 s1 · s3



· :
­ - , ­ .

· :
­ , ­ ( ), ­ ( ).



· :
­ Isabelle/HOL, Coq, PVS, Vampire, SPASS, ACL2, Simplify, Microsoft Z

· :
­ ATP « » .. ­ Xavier Leroy, Mechanized semantics with applications to program proof and compiler verification, INRIA, France, 2009 (http://pauillac.inria.fr/~xleroy/courses/ Marktoberdorf-2009/notes.pdf) ­ PVS 5-



· · · · · · «»



· , · , ·
( ),

· .



· : , · : ,






· : , · : «» , · !





:
:
int min(int* arr, int n) { int m; if (n > 0) { m = arr[0]; } int i = 0; while (i < n) { if (m > arr[i]) { m = arr[i]; } i++; } return m; }

dom(m) = Int + { } NI = { } I = Int v: Expr -> {NI, I}


:
:
int min(int* arr, int n) { int m; if (n > 0) { m = arr[0]; } (!) int i = 0; while (i < n) { if (m > arr[i]) { m = arr[i]; } i++; } return m; }

dom(m) = Int + { } NI = { } I = Int v: Expr -> {NI, I}



·
­ , ­ , .

·
­ ( , , .), ­



· :
­ ASTREE (http://www.astree.ens.fr ),

· :
­ Reps, T., Program analysis via graph reachability. Information and Software Technology 40, 11-12 (November/December 1998), pp. 701-726. ­ P. Cousot & R. Cousot A gentle introduction to formal verification of computer systems by abstract interpretation, Logics and Languages for Reliability and Security, 2010, NATO Science Series III: Computer and Systems Sciences, IOS Press, 29 pages.



· · · · · · «»


(model checking)
· , · ­ . · .


:
int count_lines(const char* filename) { int c, count = 0; FILE* f = fopen(filename, "r"); if (f != NULL) { c = fgetc(f); while (c != EOF) { if (c == '\n') { ++count; } c = fgetc(f); } if (ferror(f)) { return -1; } fclose(f); return count; } else { return -1; } }

?


:
· count_lines:
f = NULL fopen fclose return

entry

opened

closed

exit

ferror(f ) = 1



·
­ , ­ «» ;

·
­ , ­ ;

·
­ , ­ .



·
­ , ­ , , , ­ .

·
­ .



· :
­
:

­
:

­
:



· .. · : ,
­ , ­ , ­



· , · :
­ ­ ­


1:
· , 1967 ­ assertions, , · , 1969 ­ - -, (P | S | Q), , · , , 1971 ­ , · , 1975 ­ Guarded Command Languages, · , 1978 ­ (CSP), · , 1980 ­ Calculus of Communicating Systems (CCS)
1Vahe

Poladian, Software Technology Maturation Study: Model Checking Techniques and Tools, 2001.


:
· , 1977 ­ LTL, · , 1981 ­ (CTL), · , , 1981 , , 1982 ­ model checking ( ), · , 1986 ­ model checking ( ), · , 1989 ­ SPIN.

?
1981

!

?
1986

!


: « »
· , 1989 ­ (BDD), · , 1993 ­ SMV ( , BDD), · , , 1994 ­ , · 1995 ­ SPIN.


:
· , 1992 ­ , · , 1994 ­ , · , 1996, , 1998 ­ « », · , 2000 ­ , · , , 1994 ­



· · · · ·



· :
­ , Promela, , Spin,

· :
­ (, , ) ­ () ,



: http://savenkov.lvk.cs.msu.su/ mc.html SPIN:
· · Holzmann. The Spin Model Checker: Primer and Reference Manual, Addison Wesley, 2003. Spin: http://www.spinroot.com.

:
· · · · , , . : Model checking, , 2002. Peled. Software Reliability Methods, Springer, 2001. .. Model Checking. http://intsys.msu.ru/staff/mironov/modelchk.pdf .. http://intsys.msu.ru/staff/mironov/ processes.pdf



· · · · · · ­ 20.02; . 758, Linux, SPIN; 5 , ; ­ ; E-mail: model-checking@lvk.cs.msu.su, : model-checking@lvk.cs.msu.su, · ­ .



· , · 20 · :
­ (0..3 ), ­ (0..3 ), ­ «» (-1..1 ).

· .



· 5 : 50+100+50+80+100 = 380
­ [0,230) ­ 0 ( , ), ­ [230,300) ­ 1 , ­ [300,380) ­ 2 , ­ 380 ­ 3 ( «»);

· , ; · , ; · :
­ , ­ ( ), ­ 0.6.


!