Як темпоральна логіка Аміра Пнueli назавжди змінила верифікацію програмного забезпечення
Амір Пнueli змінив наше уявлення про програмне забезпечення. Він не просто писав код. Він заклав правила, які б гарантували, що код не дасть збій. Який народився 22 квітня 1941 року в Нахалі (Палестина, нині Ізраїль), він став першим ученим, який впровадив темпоральну логіку в комп’ютерні науки. За цю роботу він отримав прем’єру Т’юрінга 1996 року імені А. М. Тьюринга. Це залишається найвищою нагородою у цій галузі. У цитаті до премії відзначалися його основні роботи із запровадження темпоральної логіки та видатний внесок у верифікацію програм та систем.
Пнюлі почав свій шлях з математики. Він отримав ступінь бакалавра в Ізраїльському технологічному інституті (Техніон). Пізніше, в 1967 році, він отримав докторський ступінь математики в Інституті науки Вейцмана. Зміну спрямування він здійснив у Стенфордському університеті, де працював постдоком. Також він провів час у дослідному центрі IBM Вотсона. Цей досвід змістив його фокус у бік комп’ютерних наук.
Він повернувся до Ізраїлю як старший дослідник і приєднався до кафедри прикладної математики Інституту Вейцмана. У 1973 році він перейшов до Тель-Авівського університету, де заснував факультет комп’ютерних наук. 1981 року він повернувся до Інституту Вейцмана.
Чому Пнueli важливий для сучасного програмного забезпечення
Більшість людей не знає його імені. Але вони щодня використовують його ідеї. Амір Пнueli вирішив складну проблему. Як довести працездатність системи, коли події відбуваються одночасно? Традиційна логіка розглядає стани. Вона задається питанням, істинно чи хибно якась умова. Вона не враховує часу.
Пнueli додав час у рівняння. Він створив “темпоральну логіку”. Це дозволяє розробникам специфікувати поведінку системи у часі. Вона перевіряє безпеку (safety) та живучість (liveness). Без цього було б практично неможливо верифікувати складні системи, такі як керування повітряним рухом або медичні пристрої.
Бізнес-сторона теорії
Пнueli був не просто академіком. Він творив реальні продукти. У 1971 році він заснував компанію Mini-Systems. То була програмна компанія. У 1984 році компанія була придбана корпорацією Scitex.
Він не зупинився на досягнутому. Він співставив компанію AdCad, яка пізніше стала i-Logix. Вони розробляли програмне забезпечення інженерного проектування (CAE). Це було практичне застосування його теоретичних праць. Воно пов’язало абстрактну математику із реальними інструментами інженерії.
Ключові роботи та спадщина
Його найцитованішою роботою є спільна робота із Зохаром Манною. У 1991 році вони написали книгу The Temporal Logic of Reactive and Concurrent Systems: Specification. У 1995 році вони опублікували продовження: “Temporal Verification of Reactive Systems: Safety”.
Ці книги є обов’язковими для читання для всіх, хто вивчає верифікацію програм. Вони пояснюють, як моделювати системи, які реагують на вхідні дані. Вони показують, як перевірити, що ці системи залишаються безпечними за будь-яких умов.
Пнueli помер 2 листопада 2009 року у Нью-Йорку. Його спадщина живе у кожному рядку верифікованого коду. Щоразу, коли система доказово безпечна, працює його логіка. Область верифікації систем перебуває у неоплатному боргу проти нього.
Студенти, які вивчають конкурентні системи, повинні розпочинати з цього.
