Формальные методы и критические системы

В организациях, занимающихся разработкой критических систем, все еще продолжаются дебаты о роли формальных методов в процессе разработки систем с критическими требованиями к безопасности и надежности. Использование формальной математической спецификации и связанной с ней верификации является стандартом в Великобритании для систем, критических по обеспечению безопасности [241]. Однако большинство разработчиков критических систем считают формальные методы неэффективными и уверены, что их использование может привести даже к снижению (а не повышению) надежности системы. Формальные методы применяются на двух уровнях разработки критических систем.

1. Разработка формальной спецификации системы и математический анализ противоречий в формальной спецификации. Как отмечалось в главе 9, данная методика эффективно выявляет ошибки и упущения в системной спецификации. В этой главе использование формального подхода рассматривается на примере спецификации части системы, отвечающей за инъекции инсулина, которая описана в главе 16.

2. Формальная верификация для проверки соответствия программного кода системной спецификации. Для формальной верификации нужна формальная спецификация. Формальная верификация эффективно выявляет ошибки, сделанные на этапах программирования и проектирования системы.

Аргумент за использование формальной спецификации и связанной с ней верификации программ состоит в том, что во время формального специфицирования выполняется тщательный и подробный анализ требований. Этот анализ позволяет выявить потенциальные противоречия и упущения, которые в противном случае могут оказаться незамеченными вплоть до появления рабочей версии системы. Формальная верификация демонстрирует соответствие разрабатываемой программы спецификации.

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

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

Иногда говорят, что использование формальных методов в процессе разработки системы позволяет создать более надежные и безотказные системы. Несомненно, формальная спецификация содержит меньше противоречий, которые должен разрешать разработчик. Однако формальная спецификация и доказательство не гарантируют, что система окажется надежной на практике, чему есть несколько причин.

1. Спецификация может не отражать реальных требований пользователей системы. Установлено, что многие ошибки являются следствием ошибок и упущений в системной спецификации, не обнаруженных при создании формальной спецификации [226]. Кроме того, пользователям часто непонятны формальные нотации, поэтому они не могут непосредственно проанализировать формальную спецификацию и обнаружить в ней ошибки и упущения.

2. В доказательствах могут быть ошибки. Доказательства больших и сложных программ, как правило, также большие и сложные, поэтому часто содержат ошибки.

3. При доказательстве применяется неверный шаблон использования. Если система используется неверно, то доказательство также может быть неверным.

Несмотря на все эти недостатки, я полагаю, что формальные методы играют важную роль в разработке надежного и безопасного ПО. Формальные спецификации весьма эффективно выявляют проблемы требований, которые являются наиболее распространенными ошибками. Формальная верификация повышает уровень надежности наиболее критических компонентов этих систем. Формальные методы получают все большее распространение, поскольку постоянно растет спрос на надежные системы и увеличивается число специалистов, знакомых с этими методами. Но должно пройти еще немало времени, чтобы использование формальных методов в процессе разработки критических систем стало обычным делом.