The 16 references with 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
Butler R.W. «What is Formal Methods?» NASA LaRC Formal Methods Program, 2001.
Total in-text references: 1
  1. In-text reference with the coordinate start=2292
    Prefix
    Одним из возможных способов поиска ошибок и повышения качества ПО в рамках применяемого комплекса подходов является доказательство корректности, которое относится к формальным методам (Formal Methods)
    Exact
    [1]
    Suffix
    и успешно используется для верификации микропроцессорных устройств на Белорусской железной дороге [2, 3, 4]. Для систем, связанных с безопасностью, стандарт IEC 61508 имеет градацию уровней полноты безопасности от SIL-1 до SIL-4, а железнодорожные системы должны соответствовать наиболее строгому уровню SIL-4, который настоятельно рекомендует применение формальных методов для критически важных

2
Сивко Б.В. Доказательство корректности блока телеуправления 16-1 диспетчерской централизации «Нёман» // Вестник БелГУТа: Наука и Транспорт. – 2012. – No1(24). – С.18–21.
Total in-text references: 2
  1. In-text reference with the coordinate start=2395
    Prefix
    Одним из возможных способов поиска ошибок и повышения качества ПО в рамках применяемого комплекса подходов является доказательство корректности, которое относится к формальным методам (Formal Methods) [1] и успешно используется для верификации микропроцессорных устройств на Белорусской железной дороге
    Exact
    [2, 3, 4]
    Suffix
    . Для систем, связанных с безопасностью, стандарт IEC 61508 имеет градацию уровней полноты безопасности от SIL-1 до SIL-4, а железнодорожные системы должны соответствовать наиболее строгому уровню SIL-4, который настоятельно рекомендует применение формальных методов для критически важных систем информатизации [5].

  2. In-text reference with the coordinate start=16987
    Prefix
    , если система подготовлена к тому, чтобы быть верифицируемой, когда задачи определения функции безопасности решаются до этапов разработки и проектирования, что возможно только для разрабатываемых и проектируемых АПК [4, 6]. Описываемое определение выбора функции безопасности было опробовано на верификации ПО устройств связи с напольными объектами СЖАТ, такими как блоки телеуправления 16-1
    Exact
    [2]
    Suffix
    , светооптические светодиодные системы [3] и многопроцессорные блоки ТУ-8Б и ТС-16Б микропроцессорной централизации «Ипуть» [6]. Таким образом, разработанные общие принципы построения функций безопасности позволяют улучшить формализацию спецификаций доказательства безопасности ПО сложных АПК критически важных систем информатизации, а задача доказательства безопасности упрощается, если в процесс

3
Харлап С.Н., Сивко Б.В. Верификация программного обеспечения микропроцессорной светооптической светодиодной системы // Вестник БелГУТа: Наука и Транспорт. – 2012. – No1 (24). – С.22–25.
Total in-text references: 2
  1. In-text reference with the coordinate start=2395
    Prefix
    Одним из возможных способов поиска ошибок и повышения качества ПО в рамках применяемого комплекса подходов является доказательство корректности, которое относится к формальным методам (Formal Methods) [1] и успешно используется для верификации микропроцессорных устройств на Белорусской железной дороге
    Exact
    [2, 3, 4]
    Suffix
    . Для систем, связанных с безопасностью, стандарт IEC 61508 имеет градацию уровней полноты безопасности от SIL-1 до SIL-4, а железнодорожные системы должны соответствовать наиболее строгому уровню SIL-4, который настоятельно рекомендует применение формальных методов для критически важных систем информатизации [5].

  2. In-text reference with the coordinate start=17029
    Prefix
    Описываемое определение выбора функции безопасности было опробовано на верификации ПО устройств связи с напольными объектами СЖАТ, такими как блоки телеуправления 16-1 [2], светооптические светодиодные системы
    Exact
    [3]
    Suffix
    и многопроцессорные блоки ТУ-8Б и ТС-16Б микропроцессорной централизации «Ипуть» [6]. Таким образом, разработанные общие принципы построения функций безопасности позволяют улучшить формализацию спецификаций доказательства безопасности ПО сложных АПК критически важных систем информатизации, а задача доказательства безопасности упрощается, если в процессе разработки используются методы построения

4
Сивко Б.В. Проектирование безопасного программного обеспечения микропроцессорных устройств автоматики и телемеханики // Проблемы безопасности на трансп.: тезисы докл. VI Междунар. науч. – практ. конф., Гомель, 29–30 ноября 2012 г. / М-во образования Респ. Беларусь, М-во трансп. и коммуникаций Респ. Беларусь, Бел. ж. д., Белорус. гос. ун-т трансп.: редкол.: В.И.Сенько (отв. ред.) [и др.]. – Гомель, 2012. – С.205.
Total in-text references: 3
  1. In-text reference with the coordinate start=2395
    Prefix
    Одним из возможных способов поиска ошибок и повышения качества ПО в рамках применяемого комплекса подходов является доказательство корректности, которое относится к формальным методам (Formal Methods) [1] и успешно используется для верификации микропроцессорных устройств на Белорусской железной дороге
    Exact
    [2, 3, 4]
    Suffix
    . Для систем, связанных с безопасностью, стандарт IEC 61508 имеет градацию уровней полноты безопасности от SIL-1 до SIL-4, а железнодорожные системы должны соответствовать наиболее строгому уровню SIL-4, который настоятельно рекомендует применение формальных методов для критически важных систем информатизации [5].

  2. In-text reference with the coordinate start=3123
    Prefix
    Формальные методы в качестве доказательства корректности могут быть применены как для готового ПО, так и на ранних этапах разработки всего АПК, но в любом случае одним из первых шагов верификации является определение функции безопасности, подлежащей проверке на корректность
    Exact
    [4, 6]
    Suffix
    . Функция безопасности представляет собой формализованное условие по отношению к верифицируемой системе, выполнение которого позволяет сделать заключение о безопасности функционирования СЖАТ. Для одного и того же АПК функция безопасности может быть определена по-разному, а выбор доказываемого условия может происходить на разных этапах жизненного цикла системы.

  3. In-text reference with the coordinate start=16811
    Prefix
    Практика показывает, что избежать компромисса удается только в случае, если система подготовлена к тому, чтобы быть верифицируемой, когда задачи определения функции безопасности решаются до этапов разработки и проектирования, что возможно только для разрабатываемых и проектируемых АПК
    Exact
    [4, 6]
    Suffix
    . Описываемое определение выбора функции безопасности было опробовано на верификации ПО устройств связи с напольными объектами СЖАТ, такими как блоки телеуправления 16-1 [2], светооптические светодиодные системы [3] и многопроцессорные блоки ТУ-8Б и ТС-16Б микропроцессорной централизации «Ипуть» [6].

5
David Smith J. «Safety Critical Systems Handbook. A Straightforward Guide to Functional Safety, IEC 61508 and Related Standards, Including Process IEC 61511 and Machinery IEC 62061 and ISO 13849» / David J. Smith and Kenneth G. L. Simpson // Elsevier Ltd., 2010.
Total in-text references: 1
  1. In-text reference with the coordinate start=2843
    Prefix
    Для систем, связанных с безопасностью, стандарт IEC 61508 имеет градацию уровней полноты безопасности от SIL-1 до SIL-4, а железнодорожные системы должны соответствовать наиболее строгому уровню SIL-4, который настоятельно рекомендует применение формальных методов для критически важных систем информатизации
    Exact
    [5]
    Suffix
    . Формальные методы в качестве доказательства корректности могут быть применены как для готового ПО, так и на ранних этапах разработки всего АПК, но в любом случае одним из первых шагов верификации является определение функции безопасности, подлежащей проверке на корректность [4, 6].

6
Сивко Б.В. Доказательство корректности программного обеспечения многопроцессорных устройств связи с объектами железнодорожной автоматики и телемеханики // Вестник БелГУТа: Наука и Транспорт. – 2012. – No2(25). – С.27-30.
Total in-text references: 3
  1. In-text reference with the coordinate start=3123
    Prefix
    Формальные методы в качестве доказательства корректности могут быть применены как для готового ПО, так и на ранних этапах разработки всего АПК, но в любом случае одним из первых шагов верификации является определение функции безопасности, подлежащей проверке на корректность
    Exact
    [4, 6]
    Suffix
    . Функция безопасности представляет собой формализованное условие по отношению к верифицируемой системе, выполнение которого позволяет сделать заключение о безопасности функционирования СЖАТ. Для одного и того же АПК функция безопасности может быть определена по-разному, а выбор доказываемого условия может происходить на разных этапах жизненного цикла системы.

  2. In-text reference with the coordinate start=16811
    Prefix
    Практика показывает, что избежать компромисса удается только в случае, если система подготовлена к тому, чтобы быть верифицируемой, когда задачи определения функции безопасности решаются до этапов разработки и проектирования, что возможно только для разрабатываемых и проектируемых АПК
    Exact
    [4, 6]
    Suffix
    . Описываемое определение выбора функции безопасности было опробовано на верификации ПО устройств связи с напольными объектами СЖАТ, такими как блоки телеуправления 16-1 [2], светооптические светодиодные системы [3] и многопроцессорные блоки ТУ-8Б и ТС-16Б микропроцессорной централизации «Ипуть» [6].

  3. In-text reference with the coordinate start=17115
    Prefix
    Описываемое определение выбора функции безопасности было опробовано на верификации ПО устройств связи с напольными объектами СЖАТ, такими как блоки телеуправления 16-1 [2], светооптические светодиодные системы [3] и многопроцессорные блоки ТУ-8Б и ТС-16Б микропроцессорной централизации «Ипуть»
    Exact
    [6]
    Suffix
    . Таким образом, разработанные общие принципы построения функций безопасности позволяют улучшить формализацию спецификаций доказательства безопасности ПО сложных АПК критически важных систем информатизации, а задача доказательства безопасности упрощается, если в процессе разработки используются методы построения контролепригодного ПО.

7
Fagan M.E. Design and code inspections to reduce errors in program development, IBM Systems Journal, Volume 15 Issue 3, September 1976, p. 182–211.
Total in-text references: 1
  1. In-text reference with the coordinate start=3685
    Prefix
    Для одного и того же АПК функция безопасности может быть определена по-разному, а выбор доказываемого условия может происходить на разных этапах жизненного цикла системы. Разработка и эксплуатация ПО, а также ряд исследований говорят о том, что чем позже обнаруживается ошибка, тем сложнее как выявить её, так и исправить, и тем больше проблем она может принести
    Exact
    [7, 8]
    Suffix
    . При этом исправление ошибок, допущенных при формулировании требований к системе, обходится в десятки раз дороже ошибок, допущенных во время реализации [9, 10]. Определение функции безопасности, которое относится к формализации решаемой задачи, является спецификацией по отношению к доказательству корректности и обладает теми же свойствами, что и постановка требований при разработке ПО.

8
Boehm B.W. Software engineering. IEEE Transactions on Computers 25:1226–1241, 1976.
Total in-text references: 1
  1. In-text reference with the coordinate start=3685
    Prefix
    Для одного и того же АПК функция безопасности может быть определена по-разному, а выбор доказываемого условия может происходить на разных этапах жизненного цикла системы. Разработка и эксплуатация ПО, а также ряд исследований говорят о том, что чем позже обнаруживается ошибка, тем сложнее как выявить её, так и исправить, и тем больше проблем она может принести
    Exact
    [7, 8]
    Suffix
    . При этом исправление ошибок, допущенных при формулировании требований к системе, обходится в десятки раз дороже ошибок, допущенных во время реализации [9, 10]. Определение функции безопасности, которое относится к формализации решаемой задачи, является спецификацией по отношению к доказательству корректности и обладает теми же свойствами, что и постановка требований при разработке ПО.

9
Telles M., Hsieh Y., Telles M.A. The Science of Debugging // The Coriolis Group, 2001.
Total in-text references: 1
  1. In-text reference with the coordinate start=3844
    Prefix
    Разработка и эксплуатация ПО, а также ряд исследований говорят о том, что чем позже обнаруживается ошибка, тем сложнее как выявить её, так и исправить, и тем больше проблем она может принести [7, 8]. При этом исправление ошибок, допущенных при формулировании требований к системе, обходится в десятки раз дороже ошибок, допущенных во время реализации
    Exact
    [9, 10]
    Suffix
    . Определение функции безопасности, которое относится к формализации решаемой задачи, является спецификацией по отношению к доказательству корректности и обладает теми же свойствами, что и постановка требований при разработке ПО.

10
Boehm B.W., Papaccio P.N. Understanding and controlling software costs // IEEE Trans Softw Eng 14(10):1462–1477, October 1988.
Total in-text references: 1
  1. In-text reference with the coordinate start=3844
    Prefix
    Разработка и эксплуатация ПО, а также ряд исследований говорят о том, что чем позже обнаруживается ошибка, тем сложнее как выявить её, так и исправить, и тем больше проблем она может принести [7, 8]. При этом исправление ошибок, допущенных при формулировании требований к системе, обходится в десятки раз дороже ошибок, допущенных во время реализации
    Exact
    [9, 10]
    Suffix
    . Определение функции безопасности, которое относится к формализации решаемой задачи, является спецификацией по отношению к доказательству корректности и обладает теми же свойствами, что и постановка требований при разработке ПО.

11
Nancy G. Leveson, Software safety in embedded computer systems. Communications of the ACM, 34(2):34–46, February 1991.
Total in-text references: 3
  1. In-text reference with the coordinate start=4723
    Prefix
    Последовательность этапов анализа на безопасность Условия для определения функции безопасности устанавливаются на этапе валидации на основании характеристик применяемых компонентов, множества используемых методов, стратегий обеспечения безопасности и практического опыта в рассматриваемой предметной области
    Exact
    [11]
    Suffix
    . Данный процесс независим от последующей верификации – он определяет подлежащие проверке 103 свойства и формирует исходные данные, на основании которых задается функция безопасности, используемая в доказательстве корректности.

  2. In-text reference with the coordinate start=5897
    Prefix
    Мировой опыт эксплуатации критически важных систем информатизации говорит о том, что аварии и катастрофы происходят из-за множества факторов, при этом значительная часть происшествий происходит (в том числе) из-за ошибок, допущенных при формулировке требований к системе
    Exact
    [11, 12, 13]
    Suffix
    . Например, имеется большое количество причин, из-за которых морской корабль может быть подвержен риску: столкновение с айсбергом, коррозия, взрыв груза и др. Инженерам не обязательно знать все источники рисков, но при этом во время проектирования могут быть приняты формализованные решения для минимизации опасности: корабль должен оставаться на плаву при заданном пределе количества пробоин, не

  3. In-text reference with the coordinate start=6628
    Prefix
    Пароход “Титаник” был спроектирован так, чтобы оставаться на плаву в случае затопления 4 или менее первых отсеков, что можно назвать функцией безопасности. К сожалению, столкновение с айсбергом привело к затоплению 5 первых отсеков
    Exact
    [11]
    Suffix
    . Функция безопасности была задана исходя из практического опыта и знаний того времени, и после её определения проектирование системы проводилось уже на её основании. Но, как показывает история, такой подход не означает, что все возможные опасности устранены.

12
Charles Perrow. Normal Accidents: Living with High Risk Technologies. Basic Books, New York, NY, 1984.
Total in-text references: 1
  1. In-text reference with the coordinate start=5897
    Prefix
    Мировой опыт эксплуатации критически важных систем информатизации говорит о том, что аварии и катастрофы происходят из-за множества факторов, при этом значительная часть происшествий происходит (в том числе) из-за ошибок, допущенных при формулировке требований к системе
    Exact
    [11, 12, 13]
    Suffix
    . Например, имеется большое количество причин, из-за которых морской корабль может быть подвержен риску: столкновение с айсбергом, коррозия, взрыв груза и др. Инженерам не обязательно знать все источники рисков, но при этом во время проектирования могут быть приняты формализованные решения для минимизации опасности: корабль должен оставаться на плаву при заданном пределе количества пробоин, не

13
Ivars Peterson, Fatal Defect: Chasing Killer Computer Bugs, Times Books, New York, 1995.
Total in-text references: 1
  1. In-text reference with the coordinate start=5897
    Prefix
    Мировой опыт эксплуатации критически важных систем информатизации говорит о том, что аварии и катастрофы происходят из-за множества факторов, при этом значительная часть происшествий происходит (в том числе) из-за ошибок, допущенных при формулировке требований к системе
    Exact
    [11, 12, 13]
    Suffix
    . Например, имеется большое количество причин, из-за которых морской корабль может быть подвержен риску: столкновение с айсбергом, коррозия, взрыв груза и др. Инженерам не обязательно знать все источники рисков, но при этом во время проектирования могут быть приняты формализованные решения для минимизации опасности: корабль должен оставаться на плаву при заданном пределе количества пробоин, не

14
Nancy G. Leveson. Safeware: System Safety and Computers. Addison-Wesley, 1995.
Total in-text references: 1
  1. In-text reference with the coordinate start=7237
    Prefix
    При проектировании систем могут приниматься неявные допущения, которые напрямую не связаны с безопасностью функционирования, но могут повлиять на работу всего АПК. Например, допущение того, что траектории самолётов всегда будут выше уровня моря, может привести к ошибкам ПО во время полета над территориями ниже уровня моря и отказу всей системы
    Exact
    [14]
    Suffix
    . Условия безопасности работы системы могут отличаться при изменении окружения или условий функционирования, что актуально для СЖАТ, и в частности это в значительной степени проявляется при переходе с релейной базы на микроэлектронную.

15
Gerhart S.L., Yelowitz L., Observations of Fallibility in Applications of Modern Programming Methodologies // IEEE Trans. Software Eng., vol. 2, no. 3, 1976, pp. 195–207.
Total in-text references: 1
  1. In-text reference with the coordinate start=8544
    Prefix
    Таким образом, одной из проблем валидации является определение условий, подлежащих проверке, а особенности данного процесса таковы, что после формализации нет однозначного критерия и уверенности в том, что утвержденная доказываемая функция является необходимой и достаточной
    Exact
    [15]
    Suffix
    . Во время последующей разработки или анализа на безопасность может быть выяснено, что заданные рамки слишком строги и доказательство корректности провести невозможно, или напротив, слишком слабы, из-за чего уменьшается вероятность нахождения ошибок в ПО.

16
Сапожников В.В., Кравцов Ю.А., Сапожников Вл.В. Дискретные устройства железнодорожной автоматики и телемеханики // М. Транспорт, 1988.
Total in-text references: 1
  1. In-text reference with the coordinate start=10419
    Prefix
    о том, что определение доказываемой функции безопасности разрабатываемых и существующих АПК необходимо проводить на основании: – используемой стратегии обеспечения безопасности – например, во время проектирования может быть использована стратегия применения логических элементов с несимметричными отказами (h1-надежные элементы) и система должна придерживаться её во время всего жизненного цикла
    Exact
    [16]
    Suffix
    ; 105 – требований безопасности ко всей системе – например, верифицируемый компонент должен выдерживать заданные временные диапазоны сигналов взаимодействия c другими компонентами системы; – требований безопасности к рассматриваемому АПК – например, система обязана сохранять инвариант и переходить в безопасное состояние в случае внутренних сбоев.