Презентация на тему Современные направления проверки правильности программ (лекция 9 )

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

в программировании в 70-х годах прошлого столетия. Они предоставляют средства, облегчающие описание рассуждения о свойствах и особенностях программ в математической нотации.
На формальных спецификациях базируются методы доведения программ, которые были начаты работами по теории алгоритмов А.А. Маркова [1], А.А. Ляпунова [2], схемами Ю.И.Янова [3] и формальными нотациями описания взаимодействующих процессов К.А. Хоара [4] и др..

для описания правильного решения некоторой задачи, для которой она

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

формальном языке и служат для проверки правильности программы в

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

правильности программного продукта.
В настоящее время процессы верификации, валидации

и тестирования ПС регламентированы стандартом ISO/IEC-12207 из жизненного цикла ПС.
В некоторой зарубежной литературе процессы верификации и тестирования на практике отождествляются, они ориентированы на достижение правильности программы.

которые используются для формального описания свойств выполнения программ путем

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

такими средствами:
 2) арифметические операции;
 3) множества и операции над множествами;
 4)

описания последовательностей и операции над ними;
 5) описания функций и операций над ними;
 6) описания древовидных структур;
 7) средства построения моделей областей;
 8) процедурные средства языков программирования (операторы присваивания, цикла, выбора, выхода);
 9) операции композиции, аргументами и результатами которых могут быть функции, выражения, операторы;
 10) механизм конструирования новых структур данных.

доменов;
 
2) описания взаимодействий и параллельного выполнения;
 
3) спецификации языков программирования

и трансляторов;
 
4) спецификации баз данных и знаний;
 
5) спецификации пакетов прикладных программ.
 

предназначены для формализованного описания задач в терминах предметной области,

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

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

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

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

выполнения:
 
- Выполняемая (executable),
 
- Алгебраическая (algebraic),
 
- Сценарная (use case or scenarios),
 
- В ограничениях (constraints).

прототипов систем для достижения установленной цели
Алгебраические спецификации, включают

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

правильной реализации ПО в соответствии со спецификациями, выполняется в

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

программной системы при ее проектировании и после завершения ее

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

и анализ правильности выполнения заданных функций и соответствия ПО

требованиям заказчика, а также заданным спецификациям. Они представлены в стандартах] как самостоятельные процессы ЖЦ и используются, начиная от этапа анализа требований и кончая проверкой правильности функционирования программного кода на заключительном этапе, а именно, тестировании.
Для этих процессов определены цели, задачи и действия по проверке правильности создаваемого продукта (рабочие, промежуточные продукты) на этапах ЖЦ. Рассмотрим их трактовку в стандартном представлении.

(программные, технические и информационные) и взаимодействие объектов (протоколы, сообщения)

в распределенных средах;

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

- Документация к системе;

- Тесты, тестовые процедуры и входные наборы данных.

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

Этот процесс основывается:

- На стратегии и критериям верификации всех рабочих программных продуктов на ЖЦ;

- На выполнении действий по верификации в соответствии со стандартом;

- На устранении недостатков, выявленных в программных (рабочих, промежуточных и конечных) продуктах;

- На согласовании результатов верификации с заказчиком.

или другим сотрудником той же организации или сотрудником другой

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

требования для программного выполнено, и осуществляется это с помощью:
 
-

Разработанной стратегии и критериев проверки всех рабочих продуктов;
 
- Оговоренных действий по проведению валидации;
 
- Демонстрации соответствия разработанных программных продуктов требованиям заказчика и правилам их использования;
 
- Согласование с заказчиком полученных результатов валидации продукта.

лицом, например, заказчиком, осуществляет действия по внедрению и проведению

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

состоит в том, чтобы проверить и подтвердить, что конечный

программный продукт соответствует назначению и удовлетворяет требованиям заказчика. Эти процессы взаимосвязаны и определяются, как правило, одним общим термином «верификация и валидация» или «Verification and Validation» (V & V)
«верификация и валидация» основаны на планировании их как процессов, так и проверки для наиболее критичных элементов проекта: компонентов, интерфейсов (программных, технических и информационных), взаимодействий объектов (протоколов и сообщений), передачи данных между компонентами и их защиты, а также создания тестов и тестовых процедур.
После проверки отдельных компонентов системы проводятся их интеграция, повторная верификация и валидация интегрированной системы, создается комплект документации, отражающей правильность выполнения требований по результатам инспекций и тестирования.

принадлежит описание требований на языке UML с помощью сценариев

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

шагов:
1. Формализованное описание требований в виде сценариев;
 2. Создание модели

требований;
 3. Создание специальных сценариев для валидации требований;
 4. Применение валидационных сценариев в модели требований;
 5. Оценка результатов поведения модели требований;
 6. Проверка условий завершения процесса валидации и при обнаружении каких-либо неточностей повторение шагов, начиная с п. 2.
При выполнении сценариев могут возникнуть ошибочные ситуации, при которых поведения системы становится не детерминированным. В этих целей проводится контроль покрытия сценариев в модели требований валидационных сценариям с целью выявления ошибок или рисков

классов эквивалентности входных и выходных данных для валидации и

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

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

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

требований путем выполнения валидационных сценариев
- Добавление проверенных сценариев к

набору валидационных сценариев и их использование в качестве входных данных для синтеза;
- Поиск ошибок в сценариях и проверка различных композиций сценариев.

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

спецификации: 
- Базовых (простых) объектов ОМ, атрибутами которых являются данные

и операции объекта - функции над этими данными;

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

Доказательство правильности построения ОМ предусматривает:

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

Это доказательство является завершающим при проверке правильности ОМ.

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

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

проверяются с помощью модели проверки, а свойство сложного компонента

- на абстракции компонентов, собранных из примитивов и проверенных их свойств в интегрированной среде.
 
Данный подход может использоваться в распределенных программных системах, функционирующих на платформах типа CORBA, DCOM и EJB.

проверки правильности моделей ПрО, функций в языке API, безопасности

и целостности БД - в проекте SDV фирмы Microsoft и в международном проекте по формальной верификации ПС.
 
Идея создания этого проекта принадлежит Т.Хоару и обсуждалась на симпозиуме по верифицированного ВС в феврале 2005г. в Калифорнии. Затем в октябре того же года на конференции IFIP в Цюрихе был принят международный проект сроком на 15 лет по разработке целостного автоматизированного набора инструментов для проверки корректности ПС [14, 15].

теории создания и анализа программ;

- Построение всеобъемлющего интегрированного набора

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

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

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

объектов и реализаций кодов для различных программных приложений;
 
- Накопление

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