Формальные методы и тестирование программного обеспечения
В последнее время наблюдается бурное развитие компьютерных технологий. Они проникают во все сферы деятельности человека и оказывают все большее влияние на его жизнь. Системы управления транспортом и автоматизированные линии производства, банковские платежные системы и телекоммуникационные сети, медицинские системы обеспечения жизнедеятельности и интеллектуальные дома - все это является неотъемлемой частью современного мира.
Однако, чем большее значение отводится компьютерным системам, тем выше становится цена их ошибок. Как показывает практика, наиболее уязвимым местом компьютерных систем с этой точки зрения является программное обеспечение. Так, ошибка в одном программном модуле многомиллионного межпланетного корабля Mars Climate Orbiter привела к его гибели в атмосфере Марса после более чем девятимесячного полета [, ].
Более того, некорректное поведение современных программных систем влечет не только огромные убытки, но и приводит к гибели людей. Например, ошибки в программном обеспечении медицинского оборудования Therac-25 привели к получению повышенной дозы радиации и последующей смерти 7 пациентов [, ]. А арифметическая ошибка в программном обеспечении комплекса противовоздушной обороны Patriot не позволила вовремя обнаружить иракскую ракету, что привело к гибели 28 солдат во время ирако-американской войны 1991 года []. И это только малая часть уже имевших место прецедентов.
С нарастанием сложности и важности задач, решаемых программными системами, проблема обеспечения их качества становится все острее. Много надежд на существенный прогресс в этом направлении связывается с развитием формальных методов.
Рисунок 1.Схема работы методов аналитической верификации и проверки моделей
В широком смысле, под формальными методами понимаются любые попытки использования математических подходов к разработке программного обеспечения с целью повышения его качества[]. Как правило, для этого используются математические модели различных сущностей, участвующих в процессе разработки.
В последнее время наблюдается бурное развитие компьютерных технологий. Они проникают во все сферы деятельности человека и оказывают все большее влияние на его жизнь. Системы управления транспортом и автоматизированные линии производства, банковские платежные системы и телекоммуникационные сети, медицинские системы обеспечения жизнедеятельности и интеллектуальные дома - все это является неотъемлемой частью современного мира.
Однако, чем большее значение отводится компьютерным системам, тем выше становится цена их ошибок. Как показывает практика, наиболее уязвимым местом компьютерных систем с этой точки зрения является программное обеспечение. Так, ошибка в одном программном модуле многомиллионного межпланетного корабля Mars Climate Orbiter привела к его гибели в атмосфере Марса после более чем девятимесячного полета [, ].
Более того, некорректное поведение современных программных систем влечет не только огромные убытки, но и приводит к гибели людей. Например, ошибки в программном обеспечении медицинского оборудования Therac-25 привели к получению повышенной дозы радиации и последующей смерти 7 пациентов [, ]. А арифметическая ошибка в программном обеспечении комплекса противовоздушной обороны Patriot не позволила вовремя обнаружить иракскую ракету, что привело к гибели 28 солдат во время ирако-американской войны 1991 года []. И это только малая часть уже имевших место прецедентов.
С нарастанием сложности и важности задач, решаемых программными системами, проблема обеспечения их качества становится все острее. Много надежд на существенный прогресс в этом направлении связывается с развитием формальных методов.
Рисунок 1.Схема работы методов аналитической верификации и проверки моделей
В широком смысле, под формальными методами понимаются любые попытки использования математических подходов к разработке программного обеспечения с целью повышения его качества[]. Как правило, для этого используются математические модели различных сущностей, участвующих в процессе разработки.
Примерами таких моделей могут служить модель исходных требований к разрабатываемой системе, модель архитектуры системы или модель реализации системы.
Одним из основных направлений в области формальных методов являются методы доказательства корректности программ, такие как методы аналитической верификации и проверки моделей [, , , ]. В этих методах доказательство корректности программ строится по следующей схеме. Для данной программной системы создаются математическая модель требований к системе и математическая модель реализации этой системы. После чего доказывается наличие отношения "удовлетворяет" между этими двумя моделями, что и рассматривается как доказательство корректности программы (рисунок 1). Существует также целый набор вариаций подхода. Например, в качестве модели требований может выступать модель программной системы более высокого уровня абстракции, или доказательство корректности может сводиться к доказательству непротиворечивости одной из математических моделей.
Однако, несмотря на большие усилия, вложенные в развитие данного направления, на настоящий момент так и не появилось методов доказательства корректности программ, которые смогли бы предоставить приемлемые решения для обеспечения качества реальных программных систем. В результате, одним из основных средств обеспечения качества программных систем было и остается тестирование: при разработке программ с повышенными требованиями к надежности доля затрат на тестирование в бюджете проекта может достигать 80%.
Многочисленные исследования в области формальных методов нашли свое отражение и в развитии новых технологий тестирования. Одно из наиболее активно развивающихся направлений - тестирование на основе моделей, уже успело показать свои преимущества в целом ряде крупных индустриальных проектов [, , , , , , ].
Тестирование на основе моделей позволяет систематизировать и автоматизировать процесс разработки тестовых наборов посредством использования различного рода математических моделей.И в тех случаях, когда небольшого ручного тестирования оказывается недостаточно для обеспечения требуемого уровня качества программного обеспечения, тестирование на основе моделей позволяет добиться существенного повышения качества тестирования с затратами меньшими, чем при использовании других подходов.
Рисунок 2. Схема работы технологии UniTesK относительно формальных методов
Примерами таких моделей могут служить модель исходных требований к разрабатываемой системе, модель архитектуры системы или модель реализации системы.
Одним из основных направлений в области формальных методов являются методы доказательства корректности программ, такие как методы аналитической верификации и проверки моделей [, , , ]. В этих методах доказательство корректности программ строится по следующей схеме. Для данной программной системы создаются математическая модель требований к системе и математическая модель реализации этой системы. После чего доказывается наличие отношения "удовлетворяет" между этими двумя моделями, что и рассматривается как доказательство корректности программы (рисунок 1). Существует также целый набор вариаций подхода. Например, в качестве модели требований может выступать модель программной системы более высокого уровня абстракции, или доказательство корректности может сводиться к доказательству непротиворечивости одной из математических моделей.
Однако, несмотря на большие усилия, вложенные в развитие данного направления, на настоящий момент так и не появилось методов доказательства корректности программ, которые смогли бы предоставить приемлемые решения для обеспечения качества реальных программных систем. В результате, одним из основных средств обеспечения качества программных систем было и остается тестирование: при разработке программ с повышенными требованиями к надежности доля затрат на тестирование в бюджете проекта может достигать 80%.
Многочисленные исследования в области формальных методов нашли свое отражение и в развитии новых технологий тестирования. Одно из наиболее активно развивающихся направлений - тестирование на основе моделей, уже успело показать свои преимущества в целом ряде крупных индустриальных проектов [, , , , , , ].
Тестирование на основе моделей позволяет систематизировать и автоматизировать процесс разработки тестовых наборов посредством использования различного рода математических моделей.И в тех случаях, когда небольшого ручного тестирования оказывается недостаточно для обеспечения требуемого уровня качества программного обеспечения, тестирование на основе моделей позволяет добиться существенного повышения качества тестирования с затратами меньшими, чем при использовании других подходов.
Рисунок 2. Схема работы технологии UniTesK относительно формальных методов
