ГОСТ Р МЭК 61508-7—2012
Описание. Анализ потока данных представляет собой метод статического тестирования, объединяющий ин
формацию. полученную из анализа потока управления, с информацией о том. какие переменные считываются
или записываются в различных частях кода. Данный метод гложет проверять:
- переменные, которые могут быть считаны до присвоения им значений. Такую ситуацию можно исключить,
если всегда присваивать значение при объявлении новой переменной:
- переменные, записанные несколько раз. но не считанные. Такая ситуация может указывать на пропущен
ный код;
- переменные, которые записаны, но никогда не считываются. Такая ситуация может указывать избьлочный код.
Аномальный потокданных не всегда непосредственно соответствует программным ошибкам, но если анома
лии исключены, то маловероятно, что код будет содержать ошибки.
Литература:
Software engineering: Update. Ian Sommerville. Addison-Wesley Longman. Amsterdam: 8m ed.. 2006. ISBN
0321313798. 9780321313799.
Software Engineering. Ian Sommerville. Pearson Studium. 8. Auflage, 2007. ISBN 3827372577. 9783827372574.
C.5.11 Тестирование на символьном уровне
П р и м е ч а н и е — Ссыпка на данный метод/средство приведена в МЭК 61508-3 (таблица В.8).
Цель. Показать соответствие между исходным кодом и спецификацией.
Описание. Переменные программы оцениваются после замены во всех операторах присваивания левой его
части на правую. Условные ветви и циклы преобразуются в булевские выражения. Окончательный результат пред
ставляет собой символьное выражение для каждой переменной программы. Это выражение является формулой
для значения, которое программа вычислила бы. если задать реальные данные. Оно может быть проверено от
носительно предполагаемого выражения.
Такое использование символьного выполнения является систематическим способом генерирации тестовыхдан
ных для ветвей логики программы. Символьное средство выполнения гложет быть включено в интегрированный ком
плекс инструментальных средств для выполнения тестирования и анализа кода элемента программного обеспечения.
Литература:
Using symbolic execution for verifying safety-critical systems. A. Coen-Porisini. G. Denaro, C. Ghezzi, M. Pezze.
Proceedings of the 8th European software engineering conference, and 9th ACM SIGSOFT international symposium on
Foundations of software engineering. ACM. 2001. ISBN:1-58113-390-1.
Using symbolic execution to guide test generation. G. Lee. J. Morris, K. Parker. G. Bundell. P.Lam. In Software
Testing, Verification and Reliability, vot. 15. No. 1.2005. John Wiley & Sons. Ltd.
C.5.12 Формальное доказательство (верификация)
П р и м е ч а н и е — Ссылка на данный метод/средство приведена в МЭК 61508-3 (таблицы А.5 и А.9).
Цель. Доказать правильность программы относительно некоторой абстрактной модели программы, исполь
зуя теоретические и математические модели и правила.
Описание. Тестирование — распространенный способ исследовать правильность программы. Однако ис
черпывающее тестирование обычно недостижимо ввиду сложности программ, имеющих практическое значение,
поэтому таким способом может быть исследована только часть возможного поведения программы. Напротив, фор
мальная верификация применяет математические операции к математическому представлению программы, чтобы
установить, что программа ведет себя, как определено для всех возможных входных данных.
Для формальной верификации системы требуется абстрактная модель программы и ее заданное поведение
(то есть спецификация), представленные на формальном языке. Спецификация может быть полной или она может
быть ограничена определенными свойствами программы:
- свойствами функциональной корректности, то есть программа должна продемонстрировать определенную
функциональность;
- свойствами безопасности (то есть неправильное поведение никогда не будет происходить), и живучести
(то есть в конечном счете будет вести себя правильно);
- синхронизирующими свойствами, то есть события, реализующие поведение, произойдут в определен
ное время.
Результатом формальной верификации является строгий вывод о том, что абстрактная модель программы
корректна относительно спецификации для всех возможных входных данных, то есть модель удовлетворяет за
данным свойствам.
Однако правильность модели непосредственно не доказывает правильность фактической программы, по
этому далее необходим шаг, который должен показать, что модель — точная абстракция фактической программы
для моделируемых свойств. Некоторые свойства программы, представляющие практический интерес, не могут
быть формально описаны (например большинство проблем синхронизации и планирования или субъективные
свойства, такие как «ясный и простой» пользовательский интерфейс, или. на самом деле, любое свойство или цель
проекта, которые не могут быть легко представлены на формальном языке). Поэтому формальная верификация не
полностью заменяет моделирование и тестирование, но зато она дополняет эти методы, обеспечивая их дока
зательством корректности работы программы для всех входных данных. Формальная верификация может гаран
тировать корректность абстрактной модели программы, а тестирование гарантирует, что фактическая программа
ведет себя, как ожидалось.
61