Награда, присуждаемая ACM и традиционно называемая Это объясняет и состав награжденных ею, и то, почему академические работы не могут быть основанием для номинации. (Тем, кто сетует на отсутствие среди награжденных этой премией наших соотечественников, следует учитывать необходимость наличия практического применения у награждаемых работ.)

Невзирая на высокий статус, Тьюринговская премия скорее почетна, чем финансово значима. И если сравнивать ее с призовыми награждениями теннисистов или гонорарами в кино и шоу-бизнесе, то ее денежное выражение ничтожно. Пока единственным спонсором премии была корпорация Intel, размер премии составлял всего 100 тыс. долл. С подключением Google он вырос до 250 тыс. Традиционно премию называют "Нобелевской премией в компьютерных науках", хотя это явное преувеличение: и уровень почета, и масштаб вознаграждения явно не в пользу Тьюринговской премии.

Лауреатами 2008 года стали Эдмунд Кларк (Университет Карнеги-Меллона), Аллен Эммерсон (Техасский университет в Остине) и Джозеф Сифаркис (Гренобльский университет, Франция). Они награждены за достижения в области, называемой в оригинале model checking, а по-русски - "верификацией моделей". Перевод оставляет впечатление, что проверка моделей является целью, однако это всего лишь средство. Если быть точным, то model checking - скорее не верификация самой модели, а метод проверки какой-либо системы с использованием модели. Верификация с использованием модели - один из четырех теоретически возможных способов проверки проекта аппаратных или программных систем; помимо него выделяют еще имитационное моделирование, тестирование и дедуктивную верификацию.

Как самостоятельное направление model checking сложилось после ряда известных катастроф крупных объектов космической индустрии, именно они стимулировали работы по тестированию и проверке. Обнаружилось, что трагические события были следствием сложности, так как подобные системы состоят из большого числа компонентов, взаимодействующих между собой и с системными данными. Количество системных компонентов так велико, что могут возникать неоднозначные ситуации или коллизии, подлежащие обнаружению. Основные исследования в этом направлении были сделаны на протяжении последнего десятилетия.

Model checking осуществляется в три этапа – создание модели, создание спецификации системы, верификация модели по спецификации. В данном случае под моделью понимаются не те модели, которые были так или иначе использованы в процессе проектирования. Наоборот - реальная аппаратная или программная система, конвертированная в формальную модель, предназначенную для интерпретации как автомат с конечным числом состояний.

Методы model checking позволяют алгоритмически верифицировать формальные системы. Они в большей степени подходят к аппаратным системам, чем к программным, поскольку последние не всегда удается описать формально. Поэтому область применения model checking пока ограничена моделированием аппаратуры и в лучшем случае аппаратно-программных встроенных систем. Базисом для model checking служит математический аппарат темпоральной логики (temporal logic), то есть такой логики, в которой присутствует фактор времени. Эта разновидность логики была предложена в 60-е годы, обычно ее появление связывают с именами Амира Пнуели и Зохара Манна. Лауреаты премии Тьюринга смогли приложить аппарат темпоральной логики к решению практических задач, создав методы формальной верификации систем. Признанным родоначальником model checking является профессор Университета Карнеги-Меллона Эдмунд Кларк. Его книга, ставшая классической (Э.М. Кларк, О. Грамберг, Д. Пелед "Верификация моделей программ: Model Checking"), переведена на русский язык. Еще две школы model checking сложились в университетах Остина и Гренобля, ими руководили соответственно профессора Аллен Эммерсон и Джозеф Сифаркис.

По оценкам специалистов, у model checking большое будущее, которое связано с крупными программными системами.

Поделитесь материалом с коллегами и друзьями