Бүгінгі таңда жұмыс логикасында қатесімен көптеген веб-қосымшалар бар. Бұл осалдықтардың көпшілігін қосымшаның логикасында көрсетілгеннен басқа автоматтандырылған тестілеу арқылы алдын алуға болады.
Логикалық қателерді анықтау үшін формальды тексеру әдістерін қолдану керек. Осы жұмыста осалдықты тексеріп анықтау үшін соңғы күйлері бар параллель жүйелерді автоматты формальды түрде тексеру әдісі қолданылды. Осы мақсаттарға қол жеткізу үшін Spin утилитасында модель құрылды, верификация жүргізілді және нәтижелер алынды. Осылайша, вебқосымшаның алгоритміндегі осалдықтардың бірін көрсетуге әрекет жасалды.
түйін сөздер: верификация, алгоритмді тексеру, веб қосымшасы, қосымшаның қауіпсіздігі, логикалық қателер, параллель процестер, Spin утилитасы, Model Checking.
