Тьюринговская премия, выдаваемая Association for Computing Machinery, самым крупным в мире компьютерным научно-образовательным сообществом, основанным в 1947 году, была учреждена в 1966 году. Премия вручается за вклад в усовершенствование компьютерных технологий. Чтобы ее получить, нужно сделать нечто такое, что имеет значимость для практического развития компьютерных систем. Это объясняет и состав награжденных ею, и то, почему академические работы не могут быть основанием для номинации. (Тем, кто сетует на отсутствие среди награжденных этой премией наших соотечественников, следует учитывать необходимость наличия практического применения у награждаемых работ.)
Невзирая на высокий статус, Тьюринговская премия скорее почетна, чем финансово значима. И если сравнивать ее с призовыми награждениями теннисистов или гонорарами в кино и шоу-бизнесе, то ее денежное выражение ничтожно. Пока единственным спонсором премии была корпорация 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 большое будущее, которое связано с крупными программными системами.