Аннотация:
Предложен подход на основе аксиоматических базисов, позволяющий формализовать решение ряда проблем разработки и верификации отказоустойчивых и безопасных систем. Сформулированы положения и задачи аксиоматико-базисного подхода. Показано, что подход согласуется с опытом инженерии безопасных и отказоустойчивых систем; позволяет повышать их отказоустойчивость и безопасность; сравнивать отказоустойчивость систем; сохранять баланс между отказоустойчивостью и сложностью разработки и верификации; применять формальные методы для доказательства; формализовать интеграцию систем; повышать и оценивать уровень диверситета без привлечения независимых групп разработчиков и экспертов; формализованно проектировать и верифицировать системы, обнаруживающие собственные отказы. Вместе с тем подход позволяет решать актуальные проблемы отказоустойчивых и безопасных систем, такие как формализация методов внутрипроцессорного контроля и разработка условий его проведения, а также доказательство достаточности диверситета разрабатываемых и верифицируемых систем. Предложен подход на основе аксиоматических базисов, позволяющий формализовать решение ряда проблем разработки и верификации отказоустойчивых и безопасных систем. Сформулированы положения и задачи аксиоматико-базисного подхода. Показано, что подход согласуется с опытом инженерии безопасных и отказоустойчивых систем; позволяет повышать их отказоустойчивость и безопасность; сравнивать отказоустойчивость систем; сохранять баланс между отказоустойчивостью и сложностью разработки и верификации; применять формальные методы для доказательства; формализовать интеграцию систем; повышать и оценивать уровень диверситета без привлечения независимых групп разработчиков и экспертов; формализованно проектировать и верифицировать системы, обнаруживающие собственные отказы. Вместе с тем подход позволяет решать актуальные проблемы отказоустойчивых и безопасных систем, такие как формализация методов внутрипроцессорного контроля и разработка условий его проведения, а также доказательство достаточности диверситета разрабатываемых и верифицируемых систем.