The 16 reference contexts in paper K. Bochkov A., B. Sivko V., К. Бочков А., Б. Сивко В. (2016) “ВЫБОР И ОПРЕДЕЛЕНИЕ ФУНКЦИИ БЕЗОПАСНОСТИ ПРИ ВЕРИФИКАЦИИ МИКРОПРОЦЕССОРНЫХ СИСТЕМ ЖЕЛЕЗНОДОРОЖНОЙ АВТОМАТИКИ И ТЕЛЕМЕХАНИКИ // SELECTION AND DEFINITION OF SAFETY FUNCTION WHEN VERIFYING RAILWAY SIGNALLING AND REMOTE CONTROL COMPUTER-BASED SYSTEMS” / spz:neicon:sustain:y:2014:i:2:p:101-115

  1. Start
    2292
    Prefix
    Одним из возможных способов поиска ошибок и повышения качества ПО в рамках применяемого комплекса подходов является доказательство корректности, которое относится к формальным методам (Formal Methods)
    Exact
    [1]
    Suffix
    и успешно используется для верификации микропроцессорных устройств на Белорусской железной дороге [2, 3, 4]. Для систем, связанных с безопасностью, стандарт IEC 61508 имеет градацию уровней полноты безопасности от SIL-1 до SIL-4, а железнодорожные системы должны соответствовать наиболее строгому уровню SIL-4, который настоятельно рекомендует применение формальных методов для критически важных
    (check this in PDF content)

  2. Start
    2395
    Prefix
    Одним из возможных способов поиска ошибок и повышения качества ПО в рамках применяемого комплекса подходов является доказательство корректности, которое относится к формальным методам (Formal Methods) [1] и успешно используется для верификации микропроцессорных устройств на Белорусской железной дороге
    Exact
    [2, 3, 4]
    Suffix
    . Для систем, связанных с безопасностью, стандарт IEC 61508 имеет градацию уровней полноты безопасности от SIL-1 до SIL-4, а железнодорожные системы должны соответствовать наиболее строгому уровню SIL-4, который настоятельно рекомендует применение формальных методов для критически важных систем информатизации [5].
    (check this in PDF content)

  3. Start
    2843
    Prefix
    Для систем, связанных с безопасностью, стандарт IEC 61508 имеет градацию уровней полноты безопасности от SIL-1 до SIL-4, а железнодорожные системы должны соответствовать наиболее строгому уровню SIL-4, который настоятельно рекомендует применение формальных методов для критически важных систем информатизации
    Exact
    [5]
    Suffix
    . Формальные методы в качестве доказательства корректности могут быть применены как для готового ПО, так и на ранних этапах разработки всего АПК, но в любом случае одним из первых шагов верификации является определение функции безопасности, подлежащей проверке на корректность [4, 6].
    (check this in PDF content)

  4. Start
    3123
    Prefix
    Формальные методы в качестве доказательства корректности могут быть применены как для готового ПО, так и на ранних этапах разработки всего АПК, но в любом случае одним из первых шагов верификации является определение функции безопасности, подлежащей проверке на корректность
    Exact
    [4, 6]
    Suffix
    . Функция безопасности представляет собой формализованное условие по отношению к верифицируемой системе, выполнение которого позволяет сделать заключение о безопасности функционирования СЖАТ. Для одного и того же АПК функция безопасности может быть определена по-разному, а выбор доказываемого условия может происходить на разных этапах жизненного цикла системы.
    (check this in PDF content)

  5. Start
    3685
    Prefix
    Для одного и того же АПК функция безопасности может быть определена по-разному, а выбор доказываемого условия может происходить на разных этапах жизненного цикла системы. Разработка и эксплуатация ПО, а также ряд исследований говорят о том, что чем позже обнаруживается ошибка, тем сложнее как выявить её, так и исправить, и тем больше проблем она может принести
    Exact
    [7, 8]
    Suffix
    . При этом исправление ошибок, допущенных при формулировании требований к системе, обходится в десятки раз дороже ошибок, допущенных во время реализации [9, 10]. Определение функции безопасности, которое относится к формализации решаемой задачи, является спецификацией по отношению к доказательству корректности и обладает теми же свойствами, что и постановка требований при разработке ПО.
    (check this in PDF content)

  6. Start
    3844
    Prefix
    Разработка и эксплуатация ПО, а также ряд исследований говорят о том, что чем позже обнаруживается ошибка, тем сложнее как выявить её, так и исправить, и тем больше проблем она может принести [7, 8]. При этом исправление ошибок, допущенных при формулировании требований к системе, обходится в десятки раз дороже ошибок, допущенных во время реализации
    Exact
    [9, 10]
    Suffix
    . Определение функции безопасности, которое относится к формализации решаемой задачи, является спецификацией по отношению к доказательству корректности и обладает теми же свойствами, что и постановка требований при разработке ПО.
    (check this in PDF content)

  7. Start
    4723
    Prefix
    Последовательность этапов анализа на безопасность Условия для определения функции безопасности устанавливаются на этапе валидации на основании характеристик применяемых компонентов, множества используемых методов, стратегий обеспечения безопасности и практического опыта в рассматриваемой предметной области
    Exact
    [11]
    Suffix
    . Данный процесс независим от последующей верификации – он определяет подлежащие проверке 103 свойства и формирует исходные данные, на основании которых задается функция безопасности, используемая в доказательстве корректности.
    (check this in PDF content)

  8. Start
    5897
    Prefix
    Мировой опыт эксплуатации критически важных систем информатизации говорит о том, что аварии и катастрофы происходят из-за множества факторов, при этом значительная часть происшествий происходит (в том числе) из-за ошибок, допущенных при формулировке требований к системе
    Exact
    [11, 12, 13]
    Suffix
    . Например, имеется большое количество причин, из-за которых морской корабль может быть подвержен риску: столкновение с айсбергом, коррозия, взрыв груза и др. Инженерам не обязательно знать все источники рисков, но при этом во время проектирования могут быть приняты формализованные решения для минимизации опасности: корабль должен оставаться на плаву при заданном пределе количества пробоин, не
    (check this in PDF content)

  9. Start
    6628
    Prefix
    Пароход “Титаник” был спроектирован так, чтобы оставаться на плаву в случае затопления 4 или менее первых отсеков, что можно назвать функцией безопасности. К сожалению, столкновение с айсбергом привело к затоплению 5 первых отсеков
    Exact
    [11]
    Suffix
    . Функция безопасности была задана исходя из практического опыта и знаний того времени, и после её определения проектирование системы проводилось уже на её основании. Но, как показывает история, такой подход не означает, что все возможные опасности устранены.
    (check this in PDF content)

  10. Start
    7237
    Prefix
    При проектировании систем могут приниматься неявные допущения, которые напрямую не связаны с безопасностью функционирования, но могут повлиять на работу всего АПК. Например, допущение того, что траектории самолётов всегда будут выше уровня моря, может привести к ошибкам ПО во время полета над территориями ниже уровня моря и отказу всей системы
    Exact
    [14]
    Suffix
    . Условия безопасности работы системы могут отличаться при изменении окружения или условий функционирования, что актуально для СЖАТ, и в частности это в значительной степени проявляется при переходе с релейной базы на микроэлектронную.
    (check this in PDF content)

  11. Start
    8544
    Prefix
    Таким образом, одной из проблем валидации является определение условий, подлежащих проверке, а особенности данного процесса таковы, что после формализации нет однозначного критерия и уверенности в том, что утвержденная доказываемая функция является необходимой и достаточной
    Exact
    [15]
    Suffix
    . Во время последующей разработки или анализа на безопасность может быть выяснено, что заданные рамки слишком строги и доказательство корректности провести невозможно, или напротив, слишком слабы, из-за чего уменьшается вероятность нахождения ошибок в ПО.
    (check this in PDF content)

  12. Start
    10419
    Prefix
    о том, что определение доказываемой функции безопасности разрабатываемых и существующих АПК необходимо проводить на основании: – используемой стратегии обеспечения безопасности – например, во время проектирования может быть использована стратегия применения логических элементов с несимметричными отказами (h1-надежные элементы) и система должна придерживаться её во время всего жизненного цикла
    Exact
    [16]
    Suffix
    ; 105 – требований безопасности ко всей системе – например, верифицируемый компонент должен выдерживать заданные временные диапазоны сигналов взаимодействия c другими компонентами системы; – требований безопасности к рассматриваемому АПК – например, система обязана сохранять инвариант и переходить в безопасное состояние в случае внутренних сбоев.
    (check this in PDF content)

  13. Start
    16811
    Prefix
    Практика показывает, что избежать компромисса удается только в случае, если система подготовлена к тому, чтобы быть верифицируемой, когда задачи определения функции безопасности решаются до этапов разработки и проектирования, что возможно только для разрабатываемых и проектируемых АПК
    Exact
    [4, 6]
    Suffix
    . Описываемое определение выбора функции безопасности было опробовано на верификации ПО устройств связи с напольными объектами СЖАТ, такими как блоки телеуправления 16-1 [2], светооптические светодиодные системы [3] и многопроцессорные блоки ТУ-8Б и ТС-16Б микропроцессорной централизации «Ипуть» [6].
    (check this in PDF content)

  14. Start
    16987
    Prefix
    , если система подготовлена к тому, чтобы быть верифицируемой, когда задачи определения функции безопасности решаются до этапов разработки и проектирования, что возможно только для разрабатываемых и проектируемых АПК [4, 6]. Описываемое определение выбора функции безопасности было опробовано на верификации ПО устройств связи с напольными объектами СЖАТ, такими как блоки телеуправления 16-1
    Exact
    [2]
    Suffix
    , светооптические светодиодные системы [3] и многопроцессорные блоки ТУ-8Б и ТС-16Б микропроцессорной централизации «Ипуть» [6]. Таким образом, разработанные общие принципы построения функций безопасности позволяют улучшить формализацию спецификаций доказательства безопасности ПО сложных АПК критически важных систем информатизации, а задача доказательства безопасности упрощается, если в процесс
    (check this in PDF content)

  15. Start
    17029
    Prefix
    Описываемое определение выбора функции безопасности было опробовано на верификации ПО устройств связи с напольными объектами СЖАТ, такими как блоки телеуправления 16-1 [2], светооптические светодиодные системы
    Exact
    [3]
    Suffix
    и многопроцессорные блоки ТУ-8Б и ТС-16Б микропроцессорной централизации «Ипуть» [6]. Таким образом, разработанные общие принципы построения функций безопасности позволяют улучшить формализацию спецификаций доказательства безопасности ПО сложных АПК критически важных систем информатизации, а задача доказательства безопасности упрощается, если в процессе разработки используются методы построения
    (check this in PDF content)

  16. Start
    17115
    Prefix
    Описываемое определение выбора функции безопасности было опробовано на верификации ПО устройств связи с напольными объектами СЖАТ, такими как блоки телеуправления 16-1 [2], светооптические светодиодные системы [3] и многопроцессорные блоки ТУ-8Б и ТС-16Б микропроцессорной централизации «Ипуть»
    Exact
    [6]
    Suffix
    . Таким образом, разработанные общие принципы построения функций безопасности позволяют улучшить формализацию спецификаций доказательства безопасности ПО сложных АПК критически важных систем информатизации, а задача доказательства безопасности упрощается, если в процессе разработки используются методы построения контролепригодного ПО.
    (check this in PDF content)