Технологія MODEL CHECKING

Розробка паралельних та розподілених багатопоточних програм вимагає особливої ретельності та синхрогвзації роботи окремих частин програми. Це обумовлено великою кількістю помилок, які виникають при розробці таких програм. Особливо це актуально для бортових систем управління літаком або космічним кораблем. Паралельні та розподілені системи можуть працювати коректно довгий час і роками зберігати 'тонкі' помилки, які можуть проявитись у виключних ситуаціях. Такі помилки призводили до крупних аварій і катастроф. Нагадаємо найбільш гучні з них. Так 4 червня 1966 р. на 39 секунді при першому запуску вибухнула ракета «Аріан 5» – аналог російської ракети «Протон». Бортова система ракети «Аріан 5» використовувала ПЗ попередньої версії «Аріан 4», але архітектура апаратної частини була змінена. Після проведеного ретельного розслідування було виявлено помилку в навігаційній програмі бортового комп'ютера. Втрати були величезними. Це ракета, вартість якої перевищувала 7 млрд доларів, встановлене на борту наукове обладнання вартістю більш ніж півмільярда доларів, До цього треба додати втрати від недоотриманої вигоди, а також втрати репутації ракети-носія. Непрямі втрати склали біля 2 млрд. доларів.

25 грудня 2004 р. після семирічного польоту космічний зонд «Гюйгенс» відділився від автоматичної міжнародної станції «Кассіні» і почав спуск на поверхю Титану - супутника Сатурну. 15 січня 2005 р. зонд вперше в історії почав передавати інформацію з поверхні Титану. Помилка в бортовій системі призвела до того, що половина переданої інформації була втрачена. Загальні затрати на розробку складали 2,5 млрд. доларів.

20 грудня 1995 р. зазнав катастрофи літак «Боінг» 757, загинуло 159 людей. Розслідування виявило помилку в одному символі в програмній системі управління польотом. Компанії-виготовники бортового комп'ютера та ПЗ були визнані винними в загибелі людей, родичам жертв було виплачено 300 млн. доларів.

23 березня 2003 р. система «Patriot» помилково ідентифікувала британський бомбардувальник «Tornado» як наближаючу ворожу ракету, та автоматично виконала залп. Загинули 2 пілоти. 2 квітня 2003 р. системою «Patriot» був знищений американський винищувач F-16, пілот загинув. В обох випадках причиною були помилки в бортовій системі автоматичного виявлення цілі та наведення.

Наведені приклади показують, що помилки в складних програмних та апартних системах регулярно виявляються при розробці складних систем.

В наш час, коли все частіше людське життя залежить від роботи автоматичних систем, проблема гарантії коректності програмних та апаратних частин цих систем набуває першочергового значення. Надійність та передбачуваність у поведінці таких систем є більш важливим чинником, ніж усе інше.

Правильність таких програм неможливо довести простим тестуванням, майже на всіх наборах початкових даних вони можуть працювати правильно. Тільки строгий формальний аналіз та верифікація програми можуть виявити помилку.

Формальна верифікація програми являє собою сукупність прийомів та методів формального доведення того, що модель програмної системи задовільняє заданій формальній специфікації. Оскільки будь-що формально довести можна тільки відносно формальної моделі, то аналізуєма система для верифікації та наступної реалізації повинна бути представлена формальною моделлю. Вимоги до кінцевого продукту частіше за все розмиті. Для здійснення верифікації специфікація програми повинна складатись з набору формальних тверджень щодо бажаних властивосткй поведінки системи. Для формальної специфікації застосовується мови логики, кожне твердження якої може бути істиним або хибним для програмної системи, яка перевіряється. Верифікація передбачає перевірку виконання заданих формальних тверджень на данній формальній моделі. В області верифікації програм впродовж десятиліть робились серйозні зусилля по розробці теорії, алгоритмів та техніки верифікації. На даний час ці методи розробляються у трьох основних напрямках:

- дедуктивна верифікація;

- перевірка еквівалентності;

- переваірка моделі (model checking).

Дедуктивна верифікація – це перевірка правильності програми, яка зводиться до доведення теорем у підходящій логічній системі. Цей напрямок розробляється вже більше 40 років, з тих часів, коли Роберт Флойд та Ентоні Хоар вперше поставили проблему доведення правильності програм. Верифікація програм при цьому виконується дедукцією на основі аксиом та правил виводу. Це досить складна процедура не може бути повністю аітоматизована, вона вимагає участі людини, яка діє на основі здогадок та передбачень, та використовує інтуіцію при побудові інваріантів та нетривіальному виборі альтернатив.

Перевірка еквівалентності пов'язана з розробкою формальних моделей взаємодіючих процесів, поданням в рамках таких моделей, як специфікації, так і реалізації та перевіркою еквівалентності поведінок формально визначених моделей поведінки. Цей напрямок був розпочатий працями Робіна Міллера розробкою ним алгебри процесів Обчислення взаємодіючих систем (Calculus of Communicating systems – CCS) біля 30 років тому.

Метод model checking [16] пов'язаний з формальною перевіркою виконання на моделі реалізації властивостей поведінки, які специфіковані на мові формальної логики. Цей метод розроблявся біля 20 років. Метод model checking може бути повністю автоматизований. Model checking – це метод перевірки того, що на даній формальній моделі системи задана логічна формула виконується (приймає істинне значення). Ця техніка була розроблена для моделей систем переходів і так званих «темпоральних» логик. Для реалізації за цим методом реальна система подається простою моделлю у вигляді кінцевого автомату з системою переходів та кінцевою кількістю станів. При цьому кожен стан описується так званими структурами Крипке, які враховують всі стани моделі, початковий стан, правила переходу в інші стани із застосуванням темпоральної логики.

На даний час ця методика розробки складного ПЗ має промислове впровадження та підвищений рівень довіри і широко застосовується при розробці складних систем. Вчені Е. Кларк, А.Емерсон та Дж. Сифакис були були нагороджені у 2007 р. премією імені А. Т'юринга за їх внесок в доведення метода model checking до виробничої технології, яка дозволяє здійснювати верифікацію моделей реальних програмних та апаратних систем. В багатьох роботах наводяться результати використання цієї технології для верифікації програмно-апаратних систем у критичних застосуваннях.