ГОСТ Р МЭК 61508-7—2012
Использование формальной верификации на стадии проектирования может значительно уменьшить время
разработки, обнаруживая существенные ошибки и упущения на ранних стадиях проектирования, и таким образом
сократить время, необходимое на итерации между проектированием и тестированием.
Ряд формальных методов, применяющихся на практике, описаны в С.2.4: например. CCS. CSP. HOL. LOTOS.
OBJ. временная логика. VDM и 2.
С.5.12.1 Проверка модели
Проверка модели — метод для формальной верификации реактивных и конкурентных систем. Задавая ко
нечное состояние структуры, которая описывает поведение системы, проверяется свойство, записанное в виде
формулы во временной логике, удовлетворяет оно или нет структуре. Для автоматического и исчерпывающего
прохода всех состояний структуры используются эффективные алгоритмы (например SPIN. SMV и UPPAAL). Если
свойство не удовлетворяется, то генерируется контрпример. Эта процедура показывает, как свойства нарушаются в
структуре, и содержит очень полезную информацию для исследования системы. Метод проверки модели может
обнаружить «глубокие ошибки», которые могут быть не обнаружены при обычном контроле и тестировании.
Необходимо отметить, что метод проверки модели полезен при анализе нюансов сложной структуры. Это
может быть полезно для некоторых приложений с низким УПБ. но необходимо быть очень внимательным, если
нюансы сложной структуры существуют в приложениях с высоким УПБ.
Литература:
Is Proof More Cost-Effective Than Testing? S. King. R. Chapman, J. Hammond. A. Pryor. IEEE Transactions on
Software Engineering, vol. 26. No. 8. August 2000.
Model Checking. E.M. Clarke. O. Grumberg. and D.A. Peled. MIT Press. 1999. ISBN 0262032708.9780262032704.
Systems and Software Verification: Model-Checking Techniques and Tools. B. Berard. M. Bidoit. A. Finkei,
F. Laroussinie. A. Petit L. Petrucci. Ph. Schnoebelen. and P. Mckenzie, Springer. 2001, ISBN 3-540-41523-8.
Logic in Computer Science: Modelling and Reasoning about Systems. M. Huth and M. Ryan. Cambridge University
Press. 2000. ISBN 0521652006. 0521656028.
The Spin Model Checker: Primer and Reference Manual. G.J. Holzmann.Addison-Wesley. 2003. ISBN 0321228626.
9780321228628.
C.5.12.2 (He используется.)
C.5.13 Метрики сложности программного обеспечения
П р и м е ч а н и е — Ссылка на данный метод/средсгво приведена в МЭК 61508-3 (таблицы А.9 и С.19).
Цель. Прогнозирование характеристик программ исходя из свойств самих программ или их разработки, либо
предысторий тестирования.
Описание. Данные методы оценивают некоторые структурные свойства программных средств и их отноше
ния к требуемым характеристикам, например, надежность или сложность. Для оценки большинства средств требу
ются программные инструменты. Некоторые применяющиеся метрики перечислены ниже:
- теоретическая сложность графа. Эта метрика может быть применена на раннем этапе жизненного цикла
для оценки компромиссных решений и основана на величине сложности графа управления программы, представ
ленной ее цикломагическим числом;
- число способов активизации некоторых программных модулей (доступность) — чем больше программных
модулей может быть доступно, тем должна быть большая вероятность их отладки;
- теория метрик Холстеда. При помощи этих средств вычисляют длину программы путем подсчета коли
чества операторов и операндов: данная метрика дает меру сложности и размеры, которые формируют основу для
сравнений при оценке будущих разрабатываемых ресурсов:
- число входов и выходов на программный модуль. Сведение к минимуму числа точек входов/выходов явля
ется ключевой особенностью методов структурного проектирования и программирования.
Литература:
Metrics and Models in Software Quality Engineering. S.H. Kan. Addison-Wesley, 2003. ISBN 0201729156,
9780201729153.
C.5.14 Формальные проверки
П р и м е ч а н и е — Ссылка на данный метод/средство приведена в МЭК 61508-3 (таблица В.8).
Цель. Обнаружение ошибок в элементе программного обеспечения.
Описание. Формальный контроль — структурированный процесс проверки материалов о программном обе
спечении. который выполняется коллегами разработчика этого материала в целях найти ошибки и помочь раз
работчику улучшить материал. Разработчик не должен принимать участие в процессе контроля, кроме информи
рования проверяющих на этапе их ознакомления с материалами. Формальные проверки могут быть выполнены
для конкретных элементов программного обеспечения, созданных на любой стадии жизненного цикла разработки
программного обеспечения.
Проверяющие должны ознакомиться с проверяемыми материалами до выполнения проверки. Роли прове
ряющих в процессе проверки должны быть ясно определены. Должна быть подготовлена программа проверки.
Должны быть определены входные и выходные критерии, основанные на требуемых характеристиках элемента
программного обеспечения. Входные критерии — это такие критерии или требования, которые должны быть удов
летворены до выполнения проверки. Выходные критерии — это такие критерии или требования, которые должны
быть удовлетворены, чтобы считать процесс проверки завершенным успешно.
62