Тестирование на основе формальных спецификаций в процессах разработки программных комплексов

Тестированием программного обеспечения (ПО) занимаются так же давно, как и собственно разработкой ПО. За последние 20−30 лет многое изменилось в программировании в целом и в этой его части — в тестировании. В частности, тестирование признано важной составляющей процесса разработки, часто эта часть требует времени и ресурсов больше, чем собственно программирование [Майерс, Beizer, Binder, Липаев]. Кроме того, признано, что в основе эффективных методов тестирования должны лежать хорошо обоснованные методики, а еще лучше — математические теории, так как в этом случае результаты будут предсказуемы, тем самым процессы разработки будут в большей степени управляемы, а само ПО будет более качественным, в частности, более надежным. Нет никаких сомнений, что работы по теории тестирования крайне важны. Об этом свидетельствуют, например, темы крупнейших научных конференций по различным отраслям информатики. Сомнение может быть в другом — не слишком ли рано мы пытаемся внедрить формальные методы в реальные программистские проекты, причем не в относительно простые фазы, типа прототипирования и эскизного проектирования, а в самые дорогостоящие фазы, такие как в тестирование, где приходится иметь дело не с моделями, сложностью которых исследователь может управлять, а с реальными комплексами, которые приходится тестировать «как есть» — то есть, не меняя размеров, структуры и сложности целевого ПО. Попыткой снять эти сомнения является данная диссертационная работа. Методы, которые рассматриваются в ней, показали возможность использования формальных спецификаций в тестировании реального ПО, включая операционные системы реального времени, компиляторы и реализации телекоммуникационных протоколов. В пользу растущей актуальности этой тематики говорит заметное увеличение числа публикаций по использованию формальных методов для задач тестирования в последние 5−7 лет.

Основные цели работы.

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

• разработать методы построения формальных спецификаций и моделей, являющихся исходными данными для генерации тестов;

• разработать методы построения тестов по спецификациям и моделям;

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

• провести апробацию разработанных методов и инструментов, позволяющую подтвердить их эффективность.

Научная новизна.

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

Традиционная схема разработки программных комплексов, которые должны отвечать высоким требованиям качества, в первую очередь, надежности, выглядит следующим образом [Майерс, Beizer, Binder, Липаев]: разрабатываются функциональные требования, затем создается проект, на основе проекта выполняется реализация (программирование и отладка). На этапе проектирования создаются формализованные спецификации. Они используются как часть постановки задачи для разработчиков-программистов и для разработчиков системных тестов. Разработка тестов для отдельных модулей выполняется после того, как модули уже созданы. После тестирования отдельных модулей создаются тесты для подсистем — это так называемое интеграционное тестирование. В самом конце очередного витка жизненного цикла дорабатываются системные тесты, и проводится системное тестирование, а потом — приемосдаточные испытания. Недостатки этой схемы следующие: разработка тестов модулей начинается поздно, поэтому общие сроки разработки удлиняютсяпроектные решения могут оказаться несогласованными с функциональными требованиями, и нет автоматизированной процедуры, позволяющей проверить эту согласованность между ними.

Для обеспечения предложенного подхода были разработаны новые нотации для описания спецификаций, тестовых сценариев, моделей тестового покрытия. Была разработана унифицированная архитектура верификационного набора, включающего в себя компоненты спецификаций и компоненты тестовой профаммы. Были разработаны методики для построения спецификаций и тестов для программных компонентов (модулей и/или подсистем), предоставляющих программный интерфейс (Application Program Interface — API), и для процессоров сложных структур данных, таких как блоки компиляторов, трансляторы и конверторы протокольных сообщенийметоды генерации тестов для реализаций телекоммуникационных протоколов.

При решении технических проблем разработки инструментов генерации тестов были решены теоретические и методические проблемы автоматической генерации метрик тестового покрытия, автоматической генерации тестовых оракулов (программ автоматического анализа поведения тестируемой программы), автоматической генерации тестовых последовательностей — наиболее сложной проблемы тестирования объектно-ориентированного ПО, проблемы тестирования ПО на соответствие с моделями разного уровня детализации.

Методы исследования.

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

Практическая значимость работы.

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

Ранее формальные спецификации рассматривались как одно из средств поддержки проектирования и, в пределе, как основа для технологии программирования будущего. Полагалось, что в таких технологиях программы будут писаться не вручную, а будут генерироваться автоматически из описания их свойств и/или ограничений целевой системы. Роль таких описаний и должны были играть спецификации. Формальные спецификации не рассматривались в контексте тестирования, поскольку при генерации качество программы должно было бы обеспечиваться автоматически, по построению.

Однако эта идеальная схема оказалась неработоспособной. Причина здесь следующая. Возможность ошибок в спецификациях допускалась всегда. Для того, чтобы их обнаружить и получить в конечном итоге «правильные» спецификации, разрабатывались методы верификации. Некоторые подходы к верификации спецификаций ограничивались доказательством корректности спецификаций, принадлежащих одному уровню детализации. Например, в Венском методе разработки программ (VDM) [VDM] предлагалось использовать несколько трансформированный метод математической индукции. Сначала специфицировались инварианты типов данных, преди пост-условия функций (операций) и устанавливалось, что в начальном состоянии инварианты не нарушены. Затем требовалось доказать, что, если перед вызовом каждой из функций инварианты типов данных не нарушены, то и в результате выполнения функций инварианты не нарушаются.

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

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

Предложенный подход может быть распространен на другие фазы жизненного цикла и процессы разработки ПО. С общих позиций подход может быть определен как использование моделей разного уровня детализации (разной архитектуры и разных парадигм) в разработке, исследовании и развитии ПО. Идея применения моделирования в процессах разработки ПО не оригинальна. Эта идея явно высказывалась уже 80-е годы и, вероятно, раньше. Очередной импульс развитию идеи моделирования придали работы по объектно-ориентированному анализу программ и созданию универсального языка описания моделей UML. Специфической особенностью методов моделирования (спецификации), которые развиваются под руководством автора1, является уровень формальности и детальности используемых моделей, а именно, описание семантики интерфейсов в форме неявных спецификаций (в некоторых случаях алгебраических и явных спецификаций), позволяющее задать не только основную функциональность, но и всю функциональность, включая поведение в нештатных ситуациях, с учетом коллизий, обусловленных параллелизмом, распределенностью системы и асинхронностью взаимодействия компонентов системы. На практике, в реальных проектах были апробированы формальные методы для решения задач:

• анализа (неформальных) требований, их систематизации и частичной формализации;

1 В первую очередь, это касается методологии UniTesK, о которой далее будет рассказано более подробно.

• отслеживания требований и управления требованиями;

• обратной инженерии (reverse engineering), а именно систематизации и формализации результатов обратной инженерии, подготовки этих результатов для передачи знаний (knowledge transfer), создания документации и тестов;

• создания пользовательской документации и поддержки ее в актуальном состоянии;

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

Использование моделей для разработки, верификации и валидации применимо не только к программным системам, но и к аппаратным. Анализ состояния в области разработки аппаратных средств показывает все большую потребность производителей интегральных схем, ASIC (Application Specific Integrated Circuits) и SoC (System-on-a-Chip) в использовании моделей как для поддержки проектирования, так и для тестирования.

Апробация.

Результаты работы были доложены на семинарах и конференциях. Важнейшие из них представлены ниже:

— Конференция по системам реального времени, RTD'94, Дубна,.

1994.

— Конференция «Индустрия программирования», Москва, 1996.

— Форум конструкторов Nortel Networks, Оттава, 1996.

— Конгресс по формальным методам, Тулуза, 1999.

— Конференция «Testing Computer Software», TCS’OO, Вашингтон.

2000.

— IV и V конференции памяти А. П. Ершова, Перспективы информационных систем, PSI'01/03, Новосибирск 2001 и 2003.

— Конференция по формальным методам FME'02 и семинар по VDM++, Копенгаген 2002.

— Академический форум компании Интел, Будапешт, 2002.

— Семинары ИПМ РАН (1996), НИИСИ РАН (1999), TCS, Sasken (Индия) 2001, Microsoft Research (Кембридж, Англия) 2000;2002, Luxoft (Москва) 2002, ВМиК МГУ (2003), ИСП РАН 2003.

Публикации.

По теме диссертации опубликовано более 20 работ, полностью отражающих основные научные результаты диссертации.

Предыстория данного исследования и общая постановка задачи.

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

Термины Computer Science и Software Engineering возникли сравнительно недавно, много позже появления вычислительных машин и программирования как области исследований и отрасли промышленности. Вместе с тем, собственно исследования в этих направлениях появились на самых ранних этапах программирования. Пожалуй, Computer Science оформилась в самостоятельную дисциплину раньше. Формальные модели и математический аппарат здесь использовались уже в 50-е годы. Предметом исследований были такие свойства программ (скорее алгоритмов), как сложность, скорость вычислений, минимизация ресурсов памяти и т. п. Алгоритмы и структуры данных — это объекты, которые легко поддаются формализации, что существенно облегчало становление Computer Science как науки.

Период зарождения и становления Software Engineering продолжался дольше и шел не так гладко. Это объясняется тем, что объектом исследования здесь являются сущности, поддающиеся формализации с трудом. Это те же программы, но уже реального, иногда громадного размерадокументация, обычно неформальная, неполная и противоречиваяпроцессы, в которые вовлекаются не только машины и программы, но и люди.

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

Если в 60-е годы основной интерес специалистов был связан с отдельными средствами разработки программ: языки программирования, компиляторы, операционные системы, системы управления базами данных (СУБД) и проч., то в 70-е годы, вместе со становлением Software Engineering, серьезное внимание начинают уделять комплексному подходу к изучению проблем жизненного цикла в целом, начинают разрабатываться технологии и методологии программирования.

С позиций нашего исследования интересно классифицировать технологии и методологии по степени формализации подходов. Можно выделить три группы:

— неформальные.

— формализованные.

— формальные технологии/методологии.

К первой группе принадлежат технологии разработки ПО, которые подробно расписывали шаги создания ПО, виды работ, виды документов и других проектных и программных материалов, методики планирования, оценки трудоемкости, качества и т. д. В рамках таких технологий разрабатывались и предлагались к использованию специальные формы документов, что частично уже являлось шагом к формализации. Примерами таких формализмов являются стандартизованные блок-схемы или input-output диаграммы компании IBM.

Ко второй группе (формализованные) технологии можно отнести метод программирования М. Джексона (Jackson Structured ProgrammingJSP) [JSP] и метод разработки программ М. Джексона (Jackson System Development Method — JSD) [JSD].

В JSP формализовался процесс проектирования системы. Основной подход был близок к идее проектирования иерархических схем. Предлагался графический язык для описания таких иерархических схем. Метод был достаточно прост и легко укладывался в традиционные тогда архитектуры разработки (середина 70-х годов). В качестве инструментальной поддержки метода были разработаны графические редакторы и конверторы графических описаний алгоритмов в тексты на языках программирования. Такими языками служили, в первую очередь, Кобол, Фортран и другие распространенные языки того времени.

JSP, в основном, ориентировался на Кобол и класс задач, архитектур программных систем, которые разрабатывались на Коболе. В связи с этим в JSP явным образом не представлены средства разработки систем реального времени, в частности, не было параллельных процессов, средств синхронизации и обмена сообщениями и др. С появлением языка Ада, в котором эти средства появились, М. Джексон разработал на смену JSP новую методологию JSD (Jackson System Development). Эта методология уже ориентировалась на Аду. JSP вошел в JSD как составная часть, предназначенная для проектирования структур данных и алгоритмов. Новые возможности JSD позволяли описывать модульную архитектуру системы, потоки данных и средства синхронизации.

Первые, получившие известность методологии третьей группыформальные методологии, появились в 70-е годы. Наибольшее распространение впоследствии получил язык SDL (Specification Definition Language) [SDL], По «формальным» признакам — это язык формальных спецификаций. Однако, далеко не все рассматривают этот язык и методики его использования как разновидность формальных методов разработки программ. Причина заключается в том, что это скорее язык прототипирования. Модели SDL — это алгоритмы процессов, которые достаточно просто могут быть оттранслированы в обычные языки программирования. Кроме того, SDL создавался как средство проектирования телекоммуникационных систем, поэтому использование его как универсального языка проектирования (спецификации проектов) в практическом плане невозможно.

В это же время появились первые работы Венской лаборатории IBM. Одной из задач лаборатории была разработка техники формального описания языков программирования, пригодной для того, чтобы по формальному описанию языка можно было автоматически строить компиляторы соответствующих языков программирования. Сначала был создан язык спецификаций VDL — Vienna Definition Language. В конце 70-х появился VDM — Vienna Development Method (Венский метод разработки программ). VDM — первая методология разработки программ, которая продемонстрировала реальность использования формальных методов в крупных промышленных разработках. Первым серьезным коммерческим проектом стал проект разработки компилятора с языка Ада, выполненного.

14 группой датских специалистов под руководством Д. Бьернера в начале 80-х.

Изначально VDM и его язык спецификаций Meta-IV рассматривались как средства для описания языков и проектирования компиляторов. Чуть позже язык Meta-IV был несколько расширен, а метод был развит с тем, чтобы можно было описывать функциональность программных интерфейсов (Application Program Interface — API). В конце 80-х язык Венского метода был приближен к нотации обычных языков программирования. В этом виде он получил название VDM-SL (VDM Specification Language). Был разработан международный стандарт VDM-SL [VDM-SL],.

Первые удачи авторов и пользователей VDM активизировали интерес исследователей к формальным методам и языкам формальных спецификаций. В 80−90-е годы появилось несколько языков, которые можно назвать наследниками VDM, например, Z и В. Эти языки более строгие, чем VDM-SL, Z вообще чрезвычайно мощный язык. Это обусловило широкое распространение Z и В в университетах и академических центрах. Вместе с тем, о реальных проектах, сопоставимых по сложности с разработкой Ада-компилятора и выполненных при помощи этих языков, не известно.

Это объясняется тем, что развитие языков спецификации и формальных методов, в основном, стимулировалось задачами аналитической верификации и задачами конструирования моделей (и затем программ), правильных по построению. Увлекаясь поставленной целью, разработчики языков и методов оставляли без должного внимания проблему переноса результатов, полученных в теории и в экспериментах, на реальные программные проекты. В частности, в последние 10 лет большое внимание уделялось так называемой «проверке моделей» (model checking). Здесь были получены интересные результаты, но нет никаких общих решений для задачи переноса собственно модели и сопутствующих артефактов, например тестов, из фазы моделирования/прототипирования в фазу реализации. Одной из первых работ, которая попыталась связать тематику формальных методов с тестированием ПО была работа [Gourlay].

Исследования видов жизненного цикла, работ и артефактов, которые типичны для каждой из фаз жизненного цикла, привело к появлению понятия «процесс разработки ПО». Различные виды процессов, способы их описания, способы их внедрения в практику привлекли к себе особый интерес после того, как исследования по проблемам качества ПО и, в частности, проблемам оценки качества, показали, что к решению задачи повышения качества ПО следует идти через улучшение качества процессов разработки ПО. Эта мысль является сейчас преобладающей в мировом сообществе разработчиков ПО. Имеются международные стандарты качества ПО [IS09000], методологии поэтапного повышения качества процессов разработки [СММ], системы сертификации, позволяющие по объективным характеристикам оценить качество процессов разработки ПО в той или иной организации, например, ISO/IEC 15 504.

Непосвященный читатель должен удивиться, узнав, что, с одной стороны, проблемы качества настолько детально изучены, что уже есть стандарты, позволяющие построить производство ПО с любым заданным уровнем качества, с другой стороны, найти программный продукт, который с точки зрения того же читателя можно безусловно назвать качественным — задача непростая. В чем же дело? Одной из причин такой ситуации является чрезвычайная громоздкость как самих стандартов, так и процессов, которые они описывают. Возникает проблема, состоящая в том, что, с одной стороны, все, что рекомендуется стандартами, является разумным и важным, но внедрить даже необходимый минимум чрезвычайно трудно. Автор видит единственный выход из этого положения: отказываться от требований стандартов нельзя, однако надо большую часть работ сделать простой, рутинной и в максимальной степени переложить работу на плечи компьютера. Последнее означает, что все больше артефактов должно быть формальными, поскольку с «неформальной» документацией компьютеры в общем случае работать не могут. Помимо собственно формализации артефактов, важно, чтобы в процессе разработки использовался некоторый единый формализм, либо совокупность формализмов с формально описанными взаимосвязями. Только это позволит внедрить соответствующие методы и инструменты в реальные процессы. Иначе, улучшив или даже полостью автоматизировав.

16 одни виды работ, легко получить ситуацию, когда результаты этих «автоматизированных» действий практически непригодны для использования в других работах.

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

Первые, классические работы по формальным методам в разработке ПО, появились в период 50−60-х годов Основные результаты этого периода связаны с именами Ляпунова, Янова, Бекуса, Флойда, Хоара. Про наиболее значимые результаты 70−80 годов уже говорилось выше. В 80−90-е годы активно разрабатываются и внедряются языки спецификаций, ориентированные на использование в массовом программировании. Такими языками можно назвать SDL и RSL — язык спецификации метода RAISE (Rigorous Approach to Industrial Software Engineering) [RSL, RAISE], которые разрабатывались не столько для академических исследований и экспериментов, сколько для использования в промышленности. Судьба SDL вполне успешна, он широко применяется, правда только в телекоммуникационной индустрии. RAISE, как и все остальные языки спецификаций и формальные методы разработки общего назначения, не столь успешен: RAISE знают и используют в нескольких университетах и не используют в промышленности. 90-е годы примечательны тем, что огромную популярность завоевал язык описания моделей UML, и широкую известность получили исследования по архитектуре объектно-ориентированных (ОО) систем. На практике использование UML, в основном, ограничиваются моделированием архитектуры. Как средство описания функциональности, он достаточно слаб2.

Активное использование SDL и, в особенности, UML показывает, что средства работы с моделями, появившиеся в последние годы, уже.

2 Этот пробел пытаются восполнить в новом стандарте языка UML 2.0.

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

Выводы.

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

Схема жизненного цикла развития ПО, основанная на формализованных и формальных методах разработки.

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

• Определение требований.

• Проектирование и разработка.

• Тестирование.

• Сопровождение.

На каждой из фаз жизненного цикла формальные методы вносят следующий вклад:

• Определение требований. На этой фазе формальные методы упрощают строгое и/или формальное описание предметной области, бизнес логики, общих представлений об архитектуре будущей реализации. Результаты фазы представляются не только в форме документации на естественном языке, но и в виде формализованных и/или формальных описаний, что, в свою очередь, становится фундаментом для строгого описания интерфейсов, собственно функциональных требований к реализации, требований к тестам. Формализация критериев проверки требований и критериев полноты тестирования в целом закладывает базу для отслеживания (трассировки) требований на всех последующих фазах жизненного цикла.

• Проектирование и разработка. Здесь формальные методы используются при уточнении требований, трансформации требований в сценарии использования и архитектурные решения, при увязке сценариев и архитектурных решений с функциональными требованиями. Более подробное рассмотрение потенциала формальных методов на этой фазе показывает, что они существенно упрощают анализ описаний требований, сценариев использования и архитектурных решений на предмет проверяемости выполнения требований, анализ непротиворечивости и полноты требований. Формальные методы предоставляют методологическую базу для последовательного уточнения проектной документации. Еще один важный вклад — поддержка так называемого ко-верификациОнного процесса — синхронизованной разработки собственно реализации и тестов на основе согласованных формальных спецификаций. Документирование на основе формальных спецификаций носит более систематический характер и позволяет автоматизировать поддержку документации в актуальном состоянии. Разработка и ведение формальных спецификаций хорошо согласуется с целевой (направленной) инспекцией кода, в основе которой лежат проверки требований стандартов программирования и отдельных требований проекта. Например, это дает строгую базу для контроля за четким описанием и проверкой областей применимости (пред-условий) инспектируемого ПО.

Формальные методы в жизненном цикле тробомн и f—Л Определение | У I требований I.

Тестирое*ни* w Автоматическое тестирование.

Тестирование. Использование формальных методов позволяет существенно сократить трудоемкость и длительность фазы тестирования. Это обеспечивается, во-первых, за счет того, что тесты разрабатываются из формальных спецификаций или моделей, которые создаются еще во время проектирования — это позволяет выиграть время и завершить разработку большей части тестов до завершения реализации. Во-вторых, поскольку спецификации и модели — это материал, который хорошо приспособлен для повторного использования (reuse), общая трудоемкость разработки снижается. Решению задачи повышения доли повторно используемых спецификаций и тестов также служит механизм сопряжения абстрактных (спецификационных) и реализационных интерфейсов. Обычно такие средства называются адаптерами или медиаторами. Их использование в еще большей степени сокращает затраты на разработку тестов.

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

В расширенном варианте схема жизненного цикла включает также анализа так называемого унаследованного ПО (legacy software), спецификации облегчают анализ проблем, обратную инженерию, перепроектирование и др.

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

Предложенная схема жизненного цикла ПО отвечает требованиям современных стандартов в этой области: СММ, ISO 9000−2000, ISO/IEC TR 15 504, IEEE 830,829.

Остановимся несколько подробнее на структуре ко-верификационного процесса. Особенности этого процесса хорошо видны из сопоставления схемы жизненного цикла, которая описана в работе [Калбертсон], со схемой ко-верификационного процесса. В данном случае рассматривается схема жизненного цикла на основе прототипирования. Она очень близка к современным представлениям о том, как должен быть устроен итеративный процесс разработки. В частности, здесь устранены многие проблемы классической «каскадной» схемы жизненного цикла, где предполагается, что все работы по проектированию и разработке целевой системы можно выстроить в некоторую последовательность с четко заданными входными данными и результатами работ. Недостатком каскадной схемы является то, что работы по созданию различных видов тестов не объединены между собой и никак не объединены с собственно процессом проектирования разработки ПО. За счет этого теряются потенциальные преимущества от взаимодействия разработчиков и тестировщиков, что приводит ко многим ошибкам, не только программирования, но и проектирования.

Рисунок 2. Традиционная схема жизненного цикла. В схеме ко-верификационного процесса появляется возможность вести разработку самого ПО и создание его тестов параллельно. Основой такого процесса служат формальные спецификации программ.

Разработка архитектуры и определение интерфейсов.

Уточнение ио Уточнение спецификаций о п спецификаций.

Рисунок 3. Схема ко-верификационного процесса.

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

Выводы.

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

Предложенная схема жизненного цикла позволяет повысить качество ПО и сократить общие затраты на разработку, тестирование и сопровождение за счет высокого уровня повторного использования компонентов верификационного набора.

Спецификация и тестирование программных интерфейсов1.

В этой секции описываются наиболее значимые результаты в рамках данного исследования. Онибыли получены при разработке методов тестирования программных интерфейсов на основе их формальных спецификаций. В концептуальном плане особенностью данного подхода является идея генерации теста не по исходному тексту программы, а по тексту формальной спецификации. Идея сама по себе достаточно проста, однако для ее реализации необходимо располагать техникой разработки подходящих спецификаций, методами их анализа и, собственно, генерации тестов. Заметим, что тогда, когда эти работы начинались, не было очевидно, что из моделей (подразумевается, достаточно простых) вообще можно сгенерировать качественный тест для реальной программной системы. Не очевиден был и ответ на вопрос о том, как должен выглядеть такой тест.

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

1 Первая публикация соискателя по построению требований к тестовому набору на основе преди пост-условий была опубликована в 1994 [3]. Апробация предложенного подхода и дальнейшее развитие методов формальной спецификации и генерации тестов из формальных спецификаций началась в середине 1994 в рамках работ ИСП РАН над формальной спецификацией программного интерфейса ядра операционной системы реального времени. К началу 1997 года был создан первый комплект формальных спецификаций и технология генерации тестов из таких спецификаций. Данный пакет спецификаций до сего времени является самым крупным в европейской базе данных приложений формальных методов [FME]. Группой под руководством соискателя была разработана технология KVEST — технология тестирования программных интерфейсов на основе использования формальных спецификаций. удается не всегда. Что же делать в этом случае? В этом случае предлагается генерировать каркас (framework), полностью задающий общую архитектуру тестового набора, те компоненты, которые удается сгенерировать, и гнезда для тех компонентов, которые сгенерировать не удается. Наличие в общем случае как автоматически сгенерированных компонентов, так и разработанных вручную, и необходимость достаточно частой перегенерации тестовой программы, поскольку тестирование, как и программирование, требует экспериментов, предъявляют высокие требования к тщательности разработки архитектуры тестовой программы. Важна четкая проработка связей, как между компонентами тестовой программы, так и между исходными данными генерации тестов (например, спецификациями) и компонентами, которые из них генерируются или разрабатываются вручную на их основе. Для описания всей совокупности компонентов и их связей при разработке спецификаций и тестов автором введено понятие верификационного набора.

Схема верификационного набора.

Исходные данные для тестирования С.

Спецификации.

I I Модель теста.

Генератор тестового набора 1.

Тестовые оракулы.

Инструментальная машина Е Итераторы ^.

Тестовые сценарии.

Фильтры.

Целевая машина.

Компилятор на целевой язык программирования f Тестевы. А Г Итератор тестовой f Обходчик I 11 последовательност 11 конечного I.

V ор" упы VV «VV J.

Тестовая программа.

Рисунок 4.

Схема разработки тестов на основе спецификаций выглядит следующим образом.

Фаза 1. Определяется интерфейс программного компонента или подсистемы, состоящей из таких компонентов. Этот интерфейс должен быть достаточно богат, чтобы обеспечить проверку поведения системы в разнообразных тестовых ситуациях, и, с другой стороны, должен быть не чрезмерно большим, чтобы уложиться в ограничения на ресурсы, выделяемые на тестирование.

Фаза 2. Совокупность сущностей, включенных в состав интерфейса, задает основу для разработки формальной модели поведения целевой системы. Описание поведения этой системы и есть собственно спецификация программы. Основной вид спецификаций, который используется в предлагаемом подходе, — это так называемые имплицитные спецификации (спецификации в виде ограничений). Ограничения представляют собой преди пост-условия для операций и ограничения (инварианты) для типов данных (для классов, в случае 00 программирования).

Фазы разработки верификационного набора (вариант обратной инженерии).

Рисунок 5.

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

Фаза 3. Тестовый сценарий в рамках рассматриваемой техники создается либо на основе сценариев типового использования системы (use cases), либо на основе некоторой абстрактной модели теста. В последнем случае модель представляет собой конечный автомат. Состояния такого конечного автомата должны соответствовать состояниям целевой системы (или классам состояний целевой системы), а переходы должны соответствовать вызовам операций с определенными параметрами (либо классам таких вызовов). В рамках данной работы основное внимание уделяется подходу на основе имплицитных конечных автоматов, поскольку этот подход зарекомендовал себя наилучшим образом. Входной алфавит конечного автомата при тестировании программного интерфейса программной системы есть полный перечень всех операций со всеми возможными комбинациями значений входных параметров (включая значения глобальных переменных или других видов входных данных). Выходной алфавит — все возможные результаты всех операций. Если не учитывать количественные ограничения на размер тестовой последовательности, то прямолинейное решение задачи генерации тестовой последовательности по заданному конечному автомату вполне реально. Однако, такое решение будет практически полезным только для автоматов с крайне ограниченным числом состояний, переходов и ограниченным размером входного алфавита. В ИСП РАН был разработан метод факторизации конченых автоматов, используемых для генерации тестовых последовательностей. Кроме того, была разработана техника так называемого неявного (имплицитного) задания конечного автомата. Эта техника позволяет сократить размер описания конечных автоматов до нескольких десятков строк даже для приложений, чей исходный текст измеряется сотнями и тысячами строк (см. [Бурдонов]).

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

Общая архитектура верификационного набора представлена на следующем рисунке.

Архитектура верификационного набора.

Тестовый сценарий.

Драйвер L сценария t.

Обходчик автомата.

Спецификации j И Модель —-1 данных.

Тестовый оракул.

Медиаторы I Ц % Java/C/C+.

——-J V jJC-Л.

Анализатор тестового покрытия.

Тестируемая система.

Рисунок 6.

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

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

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

2 Часто их называют «средствами автоматизации тестирования», в отличие от «средств автоматической генерации тестов».

• отсутствие прямой и ясной связи между требованиями (их спецификациями) и тестами усложняет управление требованиями и регрессионное тестирование;

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

Взгляд на тестирование на основе формальных спецификаций с позиций верификации.

Задачу тестирования на основе спецификаций можно рассматривать как решение двух подзадач:

• тестирование собственно реализации и.

• проверка соответствия реализации и модели (обычно это называется тестированием соответствия или conformance testing).

В случае тестирования собственно реализации нас удовлетворила бы схема, показанная на Рисунке 7.

Ор in -> out pre-Op (in) = true => post-Op (in, out) = true.

Здесь используются следующие обозначения:

• Op — операция в модельном или реализационном пространстве.

• in, out — входные и выходные.

• рге-Ор — предусловие операции Ор

• post-Op — предусловие операции Ор

Рисунок 7.

То есть, тестирование должно показать, что при входных данных, удовлетворяющих пред-условию операции Ор, всегда выполняется постусловие этой операции.

Что меняется при совместном рассмотрении поведения модели и реализации? В этом случае мы должны провести испытания и для модели, и для реализации. Эти испытания должны проходить в «сходных» условиях (нельзя требовать, чтобы это были одни и те же условия, так как модель и реализация работают с разными данными — в разных пространствах данных), мы должны убедиться, что модель и реализация дали «сходные» результаты (опять заметим, что по той же причине нельзя ожидать «одни и те же результаты»).

Понятию «сходный» мы должны придать строгое значение. С этой целью задается отношение между данными реализационного и модельного пространства. Собственно отношение задается функцией абстракции или возвращающей функцией retr (эта техника часто используется в работах по аналитической верификации моделей). Эта функция определена на всех значениях входного реализационного пространства данных. Каждому реализационному экземпляру данных она сопоставляет некоторый модельный экземпляр. Имея такую функцию мы можем, выбрав очередное входное данное для тестирования реализационной операции Op-impl, провести его конвертацию и результат использовать как входное данное для модельной операции Op-mod. При этом важно убедиться, что предусловия обеих операций Op-impl и Op-mod выполнены. Так мы можем получать «сходные» входные данные.

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

Opmod.

OUT retr in.

Opjmpl retr out.

Обозначения:

• Opmod — операция в модельном (спецификационном) пространстве.

• Opjmpl — операция в реализационном пространстве.

• in, out — входные и выходные данные в реализационном пространстве.

• IN, OUT — входные и выходные данные в модельном пространстве.

• retr — восстанавливающая функция.

Рисунок 8.

Аналогичные диаграммы имеет смысл рассматривать для анализа того, что происходит при тестировании 00 классов, объектов и других программных сущностей, представляющих собой наборы операций и данных. При их тестировании приходится составлять тестовые.

IN.

Opimod OUT/IN op2mod OUT retr retr in.

OpiJmpI out/in OpzJmpI out.

Рисунок 9. последовательности — последовательности вызовов методов, функций, процедур или других видов операций.

В первом приближении диаграмма, которая иллюстрирует работу тестовой последовательности, сравнивающей поведение реализации и модели, показана на рисунке 9.

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

Решение этой проблемы было найдено группой под руководством автора. Оно состоит в том, чтобы там, где это возможно, пользоваться обратным к retr преобразованием, а там, где это невозможно, пользоваться данными, вычисленными на предыдущих шагах тестовой последовательности. В частности, нередко следующая операция в этой последовательности получает в качестве аргумента результат предыдущей (либо как явный параметр, либо как значение переменных/полей). То есть, когда это необходимо, мы будем генерировать входные данные для модели непосредственно в пространстве модельных данных, входные данные для реализации либо конвертировать при помощи обратного преобразования retr" 1, либо использовать уже имеющиеся значения из реализационного пространства, вычисленные на предыдущих шагах. Диаграмма, представляющая тестовую последовательность в случае тестирования на основе спецификаций, будет выглядеть следующим образом: tfb.

IN Opimod OUT IN Opzmod OUT retr'1 i.

I. retr retr in OpiJmpI out in OpaJmpI out.

Рисунок 10.

На этой диаграмме появились пунктирные линии с обозначением retr" 1. Это обратные преобразования по отношению к retr3. Пунктир здесь указывает на то, что такое преобразование не всегда возможно4 и не всегда необходимо, так как часть входных данных, как для модельного, так и для реализационного пространства данных строится за счет побочных эффектов предшествующих операций тестовой последовательности.

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

3 В KVEST эта пара преобразований называется impl-to-mod (от реализации к модели) и mod-to-impl (от модели к реализации).

4 Обратное преобразование в общем случае является неоднозначным и часто требует громоздких вычислений.

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

Функциональное тестирование должно решить следующие задачи. Во-первых, требуется построить достаточно представительный5 набор примеров (тестовых данных, тестовых ситуаций, тестовых случаев). Затем для каждого из элементов этого набора следует показать, что.

1 — Пост-условие реализации не нарушено: pre-Op-impl (in) => post-Op-impl (in, Op-impl (in)).

2 — Пред-условия модели не слабее пред-условий реализации: pre-Opmod (retr (in)) => pre-OpJmpl (in).

3 — Пост-условия реализации не слабее пост-условий моделиpre-Opmod (retr (in)) & post-OpJmpl (in, Opimpl (in)) => eq (retr (Opimpl (in)), Opmod (retr (in))), где eq — функция, задающая определение эквивалентности в случае, если модель задана явно, то есть как исполнимая спецификация, и задана функция эквивалентности или pre-Opmod (retr (in)) & post-OpJmpl (in, OpJmpl (in)) => post-Opmod (retr (in), retr (Opimpl (in))) в случае неявной спецификации, в форме преди пост-условий.

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

Пост-условия реализации не слабее пост-условий модели: pre-Opmod (retr (in)) => post-Opmod (retr (in), retr (OPimpl (in))).

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

06 этом сказано, например, в [24].

Заметим, что функция retr в реальных условиях может быть не определена для некоторых входных значений (более точно, иногда она вместо конвертации будет сообщать о невозможности провести конвертацию). Попытка вычислить retr для таких «запрещенных» значений означает, что при тестировании встретилась ситуация, когда модель (спецификации и средства отображения реальных данных в модельные) и реализация не соответствуют друг другу. Это, в свою очередь, означает, что надо искать дефект либо реализации, либо спецификации, либо в функции абстракции.

Выводы.

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

Спецификация и тестирование компиляторов6.

Компиляторы, в некотором плане, — один из наиболее перспективных объектов для применения формальных методов. В них соединились два условия, крайне необходимых для успешного применения формальных методов:

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

• структуры данных, с которыми оперирует компилятор, отлично документированы (описание входного языка, формат объектного модуля, набор команд машины и др.).

Кроме того, важно, что, как правило, разработчики компилятора не сталкиваются с проблемами недетерминизма, невоспроизводимости результатов и другими проблемами такого сорта, которые типичны, например, для операционных систем, СУБД, распределенных систем. Это облегчает анализ работы компилятора, в частности, его тестирование.

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

6 Автор начал заниматься вопросами формализации тестирования в конце 80-х годов. Первая публикация автора по использованию формальных спецификаций для тестирования компиляторов была опубликована в 1992 г. [2]. Апробация методики построения тестов для компиляторов была завершена в 1992 г. в проекте создания компилятора языка программирования реального времени для космического корабля «Буран».

Актуальность темы

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

Первая публикация автора по формальным методам была посвящена методике ручного создания тестовых наборов для семантических анализаторов [2]. Идея состояла в том, чтобы по структуре well-formed функций построить метрику тестового покрытия блока семантического анализа.

Было показано, что для компилятора языка, близкого к Modula-2/Modula-3, удобная метрика строится естественным образом. В терминах метрики формулируются требования к тестам — программам на целевом языке. Затем по этим требованиям тестировщики, имея лишь общие знания.

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

В данной работе использовался язык спецификаций Meta-IV и Венский метод разработки программ VDM [VDM], Опыт построения собственно формальных спецификаций языка программирования показал еще одну привлекательную сторону формальных методов, состоящую в следующем. Проектирование спецификаций — сложный процесс, тем не менее, обычно, он может быть завершен существенно быстрее собственно реализации и при этом часто вскрывает проблемы в постановке задачи7, с которыми разработчики нередко сталкиваются лишь на финальных этапах разработки, когда менять постановку задачи поздно. Спецификация позволяет ускорить обнаружение такого рода проблем, что существенно упрощает их устранение.

Работы автора по тестированию компиляторов 90−94 годов не пошли дальше ручных методик и ограничивались использованием только спецификации статической семантики языков программирования. В 2001 году произошел возврат к этой тематике, при этом в круг интересов были включены задачи тестирования back-end, а именно, блоков оптимизации и.

1 В контексте языков программирования — это проблемы уточнения семантики языковых конструкций. генерации кода. Основные результаты были получены группой, которая занималась сначала разработкой и тестированием транслятора и генераторов программ-тестов в наборе инструментов J@T [Демаков], а затем участвовала в проектах по грантам РФФИ и компании Интел. Результаты исследований [21, 23] показали, что тестирование сложных оптимизационных преобразований возможно на основе относительно простых моделей. Для всех исследованных видов оптимизации процент покрытия тестами исходного текста реализации компилятора GCC (соответствующих блоков компилятора) достигал 75−95% при относительно простых моделях, использованных для генерации тестов. Такой уровень покрытия, с одной стороны, вполне приемлем для задач промышленного тестирования, а, с другой стороны, при необходимости, может быть улучшен без значительных затрат при помощи усложнения моделей.

Общая схема процесса тестирования блоков компилятора на основе моделей выглядит, как показано на рисунке 11.

Как видно, в целом данная схема процесса «моделирование/тестирование» очень близка к схемам, показанным на рисунках 4 и 5, что еще раз позволяет указать на широкую применимость подхода к тестированию на основе формальных спецификаций или моделей.

Рисунок 11.

Выводы.

Были разработаны способы использования формальных спецификаций языков и формальных моделей языков для автоматической генерации тестов компиляторов и других процессоров формальных текстов. Предложенные способы были использованы для разработки систем тестирования компиляторов и их отдельных блоков. Результаты применения предложенных способов показали, что полученное тестовое покрытие существенно лучше покрытия, достигаемого при ручном тестировании.

Введение

формальных методов в процессы разработки ПО.

Как и почти любая новая технология, формальные методы (ФМ) испытывают серьезное сопротивление при попытках их внедрения. Серьезной проблемой является то, что значимый эффект от применения формальных методов обычно заметен только на средних и крупных проектах, а провести широкомасштабный эксперимент на таких проектах почти никогда не удается в силу высоких рисков.

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

Почему же до сих пор программисты и их менеджеры не рискуют повсеместно внедрять формальные методы хотя бы там, где это важно, например, при разработке критичных по безопасности систем, базового ПО, крупномасштабных банковских систем, и т. п. Что же мешает программистам переступить через черту и начать разработки их ПО по новому?

Этому вопросу посвящено много работ. Хороший обзор дан в [Stidolph]. Но наряду с реальными проблемами, есть и «мифы», чье влияние, возможно, сдерживает продвижение формальных методов сильнее, чем реальные трудности. К числу таких мифов, в первую очередь, относятся:

— ФМ — это чисто аналитический подход, который может применяться только к относительно простым моделям;

— ФМ требуют математического университетского образования и навыков, которые не типичны для инженеров-программистов;

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

Собственно результаты данной работы как раз и демонстрируют, что перечисленные выше утверждения, если и были верны еще несколько лет назад, то сейчас стали уже лишь мифами. Рассмотрим эти мифы более внимательно:

— ФМ — это чисто аналитический подход.

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

— ФМ требуют математического университетского образования.

Верно лишь то, что, обычно, математическое образование помогает как программистам, так и тестировщикам. Известно, что в учебных программах западных университетов, выпускающих специалистов по ПО (software engineering, IT technologies, database systems и др.), математическим дисциплинам уделяется меньше внимания, чем в российских вузах. Вместе с тем, в целом западные университеты выпускают специалистов, которые удовлетворяют требованиям промышленности разработки ПО. Заметим, что сейчас студентов учат не только языкам программирования, операционным системам и другим, ставшим уже классическими, дисциплинам. В программы практически всех университетов включены курсы по методам 00 анализа, моделированию на базе UML, методам анализа качества программных продуктов и процессов разработки ПО. По сути, эти дисциплины и закладывают тот уровень знаний, который необходим для специалистов по ФМ: аналитикам, разработчикам спецификаций, проектировщикам тестов. Заметим, что мы назвали «проектировщиков тестов», но не назвали «разработчиков тестов» и «тестировщиков», тех, кто обычно работает с пакетами регрессионного тестирования, ведет сбор и анализ результатов, формирует отчеты, и т. д. Эти виды деятельности могут выполняться техническим персоналом даже без специального образования. В качестве подтверждения этого можно сослаться на опыт передачи технологии регрессионного тестирования, разработанной в ИСП РАН, в компанию Nortel Networks и опыт проведения тренингов по технологии UniTesK, где в число обучающихся входили студенты 3−4 курсов различных вузов и инженерный персонал.

— Использование ФМ удлиняет сроки разработки.

Есть задачи, где использование ФМ не требуется. Как правило, это задачи, для решения которых имеется многократно апробированная техника, дающая вполне приемлемые результаты, как по техническим характеристикам, так и по стоимостным. В таких, почти идеальных условиях, внедрение ФМ вряд ли принесет полезный эффект. При разработке крупных программных комплексов всегда приходится встречаться с новыми задачами. Для их решения нет ни апробированных техник, ни людей, которые такие задачи уже решали. В таких ситуациях грамотное использование ФМ не удлиняет общие сроки разработки и не удорожает разработку. Это происходит за счет того, что ФМ помогают лучше понять задачу и ограничения на ее решение. Понимание, важное как для разработчиков, так и для заказчика, наступает раньше, по сравнению с ситуацией, когда используются традиционные схемы разработки. Почему? Потому что разработка формальных спецификаций, формальных моделей привлекает внимание к моментам, которые при традиционном проектировании ускользают от внимания. Полезный вклад здесь дают нестандартные парадигмы разработки спецификаций, в частности, стиль неявных (implicit) спецификаций, работа над функциями повышения и понижения уровня абстракции (функции retr и retr" 1), факторизация и другие виды редукции конечных автоматов или других моделей переходов, введение абстрактных механизмов для представления времени, асинхронных взаимодействий, и т. п.

Практически все специалисты, кто выполнял проекты с разработкой формальных спецификаций, отмечают высокое качество проектной документации, которое удается достичь при прочих равных условиях. Это, в свою очередь, объясняет высокое качество кодирования (собственно программирования) по такой проектной документации.8 Имеется много подтверждений этого факта, в том числе и на опыте работ ИСП РАН по заказам разных компаний. Прямым следствием повышения качества программирования является сокращение затрат на сопровождение ПО. Известно, что затраты на сопровождение ПО часто превышают затраты на разработку. Однако при этом важно заметить, что сопровождение ПО с большим количеством ошибок существенно дороже сопровождения качественного ПО. Тем самым, суммарная стоимость жизненного цикла программной системы, разработанной с использованием ФМ, как правило, меньше стоимости аналогичной программной системы, разработанной по традиционной схеме.

— Внедрение ФМ требует крупномасштабной программы—.

Использование ФМ в цикле разработки не требует кардинальной перестройки процессов в организации или в команде разработчиков. Опыт проведения тренингов и передачи технологии UniTesK в другие коллективы показал, что курса длиной в 4−5 дней достаточно для начала использования UniTesK методов и инструментов. При этом ФМ могут использоваться фрагментарно, то есть, для целей проектирования, или для целей разработки тестов, или для целей отслеживания требований и т. д. Даже при использовании ФМ типа UniTesK на одной из фаз жизненного цикла, разработчики смогут извлечь немало выгод из этого подхода.

С другой стороны, надо признать, что ФМ подталкивают к улучшению процессов разработки. ФМ не только показывают слабые.

8 См. например, работу [FMA-Tale], где сравнивается работа нескольких групп программистов над одной и той же задачей. Часть групп использовала ФМ, часть — нет. Статистика показала, что и время и качество реализации были существенно лучше в группах, которые включили в процесс разработки создание формальных спецификаций. стороны в имеющихся процессах (например, нечеткая проектная документация, нестыковки при переходе от одних фаз работ к другим, плохие связи между группами разработчиков, отсутствие привязки требований к тестам и проч.), что само по себе достаточно полезно. ФМ подсказывают конструктивные решения выявленных проблем. ФМ полезны везде, где недостает четкости, однозначности, явно выделенных связей, индивидуальных и инвариантных свойств данных и операций.

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

— Переход с уровня 1 на уровень 2 — Управление требованиями, что, в частности, предполагает создание ясной и недвусмысленной проектной документации и сквозную систему отслеживания требований через все фазы от проектирования до разработки и пропуска тестов. Обеспечение качества ПО (quality assurance) — Практически все виды использования ФМ ведут к повышению качества. Напрямую с повышением качества связаны формальные методы, использующиеся для верификации и валидации ПО.

— Переход с уровня 2 на уровень 3 — Кооперация групп, что требует языка обмена знаниями. Формальные спецификации — это прямой путь к решению проблемы лучшего взаимопонимания групп. Инженерия ПО. Эта область проблем связана с построением и анализом архитектур целевого ПО на основе некоторых систематических подходов, что позволяет избавиться от риска субъективных решений, обусловленных либо индивидуальными предпочтениями разработчиков, либо сиюминутными, не всегда осознанными соображениями. ФМ вносят решающий вклад в решение этой группы проблем. В первую очередь, здесь надо назвать возможности ФМ при моделировании архитектуры (сюда, в частности, относятся как методы объектно-ориентированного проектирования, так и методы объектно-ориентированного анализа), формальное описание программных контрактов, фиксация знаний о программных контрактах в результате работ по обратной инженерии ПО (reverse engineering).

— Переход с уровня 3 на уровень 4 — На 4-ом уровне СММ имется только две ключевые области — это управление качеством (software quality management) и управление разработкой на основе количественных методов (quantitative process management). В обоих случаях ФМ дают хорошую основу для определения метрик. Известны работы по метрикам сложности программ. Использование формальных спецификаций как исходных данных для генерации тестов позволило ввести новые метрики для оценки полноты тестирования. Такие метрики напрямую связаны с функциональными требованиями к системам, поэтому оценки полноты тестирования на основе таких метрик в большей степени отвечают интересам практики, чем метрики, которые строятся на основе структуры реализации.

— Переход с уровня 4 на уровень 5 — Переход на 5-й уровень СММ предполагает рассмотрение исключительно вопросов оптимизации собственно процессов разработки9, это управление изменениями процессов и внедрение новых технологий. Однако и здесь ФМ находят свое применение. Известны работы по моделированию процессов разработки. Такого рода модели позволяют выявить слабые места в организации и оценить сложности при модернизации процессов — именно эти вопросы и являются центральными при переходе на 5-й уровень СММ.

Итак, факторами, на которые следует опираться при внедрении ФМ, в первую очередь, являются следующие моменты:

• ПО как таковое и артефакты, составляющие предмет конструирования и анализа, достаточно хорошо формализуемына это надо постоянно обращать внимание и пользоваться этим обстоятельством максимально широко.

9 Предполагается, что качество программного продукта уже не требует улучшения.

• Формальные спецификации позволяют существенно «компактифицировать» документацию — что делает ее более эффективной.

• Формальные спецификации всегда могут быть подвергнуты машинному анализу или другой обработке, что открывает широкие перспективы к сокращению как сроков разработки, так и затрат человеческого труда, а, следовательно, к сокращению количества ошибок в программах.

Основной фактор успеха внедрения ФМ — это готовность команды разработчиков/организации преодолеть стереотипы сложившихся процессов разработки. Заметим, что внедрение ФМ не означает полную ломку технологических процессов в сложившемся коллективе. Более того, часто формализация сначала заменяется лишь систематизацией некоторых артефактов и технических, ручных приемов (см. опыт внедрения методики разработки тестов для компиляторов [2]). Там, где фаза систематизации завершена, можно переходить сначала к строгому, и лишь потом к формальному описанию требований и моделей целевой системы. Опыт разработки и использования формальных спецификаций показывает, что даже частичная спецификация и спецификация, которая создается на бумаге и не обрабатывается соответствующими инструментами, способна принести существенную пользу — спецификатор лучше понимает проблему, часто открывает «белые пятна» и противоречия в неформальной документации. Наличие формальных моделей хорошо сочетается с процедурами инспекции кода, в этом случае эффективность инспекции существенно возрастает.10.

Внедрение ФМ в практику не следует рассматривать как некоторую изолированную активность. В действительности, цели которые мы преследуем, используя ФМ, те же, что и цели, объявленные исследователями и ассоциациями программистских компаний, цели, связанные с улучшением качества процессов разработки ПО и качества.

10 В этом плане надо сослаться на близость этой идеи к подходу авторов концепции СММ, которые также акцентируют внимание не на идеальном процессе разработки программ, а на постепенном, пошаговом его улучшении. собственно ПО. Внедрение ФМ не идет вразрез с моделями процессов разработки ПО OMG [OMG], RUP [RUP] и др. Наоборот, опора на эти модели и стандарты качества и на модель зрелости процессов СММ упрощает внедрение ФМ в процессы разработки ПО.

Методы внедрения ФМ в реальные процессы были апробированы в нескольких промышленных и научно-исследовательских проектах. Среди этих работ большое значение имели следующие проекты:

• Формальная спецификация языка программирования и тестирование компилятора этого языка (ИПМ им. М. В. Келдыша АН СССР) (19 901 992);

• Реверс-инженерия, спецификация интерфейса ядра операционной системы реального времени Nortel Networks и разработка тестов для тестирования ядра 1994;1997;

• Апробация ко-верификационного процесса в проекте ре-инженирии подсистемы управления очередями (Nortel Networks) (1998);

• Регрессионное тестирование ПО Nortel Networks (1999);

• Целевая инспекция кода (Nortel Networks) (2001);

• Формализация требований стандарта прототкола IPv6 и разработка тестов для реализации, выполненной Microsoft Research (2000;2001);

• Совместный проект с Санкт-Петербургским Государственным Университетом по внедрению UniTesK метода на платформе языка программирования С (2002);

• Тестирование отдельных блоков компиляторов шрС, GCC, Ореп64 (гранты РФФИ и Intel) (2001;2003).

В следующей далее таблице приведены виды методик и инструментов, поддерживающих процессы, использующие ФМ, а также проекты, где они были опробованы.

Методическая и инструментальная поддержка.

Фаза Метод или инструмент Апробация.

Определение требований Методы увязки требований и спецификаций IPv6 требования формализованы и трансформированы в тесты.

Проектирование KVEST, UniTesK методы разработки спецификаций, инструменты их анализа, инструменты, RSL анализатор, CTesK, J ®T, VDM++TesK Nortel Networks, Microsoft Research projects.

Разработка то я®и метод разработки тестов компиляторов на основе моделей то же, ИПМ РАН и Intel.

Тестирование то >ма то же.

Обратная инженерия KVEST Nortel Networks.

Выводы.

На основе анализа проблем внедрения формальных методов в промышленные разработки ПО были выявлены причины, тормозящие использование формальных методов. Было показано, что основные аргументы против использования ФМ в промышленности базируются не на объективных фактах, а на традиционных заблуждениях.

Серьезным аргументом против ФМ являются повышенные требования к персоналу (подготовка по математике и знание языков формальной спецификации). Было предложено общее решение этой проблемы — разработка спецификационных расширений универсальных языков программирования. Разработана методика расширения языков программирования для целей спецификации и тестирования, построены расширения для языков С, С++, Java, С#, VDM++.

Заключение

.

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

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

Особенность предложенного подхода состояла в том, что по сути предлагалось получить тесты более высокого качества из моделей, которые содержат реализационных деталей меньше, чем исходный текст, так как являются более абстрактными. Разработанные методики специфицирования и генерации тестов из спецификаций показали, что для промышленного ПО удается достичь тестового покрытия исходного текста около 80−95%, что существенно выше, чем нормы покрытия тестами, принятые во многих промышленных компаниях.

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

На основе развития теории спецификации и тестирования разработаны технология и программные средства создания систем тестирования программных комплексов. Технология допускает адаптацию на различные языковые и операционные платформы, что было продемонстрировано реализацией инструментов семейства UniTesK.

Разработанные методы и средства поддержки формальных спецификаций и автоматизации тестирования внедрены в ряде промышленных проектов. Показана результативность предложенного подхода. Так в ядре операционной системы реального времени, которая уже находилась в эксплуатации около 10 лет, удалось обнаружить более 200 ошибок. В реализации протокола IPv6 была обнаружена серьезная ошибка, которую не удалось обнаружить другим группам тестировщиков.

В дополнение к перечисленным результатам, непосредственно связанным с автоматизацией тестирования, получены важные результаты, выходящие за рамки данной тематики. Во-первых, это методика построения спецификационного расширения языков программирования, которая позволяет отказаться от использования академических языков формальной спецификации в промышленных проектах. Разработаны спецификационные расширения для языков программирования С, С++, С#, Java. Разработано семейство инструментов поддержки разработки спецификаций на этих языках.

11 Композиция неявных спецификаций (преди пост-условий и инвариантов типов данных) и неявных конечных автоматов.

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

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

Продемонстрировано, что предложенный метод разработки спецификаций и автоматизации тестирования применим как при разработке объектно-ориентированного, так и не объектно-ориентированного ПО, при разработке разных видов ПО, в частности, таких как: операционные системы, компиляторы и реализации телекоммуникационных протоколов.

Публикации автора по теме диссертации.

1. А. К. Петренко Венский метод разработки программ — VDM. Неформальное введение// Программирование, N 6,1990.

2. М. В. Борисова, Т. А. Морозова, А. К. Петренко, Т. А. Чацкина. Тестирование компиляторов на основе формальной модели языка//Препринт ИПМ им. М. В. Келдыша АН СССР, N 45,1992.

3. А. К. Петренко Спецификация тестов на основе описания трасс // Программирование, 1, 1993.

4. А. К. Петренко Методы отладки и мониторинга параллельных программ // Програмирование, 3,1994.

5. Крюков В. А., Максимов А. В., Петренко А. К., Полилова Т. А. Иерархическое конфигурационное управление // Программирование, N3, 1994.

6. В. А. Крюков, А. К. Петренко, Ю. В. Трунов, К. Б. Федоров. GRAPHIT-graphic integrated environment for real-time system development// Тезисы межд. конференции Real-Time Data RTD-94, Дубна, июнь 1994.

7. В. Ф. Алексахин, Д. М. Арапов, В. А. Крюков, В. А. Иванов, А. Ю. Вашакидзе, А. К. Петренко Monitoring and debugging in RAMPA // Proc. of 2th Int.Conf. «Software for multiprocessors and supercomputers» Moscow, Sept. 19−23,1994, 309−326.

8. Петренко A.K. и др. Технология программирования// Сборник «Современное состояние и тенденция развития информационных технологий в России», Миннауки, Научный совет по ГНТП «Информатизация России», 1995 г., стр.88−108.

9. I. Burdonov, A. Kossatchev, S. Cheng, A. Petrenko, H.Wong. Formal Specification and Verification of SOS Kernel // BNR/NORTEL Design Forum, June 1996.

Ю.В. А. Крюков, А. К. Петренко Интегрированный подход к разработке крупных программных систем управления реального времени // Труды конференции «Индустрия программирования», Москва, 1996.

11.1. Burdonov, A. Kossatchev, A. Petrenko, D.Galter. KVEST: Automated Generation of Test Suites from Formal Specifications // Proceedings of Formal Method Congress, Toulose, France, 1999, LNCS, pp.608−621.

12.И. Б. Бурдонов, А. В. Демаков, А. С. Косачев, А. В. Максимов, А. К. Петренко Формальные спецификации в технологиях обратной инженерии и верификации программ // Труды Института системного программирования РАН, N 1, 1999, стр. 31−43.

13.Е. А. Кузьменкова, А. К. Петренко. Формальная спецификация программ на языке RSL (методическое пособие по практикуму) // МГУ им. М. В. Ломоносова, Москва, 1999, 57 стр. Е. А. Кузьменкова, А. К. Петренко. Формальная спецификация программ на языке RSL (методическое пособие по практикуму) // МГУ им. М. В. Ломоносова, Москва, 1999, 57 стр.

14. A. Petrenko, A.Vorobiev. Industrial Experience in Using Formal Methods for Software Development in Nortel Networks // Proceedings of Testing Computer Software Conference — TCS 2000, Washington, June, 2000.

15.Е. А. Кузьменкова, А. К. Петренко. Формальная спецификация программ на языке RSL (конспект лекций) // МГУ им. М. В. Ломоносова, Москва, 2001, 107 стр.

16.I.B.Bourdonov, A.S.Kossatchev, V.V.Kuliamin, A.Petrenko. Experiences in using testing tools and technology in real-life applications // Proceedings of SETT'01, India, Pune, 2001.

17.A.K.Petrenko. Specification Based Testing: Towards Practice // Proc. of Andrei Ershov Fourth International Conference PCI'01, Novosibirsk, LNCS, Vol. 2244, 2001, pp. l57−162.

18.I.B.Burdonov, A.V.Demakov, A.A.Jarov, A.S.Kossatchev, V.V.Kuliamin, A.K.Petrenko, S.V.Zelenov. J@va: extension of Java for real-life specification and testing // Proc. of Andrei Ershov Fourth International Conference PCI'01, Novosibirsk, LNCS, Vol. 2244, 2001, pp.301−308.

19.B. Bourdonov, A. S. Kossatchev, V. V. Kuliamin, A. K. Petrenko,. UniTesK Test Suite Architecture// Proceedings of FME'2002 conference, Copenhagen, Denmark, LNCS, No. 2391, 2002, pp. 77−88.

20.A.A.Koptelov, V. V. Kuliamin, A. K. Petrenko, VDM++TesKVDMTool extension for specification based testing // Proceedings of workshop on VDM++, Copenhagen, Denmark, 2002, pp. 1−16.

21.С. В. Зеленов, С. А. Зеленова, A.C. Косачев, A.K. Петренко. Генерация тестов для компиляторов и других текстовых процессоров // «Программирование», Москва, 2003, том. 29, N 3.

22.V.V.Kuliamin, A.K.Petrenko, N.V.Pakoulin, A.S.Kossatchev, I.B.Bourdonov. Integration of Functional and Timed Testing of Real-time and Concurrent Systems // Proc. of Andrei Ershov Fifth International Conference PCI'03, Novosibirsk, LNCS, 2003, (printed).

23.A.S.Kossatchev, A.K.Petrenko, S.V.Zelenov, S.A.Zelenova. Application of Model-Based Approach for Automated Testing of Optimizing Compilers. In Proceedings of the International Workshop on Program Understanding (Novosibirsk — Altai Mountains, Russia), July 14−16,2003, 81−88.

24. В. В. Кулямин, А. К. Петренко, А. С. Косачев, И. Б. Бурдонов. Подход UniTesK к разработке тестов //" Программирование", Москва, 2003, том. 29, N 6.

25.Coverage-driven Automated Compiler Test Suite Generation, A. Kalinov, A. Kossatchev, A. Petrenko, M. Posypkin, and V. Shishkov, Electronic Notes in Theoretical Computer Science, Vol. 82(3), 2003, Proceedings of LDTA'2003.

26. A. Kalinov, A. Kossatchev, A. Petrenko, M. Posypkin, V. Shishkov. Using ASM Specifications for Compiler TestingProceedings of Abstract State Machines// Advances in Theory and Applications 10th International Workshop, ASM 2003.

Ссылки на работы других авторов.

Бурдонов] И. Б. Бурдонов, А. С. Косачев, В. И. Кулямин. Использование конечных автоматов для тестирования ПО// Программирование, № 2, 2000.

Демаков] А. Демаков, С. Зеленов, С.Зеленова. Тестирование парсеров текстов на формальных языках // Программные системы и инструменты. Тематический сборник факультета ВМиК МГУ, Москва, 2001, вып. 2, 150−156. [Калбертсон] Р. Калберсон, К. Браун, Г. Кобб. Быстрое тестирование // «Вильяме», Москва, 2002. В. В. Липаев. Обеспечение качества программных средств.

Методы и стандарты// М., «СИНТЕГ», 2001. Б. Лисков, Д.Гатэг. Использование абстракций и спецификаций при разработке и тестировании программ// М., Мир, 1989. Г. Майерс. Искусство тестирования программ// М., Финансы и статистика, 1989. B.Beizer. Software Testing Techniques. Second edition. Van Nostrand.

Reinholds, N-Y, 1990. R.Binder. Testing Object-Oriented Systems: Models, Patterns, and.

Tools// The Addison-Wesley Object Technology Series, 2000. M. Paulk et al, Capability Maturity Model SM for Software, Version 1.1.

Technical Report CMU/SEI-93-TR-024 ESC-TR-93−177,1993. [FMA-Tale] A.E.Kelley Sobel, M/R/Clarkson Formal Methods Application: An Empirical tale of Software Development// IEEE Transactions on SE 2002, Vol.28,No.3, March, 2002, pp.308−320. [FME] http://www.fmeurope.org/databases/fmadb088.html. [Gourlay] J.S.Gourlay. Introduction to the formal treatment of testing, Software Validation, Proceeding of the Symposium on Software Validation, pp. 67−72,1983. [IS09000] http://www.iso9000.org/ [ISO/IEC] http://www.sei.cmu.edu/iso.

15 504/moreinformation/SPAGOALS .html [JSD] M.A.Jackson. System Development // [JSP] M.AJackson. Principles of Program Design// [OMG] http://www.omg.org.

RAISE] The RAISE Language Group. The RAISE Development Method. Prentice Hall, 1995.

Липаев].

Лисков].

Майерс].

Beizer].

Binder].

СММ].

RSL] The RAISE Language Group. The RAISE Specification Language.

Prentice Hall, 1992. [RUP] http://www.rational.com.

SDL] CCITT Recomendation Z.100: Specification and Description.

Language (SDL). 1992. [Stidolph] D.C.Stidolph, J.Whitehead. Managerial Issues for the Consideration and Use of Formal Methods// LNCS, Vol. 2805, 2003, pp. 170−186. [VDM] D.Bjorner. Software Architectures and Programming Systems.

Designvolume I: Specification Principles — the VDM Approach. Addison-Wesley/ACM Press, 1991. [ VDM-SL] P.G.Larsen, W.Pawlowski. The Formal Semantics of ISO VDM-SL//Computer Standards and Interfaces, Vol. 17, Number 5−6, pp. 585−602, September 1995.

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ.3.

Аннотация.3.

Актуальность темы

3.

Основные цели работы.4.

Научная новизна.5.

Методы исследования.6.

Практическая значимость работы.7.

Апробация.10.

Публикации.11.

ПРЕДЫСТОРИЯ ДАННОГО ИССЛЕДОВАНИЯ И ОБЩАЯ ПОСТАНОВКА ЗАДАЧИ.12.

Выводы.18.

СХЕМА ЖИЗНЕННОГО ЦИКЛА РАЗВИТИЯ ПО, ОСНОВАННАЯ НА ФОРМАЛИЗОВАННЫХ И ФОРМАЛЬНЫХ МЕТОДАХ РАЗРАБОТКИ.19.

Выводы.24.

СПЕЦИФИКАЦИЯ И ТЕСТИРОВАНИЕ ПРОГРАММНЫХ ИНТЕРФЕЙСОВ.26.

Взгляд на тестирование на основе формальных спецификаций с позиций верификации.31.

Выводы.37.

СПЕЦИФИКАЦИЯ И ТЕСТИРОВАНИЕ КОМПИЛЯТОРОВ.38.

Выводы.41.

ВВЕДЕНИЕ

ФОРМАЛЬНЫХ МЕТОДОВ В ПРОЦЕССЫ РАЗРАБОТКИ ПО.42.

Выводы.50.

ЗАКЛЮЧЕНИЕ

51.

ЛИТЕРАТУРА

54.

Публикации автора по теме диссертации.54.

Ссылки на работы других авторов.56.

ЗАКЛЮЧЕНИЕ

51.