Что такое верификация в программировании
События
- Тестирование
- Основы
- Откуда берутся ошибки в ПО?
- Почему тестирование необходимо?
- Мифы о тестировании
- Психология тестирования
- Когда начинать и заканчивать тестирование?
- Фундаментальный процесс тестирования
- Принципы тестирования
- Верификация и валидация
- QA, QC и тестирование
- Кто занимается тестированием?
- Цели тестирования
- Что такое тестирование программного обеспечения?
- Роль тестирования в процессе разработки ПО
- Сколько стоят дефекты?
- Качество программного обеспечения (ISO/IEC 25010)
- Матрица соответствия требований (Requirements Traceability Matrix)
- Матрица покрытия и Матрица отслеживания
- Тестирование веб-проектов: основные этапы и советы.
- Мобильное и веб-приложение. В чем разница?
- Тест дизайн (Test Design)
- Agile
- Словарь тестировщика
- 75 популярных вопросов на собеседовании QA (+ примеры и ответы)
- HTML и CSS для тестировщиков
- Итеративная модель (Iterative model)
- Спиральная модель (Spiral model)
- V-модель (V-model)
- Каскадная модель (Waterfall model)
- Стадии цикла разработки ПО
- Жизненный цикл ПО
- Приемочное тестирование
- Системное тестирование
- Интеграционное тестирование
- Модульное тестирование
- White/Black/Grey Box-тестирование
- Статическое и динамическое тестирование
- Ручное и автоматизированное
- Тестирование документации
- Интернационализация и локализация
- Стресс тестирование
- Тестирование установки
- Конфигурационное тестирование
- Тестирование на отказ и восстановление
- Юзабилити
- Тестирование сборки
- Тестирование взаимодействия
- Тестирование безопасности
- Дымное тестирование
- Регрессионное тестирование
- Тестирование производительности
- Функциональное тестирование
- Нефункциональное тестирование
- Спецификация требований
- Test Plan
- Checklists для тестировщика
- Test Case
- Bug report
- Жизненный цикл дефектов
- Классификация дефектов
- Тестирование мобильных приложений
- Протоколы
- Протокол TCP/IP или как работает Интернет (для новичков)
- HTTP-запрос (HTTP request)
- Автоматизация
- Автоматизированное тестирование
- Теория по X-Path локаторам
- Как написать X-Path локатор.
- Использование tagname
- Вложенность родительского элемента.
- Как выбрать инструмент автоматизации?
- Базы данных в тестировании
- Зачем нужен SQL для тестирования?
- Общее
- Интерфейс в коде ПО
- Парадигмы программирования «ООП»
- Процесс коммуникации с помощью API
- Рефакторинг Кода
- Фреймворк в программировании
- Микросервисная архитектура ПО.
- Монолитная архитектура ПО.
- Что такое API?
- Что такое JSON
- Что не так с Android?
- Android Studio 2.0
- RxJava
- Основы
- Внутренний мир компьютера: что там внутри
Верификация и валидация
Эти два понятия тесно связаны с процессами тестирования и обеспечения качества. К сожалению, их часто путают, хотя отличия между ними достаточно существенны.
Верификация (Verification) — это статическая практика проверки документов, дизайна, архитектуры, кода, т.д.
- Верификация — это процесс включающий в себя проверку Plans, Requirement Specifications, Design Specifications, Code, Test Cases, Chek-Lists, etc.
- Верификация всегда проходит без запуска кода.
- Верификация использует методы — reviews, walkthroughs, inspections, etc.
- Верификация отвечает на вопрос “Делаем ли мы продукт правильно?”
- Верификация поможет определить, является ли программное обеспечение высокого качества, но оно не гарантирует, что система полезна. Проверка связана с тем, что система хорошо спроектирована и безошибочна.
- Верификация происходит до Validation.
Она содержит все активности которые позволяют достигнуть высокого качества программного обеспечения:
- Inspection in software engineering, refers to peer review of any work product by trained individuals who look for defects using a well defined process. (Faganinspection)
- Walkthroughs In software engineering, a walkthrough or walk-through is a form of software peer review «in which a designer or programmer leads members of the development team and other interested parties go through a software product, and the participants ask questions and make comments about possible errors, violation of development standards, and other problems».
- Reviews In software development, peer review is a type of software review in which a work product (document, code, or other) is examined by its author and one or more colleagues, in order to evaluate its technical content and quality.
Валидация (validation) – это процесс оценки конечного продукта, необходимо проверить, соответствует ли программное обеспечение ожиданиям и требованиям клиента. Это динамический механизм проверки и тестирования фактического продукта.
- Валидация всегда включает в себя запуск кода программы.
- Валидация использует методы, такие как тестирование Black Box, тестирование White Box и нефункциональное тестирование.
- Валидация отвечает на вопрос “Делаем ли мы правильный продукт?”
- Валидация проверяет, соответствует ли программное обеспечение требованиям и ожиданиям клиента.
- Валидация может найти ошибки, которые процесс Verification не может поймать.
- Валидация происходит после Verification.
На практике, отличия верификации и валидации имеют большое значение: заказчика интересует в большей степени валидация (удовлетворение собственных требований); исполнителя, в свою очередь, волнует не только соблюдение всех норм качества (верификация) при реализации продукта, а и соответствие всех особенностей продукта желаниям заказчика.
- Выбери курс для обучения
- Тестирование
- Базовый модуль тестирования
- Тестирование ПО
- Тестирование WEB-сервисов
- Тестирование мобильных приложений
- Тестирование нагрузки с JMeter
- Расширенный модуль автоматизации тестирования
- Автоматизация тестирования с Selenium WebDriver (Python)
- Автоматизация тестирования с Selenium WebDriver (Java)
- Автоматизация тестирования с Selenium WebDriver (C#)
- Автоматизация тестирования на JavaScript
- Java для автоматизаторов
- Fullstack Web Developer
- Java
- Python
- JavaScript
- HTML5 И CSS3
- Полный стек разработки на фреймворке Laravel
- Разработка CMS на основе PHP
- Git для автоматизаторов
- Практический SQL
- Основы Unix и сети
- WEB-серверы и WEB-сервисы
- Создание проекта автоматизации и написания UI тестов
- Составление комбинированных тестов UI и API. Написание BDD тестов
- IT Project Manager
- HR-менеджер в ИТ-компании
- Как правильно составить резюме и пройти собеседование
- Подготовка к сертификации ISTQB Foundation Level на основе Syllabus Version 2018
- Тестирование
- Базовый модуль тестирования
Разница между верификацией и валидацией
Верификация в тестировании ПО – процесс просмотра документации, дизайна, кода и программы для того, чтобы проверить, было ли программное обеспечение создано в соответствии с требованиями или нет. Основная цель процесса верификации – обеспечить качество приложения, дизайна, архитектуры и т.д. Процесс верификации включает в себя такие действия, как ревью, пошаговое руководство и инспекция.
Валидация в разработке ПО – динамический механизм тестирования и проверки того, действительно ли программный продукт соответствует точным потребностям заказчика или нет. Этот процесс помогает гарантировать, что ПО выполняет желаемое использование в подходящей среде. Процесс валидации включает в себя такие действия, как модульное тестирование, интеграционное тестирование, системное тестирование и пользовательское приемочное тестирование.
- Процесс верификации включает в себя проверку документации, дизайна, кода и программы, в то время как процесс валидации включает в себя тестирование и проверку самого продукта.
- Верификация не требует исполнения кода, в то время как валидация требует.
- Верификация использует такие методы, как ревью, пошаговое руководство, инспекцию и отладку, в то время как валидация использует такие методы, как тестирование чёрного ящика, белого ящика и нефункциональное тестирование.
- Верификация проверяет, соответствует ли ПО спецификации, в то время как валидация проверяет, соответствует ли ПО требованиям и ожиданиям.
- Верификация находит баги на раннем этапе цикла разработки, в то время как валидация находит баги, которые верификация не может.
- Сравнивая валидацию и верификацию в тестировании ПО, процесс верификации нацелен на архитектуру ПО, дизайн, базу данных и др., в то время как процесс валидации нацелен на реальный программный продукт.
- Верификация выполняется командой QA, в то время как валидация выполняется командой тестирования с командой QA.
- Сравнивая тестирование верификации и валидации, процесс верификации предшествует процессу валидации, в то время как процесс валидации идет после процесса верификации.
Вот основное различие между тестированием верификации и валидации:
Верификация
Валидация
Процесс верификации включает в себя проверку документов, дизайна, кода и программы
Это динамический механизм тестирования и валидации фактического продукта
Не связано с выполнением кода
Всегда связано с выполнением кода
Верификация использует такие методы, как ревью, пошаговые руководства, инспекции, отладку и т.д.
Используются такие методы, как тестирование черного ящика, тестирование белого ящика и нефункциональное тестирование
Проверяется соответствие программного обеспечения спецификации
Проверяется, соответствует ли программное обеспечение требованиям и ожиданиям заказчика
Обнаруживает баги на ранних стадиях цикла разработки
Может обнаружить баги, которые не может обнаружить верификация
Цель — архитектура приложений и программного обеспечения, спецификация, полный дизайн, высокий уровень, дизайн базы данных и т.д.
Цель — это реальный продукт
Команда контроля качества проводит проверку и убеждается, что программное обеспечение соответствует требованиям и спецификации
Валидация программного кода выполняется с привлечением команды тестирования
Идет перед валидацией
Идет после верификации
Примеры верификации и валидации.
А теперь давайте рассмотрим пример, объясняющий планирование проверки и валидации:
В области разработки ПО рассмотрите следующую спецификацию для теста на верификацию и теста на валидацию:
Кликабельная кнопка с именем Submet
Верификация включала бы проверку документа о дизайне и исправление орфографической ошибки.
В противном случае команда разработчиков создаст подобную кнопку:
Таким образом, теперь новая спецификация:
Кликабельная кнопка с именем Submit (Отправить)
Как только код готов, выполняется валидация. Тест на валидацию обнаружил:
Благодаря тесту на валидацию команда разработчиков сделает кнопку кликабельной.
Верификация и валидация
Термины верификация и валидация связаны с проверкой качества программного обеспечения. Мы используем эти термины в своих статьях и докладах. Неоднократно мы слышали различные комментарии и рассуждения, следует ли относить статический анализ исходного кода программ к верификации и валидации и в чем различие этих понятий. В целом складывается такое впечатление, что каждый вкладывает в эти термины свои понятия, а это приводит к взаимному недопониманию.
Мы решили разобраться с терминологией, чтобы придерживаться наиболее правильного толкования этих понятий. В ходе исследования, мы нашли работу В.В. Кулямина «Методы верификации программного обеспечения» [1]. В ней дается развернутое описание этих терминов, и мы приняли решение в дальнейшем опираться на определения, данные в этой работе. Приведем некоторые выдержки их этой работы, относящиеся к верификации и валидации.
Верификация и валидация являются видами деятельности, направленными на контроль качества программного обеспечения и обнаружение ошибок в нем. Имея общую цель, они отличаются источниками проверяемых в их ходе свойств, правил и ограничений, нарушение которых считается ошибкой.
Для дальнейшего изложения нам необходимо ввести термин «артефакт жизненного цикла ПО». Артефактами жизненного цикла ПО называются различные информационные сущности, документы и модели, создаваемые или используемые в ходе разработки и сопровождения ПО. Так, артефактами являются техническое задание, описание архитектуры, модель предметной области на каком-либо графическом языке, исходный код, пользовательская документация и т.д. Различные модели, используемые отдельными разработчиками при создании и анализе ПО, но не зафиксированные в виде доступных другим людям документов, не могут считаться артефактами.
Верификация проверяет соответствие одних создаваемых в ходе разработки и сопровождения ПО артефактов другим, ранее созданным или используемым в качестве исходных данных, а также соответствие этих артефактов и процессов их разработки правилам и стандартам. В частности, верификация проверяет соответствие между нормами стандартов, описанием требований (техническим заданием) к ПО, проектными решениями, исходным кодом, пользовательской документацией и функционированием самого ПО. Кроме того, проверяется, что требования, проектные решения, документация и код оформлены в соответствии с нормами и стандартами, принятыми в данной стране, отрасли и организации при разработке ПО, а также — что при их создании выполнялись все указанные в стандартах операции, в нужной последовательности. Обнаруживаемые при верификации ошибки и дефекты являются расхождениями или противоречиями между несколькими из перечисленных документов, между документами и реальной работой программы, между нормами стандартов и реальным процессами разработки и сопровождения ПО. При этом принятие решения о том, какой именно документ подлежит исправлению (может быть, и оба) является отдельной задачей.
Валидация проверяет соответствие любых создаваемых или используемых в ходе разработки и сопровождения ПО артефактов нуждам и потребностям пользователей и заказчиков этого ПО, с учетом законов предметной области и ограничений контекста использования ПО. Эти нужды и потребности чаще всего не зафиксированы документально — при фиксации они превращаются в описание требований, один из артефактов процесса разработки ПО. Поэтому валидация является менее формализованной деятельностью, чем верификация. Она всегда проводится с участием представителей заказчиков, пользователей, бизнес-аналитиков или экспертов в предметной области — тех, чье мнение можно считать достаточно хорошим выражением реальных нужд и потребностей пользователей, заказчиков и других заинтересованных лиц. Методы ее выполнения часто используют специфические техники выявления знаний и действительных потребностей участников.
Различие между верификацией и валидацией проиллюстрировано на рисунке 1.
Рисунок 1 — Соотношение верификации и валидации
Приведенные определения получены некоторым расширением определений из стандарта IEEE 1012 на процессы верификации и валидации [2]. В стандартном словаре терминов программной инженерии IEEE 610.12 1990 года [3] определение верификации по смыслу примерно то же, а определение валидации несколько другое — там говорится, что валидация должна проверять соответствие полученного в результате разработки ПО исходным требованиям к нему. В этом случае валидация являлась бы частным случаем верификации, что нигде в литературе по программной инженерии не отмечается, поэтому, а также потому, что оно поправлено в IEEE 1012 2004 года, это определение следует считать неточным. Частое использование фразы B. Boehm’а [4]:
Верификация отвечает на вопрос «Делаем ли мы продукт правильно?», а валидация- на вопрос «Делаем ли мы правильный продукт?»
также добавляет путаницы, поскольку афористичность этого высказывания, к сожалению, сочетается с двусмысленностью. Однако многочисленные труды его автора позволяют считать, что он подразумевал под верификацией и валидацией примерно те же понятия, которые определены выше. Указанные разночтения можно проследить и в содержании стандартов программной инженерии. Так, стандарт ISO 12207 [5] считает тестирование разновидностью валидации, но не верификации, что, по-видимому, является следствием использования неточного определения из стандартного словаря [3].
В заключении хочется заметить, что, согласно приведенным определениям, статический анализ исходного кода программ соответствует верификации программного обеспечения, как проверка соответствия программного кода различным стандартам кодирования. Статический анализ проверяет соответствие результатов этапа конструирования программной системы требованиям и ограничениям, сформулированным ранее.
Библиографический список
- IEEE 1012-2004 Standard for Software Verification and Validation. IEEE, 2005.
- IEEE 610.12-1990 Standard Glossary of Software Engineering Terminology, Corrected Edition. IEEE, February 1991.
- B. W. Boehm. Software Engineering; R&D Trends and Defense Needs. In R. Wegner, ed. Research. Directions in Software Technology. Cambridge, MA:MIT Press, 1979.
- ISO/IEC 12207 Systems and software engineering — Software life cycle processes. Geneva, Switzerland: ISO, 2008.
Валидация и верификация
Безопасная система – и в особенности система, которая используется для обеспечения безопасности – должны быть доверенной. Однако что лежит в основе этого доверия? Что придает уверенность в том, что основные компоненты системы реализованы правильно и не подведут в критический момент? В предыдущей статье, посвященной безопасной ОС, этот вопрос вскользь упоминался, и, как и обещали, мы возвращаемся этой теме.
Верификация и валидация используются для проверки того факта, что система, программа или аппаратное устройство в действительности обладает ожидаемыми свойствами. Эти два понятия (V&V) хоть и схожи по звучанию и постоянно используются вместе, означают существенно разные типы проверок. Напомним на всякий случай:
- Верификация – это процесс оценки того, насколько система (программа, устройство) по итогам некоторого этапа ее разработки соответствует условиям, заданным в начале этапа.
- Валидация – процесс оценки того, насколько система (программа, устройство) соответствует требованиям по ее назначению.
Если говорить еще проще, верификация задается вопросом, строим ли мы систему правильно, а валидация – строим ли мы правильную систему. И если для ответа на второй вопрос существенную играет роль экспертная оценка (от валидации собственно требований к системе до тестирования конечного продукта), то уверенный ответ на первый вопрос способны дать только формальные методы.
Конечно, каждый из этих процессов не дает полной уверенности без другого. Система может быть верифицирована только относительно конкретного критерия, к примеру, относительно гарантии отсутствия ситуации взаимной блокировки при доступе к ресурсам. Тривиальный способ такой верификации возможен при запрете синхронизируемого доступа к общим ресурсам — однако при этом могут быть нарушены свойства целостности ресурсов. Поэтому адекватность условий, согласно которым система верифицируется, тоже должна быть валидирована, а некоторых случаях и сами условия подвергаются верификации, если экспертные требования можно соответствующим образом формализовать.
Когда говорят про верификацию программы, чаще всего представляют некий магический вычислитель, который принимает на вход программный код и по нажатию кнопки – хоп – выдает вердикт: код верен или неверен, безопасен или нет. При малейшем рассмотрении этой идеальной картинки возникает множество вопросов. Первый из них, а что мы, собственно, хотим доказать? На какие вопросы способна дать ответ верификация системы? Корректность, полнота, непротиворечивость, неизбыточность данных, безошибочность и безопасность функционирования… Немного сухих фактов: некоторое время назад было доказано, что все множество свойств системы можно представить как композицию двух базовых:
- Свойство безопасности формулируется как недостижение системой при любом ее исполнении некоторого (небезопасного) состояния. Иными словами, свойство гарантирует, что ничего «плохого» не произойдет (NB: именно в этом значении словосочетание «свойство безопасности» и используется до конца статьи).
- Свойство живости, напротив, гарантирует, что после конечного числа шагов система придет в некоторое определенное состояние – то есть непременно случится что-то «хорошее».
Однако, одно дело – понимание того, что целевое свойство системы может быть представлено как композиция более простых свойств, а другое дело – корректная формализация таких свойств, с учетом того, что они должны не потерять свой действительный смысл, а иначе весь трудоемкий процесс окажется бесполезным. Случается, что требуемые свойства доказываются для ситуаций, когда система фактически не функционирует. Иногда для того, чтобы учитывать только реалистичные ситуации, дополнительно учитывается произвольное свойство справедливости (все как в жизни).
Для формализации описанных таким образом критериев часто используется аппарат классической или темпоральной логики, а для верификации – соответствующие языки. В частности, для классических условий довольно популярен Prolog, для темпоральных – языки Promela, SPIN. Но это далеко не единственный способ. Описание формальных условий поведения компьютерных программ и верификация относительно этих правил настолько специфичная и востребованная проблема, что в 1969 году была создана специальная формальная теория – алгоритмическая логика Хоара, предназначенная для дедуктивного доказательства правильности программ и способная приблизить сухие спецификации к семантике программ на императивных языках. В настоящее время выработан еще более жизненный подход к описанию критериев – в виде контрактных спецификаций программных интерфейсов.
Другая проблема – выбор и формализация объекта верификации. И несмотря на то, что верификация, казалось бы, процедура, состоящая в точном вычислении, при этом выборе нужно ориентироваться на требуемую степень уверенности в результате.
К примеру, для верификации может быть выбрана статическая конфигурация системы – значения системных параметров, информация об установленных приложениях и разрешения политики безопасности. Эти данные подаются на вход решателю, который на основе заранее заданных экспертом логических правил производит вычисления, иногда довольно сложные, и сообщает результат. К примеру, такой решатель может определить, возможен ли в системе некоторый вид атаки, или может ли пользователь получить неавторизованный доступ к каким-либо ресурсам.
Верификация конфигурации способна дать уверенность в том, как будет вести себя система, при условии, что мы доверяем поведению ее компонентов. То есть системные и прикладные программы должны вести себя так, как задано в их спецификациях, не содержать ошибок и уязвимостей, эксплуатация которых могла бы повлиять на фактическое поведение системы. 1
В реальных системах дело чаще всего обстоит не так, а значит, необходимо подвергать верификации собственно программное обеспечение 2 . Здесь снова приходится принимать не одно решение. Что подвергать верификации – высокоуровневый программный или машинный код, принимать ли во внимание влияние программного окружения и как моделировать это окружение, рассматривать ли специфические зависимости выполнения низкоуровневых операций от аппаратной платформы. Выбор снова зависит от цели верификации и от требуемой степени доверия к результатам. Предположим, нужно показать отсутствие уязвимостей определенного вида (этот пример выбран потому, что условие вероятнее всего сводится к свойству безопасности). Тестирование и статический анализ кода путем поиска типовых опасных конструкций в высокоуровневом коде обычно не относят к методам формальной верификации, т.к. как правило они не позволяют добиться полноты анализа 3 . Для решения такой задачи методы верификации производят над конструкциями программного кода логические вычисления, целью которых является доказательство того факта, что на графе передачи управления программы ни один из возможных исполняемых фрагментов (с учетом всех нелинейных переходов) не является уязвимым к указанному способу эксплуатации. Дело за малым – сформировать соответствующий критерий в достаточно общем виде и выполнить эффективное вычисление всем объеме кода программы.
При недостатке доказательств того, что компилятор сохранит доказанные для высокоуровневого представления свойства и для машинного кода, или если нужно гарантировать свойства, сформулированные для машинного кода, работа еще более усложняется. Именно из-за сложности верификации программного кода ее методы применяются к коду как можно более простому и меньшего объема, используемому в ядре безопасности ОС и низкоуровневых компонентах, на которых основано исполнение менее доверенных сервисов и приложений.
Один из перспективных подходов к верификации программ – гарантия безопасности программного кода уже при его создании, или «закладка фундамента» для упрощения будущей верификации. Показав, что используемый язык программирования обладает характеристиками, которые наделяют программный код свойствами безопасности, можно избежать утомительных проверок по крайней мере в отношении этих свойств. Генерация кода позволяет минимизировать человеческий фактор в создании кода (и ошибок в нем). Это довольно эффективно, но применяется – по крайней мере пока – только к реализации ограниченных алгоритмов в конкретно определенном контексте, так как в этом случае не избавляемся от задачи верификации кода, но переносим ее на уровень верификации нотации (языка) и средств генерации программного кода – что является еще более нетривиальной задачей, если код произвольный.
Другой подход к обеспечению верифицируемости кода при его создании – использование парадигмы контрактного программирования. В этом случае перед созданием кода определяются точные формальные (контрактные) спецификации интерфейсов, задающие предусловия (обязательства со стороны клиентов интерфейсов), постусловия (обязательства поставщика) и инварианты (обязательства по выполнению конкретных свойств). Контрактное программирование поддерживается многими языками, в том числе расширениями Java и C.
Верификация программного кода «в лабораторных условиях» может вызывать нарекания в том случае, если поведение кода в большой степени определяется его окружением. Неплохо, конечно, если система построена из слабо связанных компонентов с хорошо документированными интерфейсами – однако в реальных системах достаточно сложно предсказать влияние окружения на поведение отдельно взятого компонента. В этих случаях для оценки корректности системы приходится прибегать к анализу поведения параллельно работающих компонентов. Формальная проверка того, выполняется ли заданная логическая формула на модели системы, описывается в рамках метода, известного как Model checking. Этот метод аккумулирует существующие достижения в верификации систем и широко применяется по всему миру для проверки сложных аппаратных и программных комплексов. За работы, внесшие существенный вклад в его развитие, дважды вручалась премия Тьюринга (первый раз – в 1996 году Амиру Пнуели за «плодотворную работу по внедрению темпоральной логики в вычислительные науки, и за выдающийся вклад в верификацию программ и систем», и второй в 2007 году – ученым Кларку, Эмерсону и Сифакису «за их роль в развитии проверки на модели — высокоэффективную технику верификации программ, широко применяемую при разработке как программного, так и аппаратного обеспечения»). В настоящее время методы model checking применяются и за пределами верификации технических систем, для которых этот метод был изначально разработан.
При вручении премии Тьюринга президент ACM Стьюарт Фельдман сказал и методе Model checking: «Это великий пример того, как технология, изменившая промышленность, родилась из чисто теоретических исследований». Можно с уверенностью утверждать, что если будущее во всех областях жизни от устройств бытового назначения до критических инфраструктур за развитыми, умными и безопасными во всех смыслах технологиями, то методы V&V обеспечивают путь в это будущее.
В одной статье невозможно охватить все вопросы. Для заинтересовавшихся рекомендуем прочитать:
- Статью одного из отцов-основателей метода проверки на модели Эдмунда Кларка (Edmund M. Clarke «The Birth of Model Checking»).
- Глубже погрузиться в формальные основы метода можно при помощи замечательной книги профессора Ю.Г. Карпова «Model Checking».
- Изучить вопросы, связанные с формализацией требований безопасности и живости лучше всего на основе оригинальных работ, обзор которых можно найти в статье Ekkart Kindler «Safety and Liveness Properties: A Survey».
- Монография Ж.Теля «Введение в распределенные алгоритмы» представляет потрясающий по объему и содержанию труд по формальному представлению протоколов в сложных системах и обеспечению их корректной и надежной работы.
1 Это как раз тот случай, когда механизм валидации (на основе знаний об уязвимости ПО) помог бы или отвергнуть меры анализа конфигурации, или ввести компенсационные меры (своевременное обновление потенциально проблемного ПО) с принятием остаточных рисков. >>
2 Заметим, что верификация конфигурации и верификация программного обеспечения — не взаимозаменяемые меры. Если проверка программного кода гарантирует ожидаемое поведение программных компонентов, то проверка конфигурации обеспечивает выполнение политики безопасности при работе этих компонентов. >>
3 Однако они могут служить для валидации программного кода. >>
- Политики безопасности
- Уязвимости и эксплойты
- Тестирование
- Основы