Äîêóìåíò âçÿò èç êýøà ïîèñêîâîé ìàøèíû. Àäðåñ îðèãèíàëüíîãî äîêóìåíòà : 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.


!