ГОСТ Р МЭК 61508-7—2007
Литература:
Sneak Analysis and Software Sneak Analysis. S. G. Godoy and G. J. Engels. J. Aircraft Vol. 15, No. 8. 1978.
Sneak Circuit Analysis. J. P. Rankin, Nuclear Safety. Vol. 14. No. 5. 1973.
C.5.12 Тестирование на символьном уровне
П р и м е ч а н и е — Ссылка на данный метод/средство приведена в МЭК 61508-3 (таблица В.8).
Цель: показать соответствие между исходным кодом и спецификацией.
Описание: переменные программы оцениваются после замены во всех операторах присваивания левой
его части на правую. Условные ветви и циклы преобразуются в булевские выражения. Окончательный результат
представляет собой символьное выражение для каждой переменной программы. Оно может быть проверено
относительно предполагаемого символьного выражения.
Литература:
Formal Program Verification using Symbolic Execution. R. B. Dannenberg and G. W. Ernst. IEEE Transactions on
Software Engineering. Vol. SE-8. No. 1. 1982.
Symbolic Execution and Software Testing. J. C King. Communications of ACM. Vol. 19. No. 7, 1976.
C.5.13 Формальное доказательство
П р и м е ч а н и е — Ссылка на данный метод/средство приведена в МЭК 61508-3 (таблица В.9).
Цель: подтверждение корректности программ или спецификаций без их исполнения, используя теорети
ческие и математические модели и правила.
Описание: ряд утверждений устанавливается в различных точках программы, и они используются вкачестве
предусловий и постусловий для различных путей программы. Доказательство демонстрирует, что программа
преобразует предусловия в постусловия в соответствии с набором логических правил и завершается.
В настоящем стандарте описаны различные формальные методы, например CCS. CSP. HOL. LOTOS, OBJ,
временная логика. VDM и Z (см. С.2.4).
Альтернативным методу формального доказательства является «строгий аргумент». Подготавливается про
цедура формального доказательства, вкоторой представлены основные этапы, но включены не все математичес
кие подробности. Метод «строгий аргумент» является более слабым методом верификации, устанавливающим,
что доказательство было бы возможным, если бы к этому были предприняты попытки.
Литература:
Software Development — A Rigorous Approach. С. В. Jones. Prentice-Hall, 1980.
Systematic Software Development using VDM. С. B. Jones. Prentice-Hall, 2nd Edition. 1990.
C.5.14 Метрики сложности программного обеспечения
П р и м е ч а н и е — Ссылка на данный метод/средство приведена в МЭК 61508-3 (таблицы А.9 и А.10).
Цель: прогнозирование характеристик программ, исходя из свойств самих программ или их разработки,
либо предысторий тестирования.
Описание: данные методы оценивают некоторые структурные свойства программных средств и их отноше
ния к требуемым характеристикам, например надежность или сложность. Для оценки большинства средств требу
ются программные инструменты. Некоторые применяющиеся метрики перечислены ниже:
- теоретическая сложность графа. Эта метрика может быть применена на раннем этапе жизненного цикла
для оценки компромиссных решений и основана на величине сложности графа управления программы, пред
ставленной ее дипломатическим числом.
- число способов активизации некоторых программных модулей (доступность) - чем больше программных
модулей может быть доступно, тем должна быть большая вероятность их отладки:
- теория метрик Холстеда. При помощи этих средств вычисляют длину программы путем подсчета числа
операторов и операндов: данная метрика дает меру сложности и размеры, которые формируют основу для
сравнений при оценке будущих разрабатываемых ресурсов;
- число входов и выходов на программный модуль. Сведение к минимуму числа точек входов/выходов явля
ется ключевой особенностью методов структурного проектирования и программирования.
Литература:
Software Metrics: A Rigorous and Practical Approach. N. E. Fenton. International Thomson Computer Press.
1996, ISBN 1-85032-275-9. 2nd Edition.
A Complexity Measure. T. J. McCabe. IEEE Trans on Software Engineenng. Vol. SE-2. No. 4. December 1976.
Models and Measurements for Quality Assessments of Software. S. N. Mohanty. ACM Computing Surveys. Vol. 11,
No. 3. September 1979.
Elements of Software Science. M. H. Halstead. Elsevier, North Holland. New York, 1977.
C.5.15 Проверка разработки программ
П р и м е ч а н и е — Ссылка на данный метод/средство приведена в МЭК 61508-3 (таблица В.8).
Цель: обнаружение ошибок на всех этапах разработки программ.
55