Методика доказательства безопасности программного обеспечения микропроцессрных систем железнодорожной автоматики

Abstract

Предложена методика доказательства безопасности программного обеспечения микропроцессорных систем железнодорожной автоматики и телемеханики с помощью формальных методов, в которой рассматриваются валидация и верификация программного обеспечения в неразрывной связи с аппаратными средствами анализируемых систем. Она базируется на опыте доказательства безопасности железнодорожных устройств и на мировой теории и практике работы с критически важными объектами информатизации. Методика позволяет проводить анализ на функциональную, информационную и кибернетическую безопасность произвольных железнодорожных аппаратно-программных комплексов с объемом программного обеспечения до 10 KLOC.