C.4.4 Инструментальные средства, заслуживающие доверие на основании опыта использования
Примечание - Ссылка на данный метод/средство приведена в МЭК 61508-3 (таблица А.3).
Цель: исключение любых проблем, обусловленных ошибками транслятора, которые могут появиться во время разработки, верификации и эксплуатации программного пакета.
Описание: транслятор используется в тех случаях, когда не очевидно неправильное исполнение многих предыдущих проектов. Если отсутствует опыт эксплуатации трансляторов или в них обнаружены любые известные серьезные ошибки, то от таких трансляторов следует отказаться, если только нет каких-либо других гарантий корректной работы транслятора (см. С.4.4.1).
Если в трансляторе выявлены небольшие недостатки, то соответствующие языковые конструкции фиксируются и в проектах, связанных с безопасностью, не применяются.
Другим вариантом исключения проблем, обусловленных ошибками транслятора, является ограничение языка до его общеиспользуемых конструкций.
Настоящие рекомендации основаны на опыте построения многих проектов. Доказано, что недоработанные трансляторы служат серьезным препятствием в любой программной разработке. Такие трансляторы в общем случае делают невозможным разработку программного обеспечения, связанного с безопасностью.
В настоящее время не существует методов подтверждения корректности всего транслятора или отдельных его частей.
С.4.4.1 Сравнение исходных программ и исполнимых кодов
Цель: убедиться в том, что инструменты, используемые для создания образа PROM, не вносят в него никаких ошибок.
Описание: образ PROM обратно преобразуется в совокупность «объектных» модулей. Эти «объектные» модули обратно преобразуются в скомпонованные файлы языка, которые затем с помощью подходящих методов сравниваются с фактическими исходными файлами, используемыми первоначально для разработки PROM.
Основное преимущество данного метода состоит в том, что инструменты [компиляторы, редакторы связей (компоновщики) и т.п.], используемые для разработки образа PROM, не требуют подтверждения соответствия. Этим методом проверяют правильность преобразования исходного файла, используемого для конкретной системы, связанной с безопасностью.
Литература:
Demonstrating Equivalence of Source Code and PROM Contents. D.J. Pavey and L.A. Winsborrow. The Computer Journal Vol. 36, No. 7, 1993.
Formal demonstration of equivalence of source code and PROM contents: an industrial example. D.J. Pavey and L.A. Winsborrow. Mathematics of Dependable Systems, Ed.С Mitchell and V. Stavridou, Clarendon Press, 1995, ISBN 0-198534-91-4.
Retrospective Formal Verification of Reactor Protection System Software. D.J. Pavey, L.A. Winsborrow, A.R. Lawrence. Proceedings of the Second Safety Through Quality Conference, 1995, ISBN 1-897851-06-5.
Assuring Correctness in a Safety Critical Software Application. L.A. Winsborrow and D.J. Pavey. High Integrity Systems, Vol. 1, No. 5, pp 453-459, 1996.
C.4.5 Библиотека проверенных/верифицированных модулей и компонентов
Примечание - Ссылка на данный метод/средство приведена в МЭК 61508-3 (таблица А.3).
Цель: исключение необходимости чрезмерных повторных проверок или перепроектирования компонентов программного обеспечения и аппаратных средств при каждом новом применении. Кроме того, содействие созданию проектов, которые не были формально или строго проверены, но относительно которых имеется значительная предыстория эксплуатации.
Описание: хорошо спроектированные и структурированные PES строятся из множества компонентов и модулей аппаратных и программных средств, которые четко различаются и которые взаимодействуют друг с другом строго специфицированным способом.
Различные PES, созданные для различных применений, могут содержать большое число одинаковых или очень схожих между собой программных модулей или компонентов. Создание библиотеки таких общеприменимых программных модулей позволяет использовать большую часть ресурсов, необходимых для подтверждения соответствия проекта, сразу для нескольких применений.
Кроме того, использование подобных программных модулей для многих применений дает практическое подтверждение их успешной эксплуатации. Это практическое подтверждение увеличивает доверие пользователей к программным модулям.
Один из подходов, в соответствии с которым программному модулю можно доверять при его практическом использовании, описан в С.2.10.
Литература:
Software Reuse and Reverse Engineering in Practice. P.A.V. Hall (ed.), Chapman & Hall, 1992, ISBN 0-412-39980-6.
DIN V VDE 0801 A1: Grundsätze für Rechner in Systemen mit Sicherheitsaufgaben (Principles for Computers in Safety-Related Systems). Änderung 1 zu DIN V VDE 0801/01.90. Beuth-Verlag, Berlin, 1994.
C.4.6 Выбор соответствующего языка программирования
Примечание - Ссылка на данный метод/средство приведена в МЭК 61508-3 (таблица А.3).
Цель: обеспечение в максимальной степени требований настоящего стандарта для специального защищающего программирования, строгой типизации, структурного программирования и, возможно, суждений. Выбранный язык программирования должен обеспечить легко верифицируемый код и простые процедуры разработки, верификации и эксплуатации программ.
Описание: язык программирования должен быть полностью и однозначно определен. Язык должен быть ориентирован на пользователя или проблему, а не на процессор или платформу. Широко используемые языки программирования или их подмножества должны быть предпочтительнее языков специального применения [4], [11].
Языки программирования также должны обеспечивать:
- блоковую структуру организации программ;
- проверку времени трансляции;
- печать времени прогона и проверку ограничения массива.
Язык программирования должен включать в себя:
- использование небольших и управляемых программных модулей;
- ограничение доступа к данным в конкретных программных модулях;
- определение поддиапазонов переменных;
- любые другие типы конструкции, ограничивающие ошибки.
Если операции по безопасности системы зависят от ограничений реального времени, то язык программирования должен обеспечивать также обработку исключительных состояний или прерываний.
Желательно, чтобы язык программирования обеспечивался соответствующим транслятором, подходящими библиотеками с заранее созданными программными модулями, отладчиком и инструментами как для управления, так и для разработки.
В настоящее время еще не ясно, будут ли объектно-ориентированные языки программирования предпочтительнее других общепринятых языков.
К свойствам, которые усложняют верификацию и поэтому должны быть исключены, относятся:
- безусловные переходы (за исключением вызовов подпрограмм);
- рекурсии;
- указатели, динамически распределяемые области памяти или любые типы динамических переменных или объектов;
- обработка прерываний на уровне исходного кода;
- множество входов или выходов в циклах, блоках или подпрограммах;
- инициализация или декларация неявных переменных;
- вариантные записи и эквивалентность;
- параметры процедуры.
Языки программирования низкого уровня, в частности ассемблеры, обладают недостатками, связанными с их жесткой ориентацией на процессор машины или на определенную платформу.
Желательным свойством языка программирования является то, что его проектирование и использование должно приводить к созданию программ, выполнение которых предсказуемо. Если используется подходящий конкретный язык программирования, то в нем должно существовать подмножество, которое гарантирует, что выполнение программы предсказуемо. Это подмножество не может быть (в общем случае) статически определено, несмотря на то, что многие статические ограничения помогают гарантировать предсказуемое выполнение. Обычно это может потребовать демонстрации того, что индексы массива находятся в установленных пределах и что числовое переполнение не может возникнуть, и т.п.
Рекомендации по конкретным языкам программирования [21], [23], [25] - [28], [30] - [32] приведены в таблице С.1.
Литература:
Dependability of Critical Computer Systems 1. F.J. Redmill, Elsevier Applied Science, 1988, ISBN 1-85166-203-0.
Таблица С.1 - Рекомендации по конкретным языкам программирования
|
Язык программирования |
SIL1 |
SIL2 |
SIL3 |
SIL4 |
|
1 ADA |
HR |
HR |
R |
R |
|
2 ADA с подмножеством |
HR |
HR |
HR |
HR |
|
3 MODULA-2 |
HR |
HR |
R |
R |
|
4 MODULA- с подмножеством |
HR |
HR |
HR |
HR |
|
5 PASCAL |
HR |
HR |
R |
R |
|
6 PASCAL с подмножеством |
HR |
HR |
HR |
HR |
|
7 FORTRAN 77 |
R |
R |
R |
R |
|
8 FORTRAN 77 с подмножеством |
HR |
HR |
HR |
HR |
|
9 С |
R |
- |
NR |
NR |
|
10 Язык С с подмножеством и стандартом кодирования, а также использование инструментов статического анализа |
HR |
HR |
HR |
HR |
|
11 PL/M |
R |
- |
NR |
NR |
|
12 PL/M с подмножеством и стандартом кодирования |
HR |
R |
R |
R |
|
13 Ассемблер |
R |
R |
- |
- |
|
14 Ассемблер с подмножеством и стандартом кодирования |
R |
R |
R |
R |
|
15 Многоступенчатые диаграммы |
R |
R |
R |
R |
|
16 Многоступенчатая диаграмма с определенным подмножеством языка |
HR |
HR |
HR |
HR |
|
17 Диаграмма функциональных блоков |
R |
R |
R |
R |
|
18 Диаграмма функциональных блоков с определенным подмножеством языка |
HR |
HR |
HR |
HR |
|
19 Структурированный текст |
R |
R |
R |
R |
|
20 Структурированный текст с определенным подмножеством языка |
HR |
HR |
HR |
HR |
|
21 Последовательная функциональная диаграмма |
R |
R |
R |
R |
|
22 Последовательная функциональная диаграмма с определенным подмножеством языка |
HR |
HR |
HR |
HR |
|
23 Список команд |
R |
- |
NR |
NR |
|
24 Список команд с определенным подмножеством языка |
HR |
R |
R |
R |
|
Примечания 1 Пояснения к рекомендациям R, HR см. в МЭК 31508-3 (приложение А) 2 Системное программное обеспечение включает в себя операционную систему, драйверы, встроенные функции и программные модули, являющиеся частью системы. Программные средства обычно обеспечиваются системой безопасности при поставке. Подмножество языка следует выбирать очень внимательно с тем, чтобы исключить сложные структуры, которые могут образоваться в результате ошибок реализации. Следует проводить проверки для того, чтобы убедиться в правильном использовании подмножества языка программирования. 3 Прикладная программа представляет собой программу, разработанную для конкретного безопасного применения. Во многих случаях такая программа разрабатывается конечным пользователем либо подрядчиком, ориентированным на разработку прикладных программ. В тех случаях, когда ряд языков программирования поддерживают одни и те же рекомендации, разработчику следует выбрать тот, который повсеместно используется персоналом в конкретной промышленности или отрасли. Подмножество языка программирования следует выбирать с особым вниманием, чтобы исключить сложные структуры, которые могут привести к ошибкам реализации. 4 Если конкретный язык программирования не представлен в настоящей таблице, то это не означает, что он исключен. Этот конкретный язык программирования должен соответствовать требованиям настоящего стандарта. 5 О пунктах 15-24 см. МЭК 61131-3. |
||||
С.5 Верификация и модификация
С.5.1 Вероятностное тестирование
Примечание - Ссылка на данный метод/средство приведена в МЭК 61508-3 (таблицы А.5, А.7 и А.9).
Цель: получение количественных показателей надежности исследуемой программы. Описание: количественные показатели могут быть получены с учетом относительных уровней доверия и значимости и должны иметь следующий вид:
- вероятность ошибки при запросе;
- вероятность ошибки в течение определенного периода времени;
- вероятность последствий ошибки.
Из этих показателей могут быть: получены другие показатели, например:
- вероятность безошибочной работы;
- вероятность живучести;
- доступность;
- MTBF или частота отказов;
- вероятность безопасного исполнения.
Вероятностные соображения основываются либо на статистических испытаниях, либо на опыте эксплуатации. Обычно число тестовых примеров или наблюдаемых практических примеров очень велико. Обычно тестирование в режиме запросов занимает значительно меньше времени, чем в непрерывном режиме работы.
Для формирования входных данных тестирования и управления выходными данными тестирования обычно используются инструменты автоматического тестирования. Крупные тесты прогоняются на больших центральных компьютерах с имитацией соответствующей периферии. Тестируемые данные выбираются с учетом как систематических, так и случайных ошибок аппаратных средств. Например, общее управление тестированием гарантирует профиль тестируемых данных, тогда как случайный выбор тестируемых данных может управлять отдельными тестовыми примерами более детально.
