Неотъемлемой частью работ при разработке или модификации программных систем является верификация
| Вид материала | Документы |
- И. Н. Кузнецов, Л. В. Лойко, 453.45kb.
- Методические рекомендации «О проведении практических работ по географии», 57.48kb.
- Основы конституционного права китая, 732.42kb.
- Низаций, являясь неотъемлемой частью их хозяйственной жизни, способна при ее правильной, 109.79kb.
- Планирование и проектирование информационных систем Лекция 3 Управление рисками при, 106.01kb.
- Е служб) позволяют использовать при реализации сложных систем концепцию программных, 147.44kb.
- Программа к курсу «Музыка», 82.14kb.
- Для информационно-пропагандистских групп, 160.85kb.
- Лабораторные работы, 281.72kb.
- Программа курса по выбору для учащихся 9-х классов учитель химии, 174.55kb.
Аксиоматическая семантика как метод формальной верификации программных систем
Гайтан Е.Н.
Полтавский национальный технический университет
имени Юрия Кондратюка, Украина, Полтава
Неотъемлемой частью работ при разработке или модификации программных систем является верификация. Верификация представляет собой формальное доказательство соответствия разрабатываемой системы ее спецификации. Для повышения эффективности использования человеческих и машинных ресурсов при разработке системы верификация должна быть тесно интегрирована с процессами проектирования, разработки и сопровождения программной системы.
Процесс верификации программных систем определен базовым стандартом ДСТУ 3918-99 (ISO/IEC 12207:1995) «Информационные технологии. Процессы жизненного цикла программного обеспечения», а также международными стандартами IEEE 1012-2004 и ISO/IEC TR 19759 «Software Engineering Body of Knowledge». В рамках каскадной модели жизненного цикла программной системы верификация должна выполняться в рамках этапов жизненного цикла для проверки корректности их результатов, и именно она в первую очередь обеспечивает успешное движение к конечной цели.
Один из видов верификации – тестирование – в этой модели даже выделен в отдельный этап проекта. Однако существующие на сегодняшний день методы тестирования ПО не позволяют однозначно и полностью выявить все дефекты и установить корректность функционирования анализируемой программы, поэтому все существующие методы тестирования действуют в рамках формального процесса проверки исследуемого или разрабатываемого ПО. Поэтому для эффективной верификации сложных программных продуктов необходимо применение математического инструмента, позволяющего с помощью логического вывода выполнить формальную верификацию системы и доказать правильность работы программы и соответствие ее спецификации.
Рассмотрим аксиоматическую семантику, разработанную английским специалистом в области компьютерных систем Ч. Хоаром, в качестве основы логического вывода правильности программ. Аксиоматический метод Хоара моделирует отношения и причинно-следственные связи, возникающие между операторами языка программирования.
Так, правильность составного оператора S, состоящего из операторов S1 и S2, определяется следующим образом:
{} S1 {1} & {1} S2 {} S {}.
Аксиома, применимая для оператора цикла, выглядит следующим образом:
{ & } S1 {} {} repeat S1 until { &}.
Применение данного метода при аналитико-имитационном моделировании систем в рамках аналитической части позволяет определить целостность программы, правильность передачи данных между операторами и модулями, отсутствие в программе взаимного блокирования процессов и т.д., т.е. выполнить ее верификацию.
Литература
1. ДСТУ 3918-99 (ISO/IEC 12207:1995). Інформаційні технології. Процеси життєвого циклу програмного забезпечення. – К.: Держстандарт України, 2000. – 49 с.
2. Abran A., Moore J.W., Bourque P., Dupuis R., Tripp L. Guide to the Software Engineering Body of Knowledge / IEEE Computer Society, Los Alamos, 2005. – p. 202.
3. Хоар Ч. Взаимодействующие последовательные процессы. М.: Мир, 1989. – 264 с.
4. Кулямин В.В. Методы верификации программного обеспечения // du.ru/ft/005645/62322e1-st09.pdf.