Нужно ли учить методам формальной верификации?1

Вид материала

Документы

Содержание Надо знать! Верифицирующий компилятор

Подобный материал:

• Конспект лекций по "Аналитической верификации программ", 241.09kb.
• «Интеграция искусств в преподавании предметов гуманитарного цикла», 77.3kb.
• Современные педагогические технологии, 82.34kb.
• Удк ?????? О верификации динамических свойств систем взаимодействующих агентов, 167.14kb.
• Концепция верификации риска, безопасности и ресурса сложной технической системы, 181.86kb.
• Районный конкурс панорама методических идей. Использование современных приемов и методов, 50.2kb.
• The Government of Kazakhstan is concerned with informal employment. The reasons for, 37.8kb.
• Информационные технологии как средство активизации познавательной деятельности и творческого, 71.12kb.
• Подраздел «Какой английский учить?» Какой английский учить? Варианты и диалекты, 2144.83kb.
• К. Г. Паустовский «Кот-ворюга», 32.43kb.

Нужно ли учить методам формальной верификации?¹

Шилов Н.В., Шилова С.О., Бодин Е.В.

Введение

Скупой платит дважды…

Мир очень изменился за последние 30 лет. Век информационных технологий сменил век достижений технологий обычных. Человечество не так далеко шагнуло в космос, не освоило океаны, не изменило принципиально транспорт и энергетику – но! Мобильная связь, компьютеры и вездесущий Интернет. Всё большая часть жизни уходит в виртуальную реальность. Нажми лишь нужные кнопки!

Мы обращаемся с «умной» техникой, как феи со своим волшебным реквизитом, забывая, что этот «ум» – программы, написанные людьми. Языки программирования всё более высокого уровня, машинная графика, программы, пишущие программы… Пирамида растёт. Как происходят вычисления в конкретном компьютере? Ведь в вычислительных машинах нет действительных чисел, даже и рациональных почти нет; есть, к примеру, типы INTEGER и REAL.

И ведь ошибки могут быть не только в вычислениях. Могут ошибаться специалисты, создающие математическую модель процесса или сооружения. Могут быть ошибки в алгоритме решения задачи. Могут быть ошибки в программной реализации алгоритма. Используя выросшие, как на дрожжах, информационные технологии, мы делаем выводы о реальности – а насколько эти выводы верны?

Аварии в энергетике и на транспорте, обрушения зданий и сооружений – похоже, XXI век становится веком техногенных катастроф. И во многом потому, что человечество слишком небрежно относится к тому аппарату, с помощью которого проектирует свою мощную технику и управляет ею. Ещё не забылись обрушения зданий Московского аквапарка и Басманного рынка. Нодар Канчелли, архитектор и проектировщик этих зданий, сослался на ошибку в программе для расчёта прочности [1]. Программными ошибками были вызваны серьёзные аварии на заводах, катастрофы с самолётами, гибель больных при лечении. Ошибки в программном обеспечении систем управления работой электростанций всех типов, трубопроводов, энергосистем, водоочистных сооружений приводили (и не раз ещё приведут) к очень серьёзным последствиям [2, 3, 4].

Что же можно предпринять? Как убедиться в том, что программное обеспечение работает правильно? Как понять, нет ли ошибок в вычислительной программе? На вопросы «как» точных ответов в общем случае нет. А вот с вопросом «что»…

С ошибками в программах борются разными способами. Во-первых, программы отлаживаются и тестируются, что не исключает ошибок совсем, но значительно уменьшает их число. Во-вторых, при написании программ для критически важных систем используются безопасные языки программирования (например, официальным языком программирования в Пентагоне является язык ADA [5]. В третьих, программы формально верифицируются – о том, что это такое, и пойдёт речь дальше в нашей статье. В четвёртых, во всём мире – но не в нашей стране – выделяются довольно большие средства для проведения научных исследований и производства безопасного программного обеспечения². Мы же можем (пока ещё можем) лишь «быть в курсе дела» – т. е. понимать, что сделали наши коллеги, вести теоретические разработки и делать реальные продукты лишь на самых простых, модельных задачах. Создание безопасного программного обеспечения – задача трудоёмкая, нужен длительный труд многих очень квалифицированных специалистов. Но это будет не так дорого стоить, как героический труд бессменного Шойгу и его министерства. Или в планах России нет больше сложных технологических проектов?

Надо знать!

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

Начнём с самого термина «верификация». Он произошедший от лат. verus – «истинный» и означает подтверждение соответствия конечного продукта некоторым эталонным требованиям. Для нас конечный продукт – программа на некотором формальном языке программирования, и нас будет интересовать формальная верификация, т. е. доказательство правильности программы в соответствии с формальным описанием её свойств.

Как видите, много формального. Но формализм здесь не только и не столько математический. Тема и методы наших исследований – в области информатики (и, конкретнее, теоретического программирования).

Информатику уже изучают в школах. Но, если о математике, физике, биологии и т. д. в обществе давно сложилось устойчивое представление, об информатике ещё стоит поговорить. Информатика – наука о способах получения, накоплении, хранении, преобразовании, передаче и использовании информации. Она включает в себя многие дисциплины: абстрактные, вроде анализа алгоритмов, и довольно конкретные, например, разработка языков программирования. Конечно же, очень велико влияние математики на информатику. Яркий пример этого влияния – это теоретическое программирование: изучение математических моделей алгоритмов, структур данных, программ и т. п. с применением математической логики, абстрактной алгебры, топологии и т. д. Идеи, подходы и методы информатики также могут быть плодотворно использованы в математике³. Самая престижная научная премия в области информатики – премия имени Алана М. Тьюринга. Лауреат этой премии 1980 г., британский учёный Антони Хоар перечислил несколько глобальных проблем программирования как науки [6] и среди них – проблему создания верифицирующего компилятора.

Верифицирующий компилятор – компьютерная программа, переводящая (транслирующая) написанные человеком программы с языка высокого уровня в эквивалентные программы, пригодные для непосредственного исполнения на вычислительной машине, и при этом доказывающая специфицируемые человеком математические утверждения о свойствах транслируемых программ. Все, кто писал компьютерные программы, знают, как трудно бывает их отладить – т. е. добиться того, чтобы программа работала, и работала правильно (хотя бы на первый взгляд). Проверка синтаксической правильности (т. е. правильности употребления конструкций языка, «грамматика») и трансляция в исполняемый машинный код осуществляются полностью автоматически специальными программами (мы не будем сейчас вдаваться в тонкости употребления терминов «транслятор», «интерпретатор» и «компилятор»). А вот дальше… Воспользуемся следующим образным сравнением из предисловия переводчиков к книге [9]: «Средства отладки программы, которые входят в состав всякой развитой системы программирования, могут помочь разработчику в той же мере, в какой лопата оказывает помощь кладоискателю. Главные вопросы - где копать и стоит ли копать вообще? Здесь скорее пригодилось бы устройство наподобие металлоискателя. Но хороший металлоискатель - это тонкий инструмент, требующий знания его устройства и умелого обращения. Так что кроме лопаты неплохо бы использовать и автоматические системы поиска ошибок и проверки правильности функционирования программ…» Такой автоматической системой и должен стать верифицирующий компилятор. Человек, написавший программу, указывает, какими свойствами программа должна обладать (как это делается – вопрос отдельный и тоже будет обсуждаться). Верифицирующий компилятор, транслируя программу в исполняемый код, доказывает, что эти свойства выполняются. Результат его работы – не только машинный код, но и проверка выполнения (или невыполнения) конкретных условий, т. е . автоматическая проверка правильности работы программы (или неправильности – с указанием на то, какое именно условие не выполняется.) Создание верифицирующего компилятора – глобальная проблема программирования, находящаяся в стадии решения, требующая систематических многолетних и скоординированных усилий специалистов во всем мире.

Теперь попробуем разобраться с тем, что же это за специфицированные человеком математические утверждения о свойствах транслируемых программ. Программы описывают преобразования данных, но не смысл этих преобразований. Смысл преобразований (т. е. семантику программ) описывают спецификации программ. Поэтому наряду с языками программирования существуют языки спецификаций программ. Существуют разные парадигмы языков программирования (например, императивная, функциональная и логическая), существуют и разные парадигмы спецификации программ (логическая, алгебраическая и т. д.). Познакомимся с логическими спецификациями на примере детерминированных программ, у которых каждый шаг исполнения однозначно определяется текущей конфигурацией (т. е. значениями переменных и исполняемым оператором). Отдельно будем рассматривать программы вычислительные и резидентные (или реактивные):

• Вычислительная программа – это программа, которая за конечное время преобразует начальные (входные) в заключительные (выходные) значения.
  
• Резидентная программа – это программа, которая должна работать бесконечно долго, но может в процессе многократно получать входные значения и многократно выдавать выходные значения (например, операционная система).
  

Здесь мы ограничимся только вычислительными программами.

Для детерминированных вычислительных программ используют два вида логических спецификаций, которые называются:

• условиями частичной корректности,
  
• условиями тотальной корректности.
  

Эти условия обозначаются как и соответственно, где  – программа, предусловие  – это условие на входные данные, которое требуется перед исполнением программы , а постусловие  – это условие на выходные данные, гарантируемое после исполнения программы .

Говорят, что условие частичной корректности  истинно (верно), или программа  частично корректна по отношению к предусловию и постусловию  (обозначение ╞), если на любых входных данных, которые удовлетворяют свойству , программа  или не останавливается (зацикливается, зависает и тому подобное), или останавливается с выходными данными, которые удовлетворяют .

Говорят, что условие тотальной корректности  истинно (верно), или программа  тотально корректна по отношению к предусловию  и постусловию  (обозначение ╞), если на любых входных данных, которые удовлетворяют свойству , программа  всегда останавливается с выходными данными, которые удовлетворяют .

Таким образом, для детерминированных программ разница между частичной и тотальной корректностью состоит в завершаемости программы: частичная корректность допускает неостановку программы, а тотальная – запрещает.

Пример спецификаций корректности: задача на вычисление целой части квадратного корня из натурального числа. Неформально программу, которая решает эту задачу, можно специфицировать так: по целому неотрицательному числу n вычислить [n^1/2]. В качестве решения программист написал следующую программу SR, которая (по мнению этого программиста) решает поставленную задачу (причём без использования операции умножения и без вложенных циклов):

VAR x,y,n : INT;
x := 0 ; y := 0 ;
WHILE y <= n DO (y := y + x + x + 1; x := x + 1);
x:= x - 1

Потом этот программист специфицировал программу условием частичной корректности {n0}SR{x²n & (x+1)²>n}. Истинность этого условия означает, что при любом натуральном начальном значении N переменной n эта программа SR если когда-либо завершит свою работу, то заключительное значение X переменной x будет таким, что X²N & (X+1)²>N, т. е. будет равно [N^1/2]. А истинность условия тотальной корректности [n0]SR[x²n & (x+1)²>n] означает дополнительно, что программа SR обязательно завершит свою работу.

Итак, мы получили представление о том, как специфицировать программу математическими условиями. Как же доказывается выполнение (или невыполнение) этих условий? Уже на этом этапе трудно объяснить существующие методы на популярном уровне, поэтому ограничимся только одним из них – методом потенциалов, принадлежащим Р. Флойду. Этот метод для доказательства завершаемости детерминированных программ кратко можно описать таким образом:

• выбирается конечное множество числовых значений, которые называются потенциалами;
  
• каждому возможному набору значений используемых переменных сопоставляется некоторый потенциал.
  

Тогда условие корректности метода потенциалов состоит в следующем: каждое исполнение тела любого цикла в алгоритме уменьшает значение потенциала. – Заметим, что истинность условия корректности обеспечивает завершаемость работы алгоритма. Пример применения метода потенциалов можно найти в [7].

Заключение

Выше мы обсудили, насколько актуальна и сложна задача создания верифицирующего компилятора. Напомним, однако, что, по мнению одного из классиков программирования А. Хоара, проблема верифицирующего компилятора является одной из центральных и глобальных проблем (Grand Challenge) программирования как науки, решить которую невозможно в одиночку или небольшим коллективом ученых. Решение такой проблемы может быть достигнуто только на пути комбинации (а затем и интеграции) частных продвижений отдельных коллективов.

Мы также обсудили список основных понятий и одни из методов формальной верификации вычислительных детерминированных программ. Но многое осталось за рамками этой короткой статьи. Например – понятие верификации моделей [9] или об эффективной генерации условия корректности по специфицированной программе и автоматическом доказательстве сгенерированных условий корректности.

Дело в том, что алгоритмы генерации условий корректности непосредственно по классическим правилам аксиоматической семантики Флойда – Хоара имеют экспоненциальную сложность. Для генерации условий корректности программ можно использовать оригинальный полный алгоритм генерации условий корректности [8], разработанный в рамках проекта РФФИ № 06-01-00464-а «Развитие методов верификации и спецификации свойств моделей программных систем». Этот алгоритм имеет квадратичную сложность. Минимизация списка условий корректности производится также автоматически. Завершив эту работу, мы получим некоторый список условий в виде булевских формул. Для проверки выполнимости этих формул предполагается использовать автоматические булевские решатели (SAT solvers), возможно, в комбинации с проблемно-ориентированными разрешающими процедурами для теорий проблемных областей (SAT modulo Theories). Но это – уже тема для дальнейших исследований в рамках нового проекта РФФИ № 09-01-00361«Автоматическая верификация программ с использованием булевских решателей». Каждый шаг на этом пути требует серьёзного теоретического обоснования. И очень много ещё предстоит сделать. Но работу в этом направлении вести надо, и очень активно.

Литература

1. Чёрный Г. Рассказы о современной механике. Квант, №3, 2009.
   
2. Живич М., Каннингэм Р. Истинная цена программных ошибок. Открытые системы, №3, 2009. (Доступна на u/os/2009/03/8158133/)
   
3. Аджиев В. Мифы о безопасном ПО: уроки знаменитых катастроф. Открытые системы, №06, 1998. (Доступна на u/os/1998/06/179592)
   
4. cl.ac.uk/Risks
   
5. Бар Р. Язык Ада в проектировании систем. М.: Мир, 1988.
   
6. Hoare C.A.R. The Verifying Compiler: A Grand Challenge for Computing Research. Proceedings of A. P. Ershov Memorial Conference «Perspectives of System informatics», Novosibirsk, Russia, 2003. Lecture Notes in Computer Science. Springer Verlag. 2003. Vol..2890. p.1 – 12.
   
7. Шилов Н.В., Андреева Т.А., Городняя Л.В., Бодин Е.В. Этюд на тему Дейкстры: информатики в роли геометров. Потенциал, №9, 2006. Стр.30 – 37.
   
8. Шилов Н.В., Ануреев И.С., Бодин Е.В. О генерации условий корректности для императивных программ. Программирование, №6, 2008. Стр. 1 – 24.
   
9. Кларк Э. М., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking. М.: Издательство Московского центра непрерывного математического образования, 2002.