АВТОМАТИЗИРОВАННАЯ ПРОВЕРКА СИСТЕМЫ ПРОГРАММНОГО ОБЕСПЕЧЕНИЯ

1. Способ, содержащий этапы, на которых:
создают спецификацию, которая включает в себя свойства комплекта программного обеспечения, содержащего одно или более приложений, один или более драйверов устройств и операционную систему;
проверяют, что свойства комплекта программного обеспечения согласуются со спецификацией; и
предоставляют указание о том, что комплект программного обеспечения прошел проверку на согласованность со спецификацией.
2. Способ по п.1, дополнительно содержащий этап, на котором доказывают, что свойства комплекта программного обеспечения согласуются со спецификацией.
3. Способ по п.2, в котором этап доказывания, что свойства комплекта программного обеспечения согласуются со спецификацией, содержит этапы, на которых:
доказывают функциональную правильность комплекта программного обеспечения; и
доказывают реляционные свойства комплекта программного обеспечения.
4. Способ по любому из пп.1-3, в котором спецификация содержит высокоуровневую спецификацию, которая выражена машиной с конечным числом состояний.
5. Способ по любому из пп.1-3, дополнительно содержащий этапы, на которых:
компилируют код на высокоуровневом языке, реализующий комплект программного обеспечения, в код на языке ассемблера; и
проверяют, что свойства кода на языке ассемблера согласуются со спецификацией.
6. Способ по любому из пп.1-3, дополнительно содержащий этап, на котором преобразовывают спецификацию в низкоуровневую спецификацию перед проверкой того, что свойства комплекта программного обеспечения согласуются со спецификацией.
7. Система, содержащая:
один или более процессоров; и
один или более машиночитаемых носителей информации, хранящих команды, исполняемые одним или более процессорами для выполнения действий, содержащих:
компиляцию варианта реализации на высокоуровневом языке системы программного обеспечения для создания варианта реализации на языке ассемблера, при этом система программного обеспечения включает в себя операционную систему, один или более драйверов и одно или более приложений;
проверку функциональной правильности системы программного обеспечения; и
доказывание реляционных свойств варианта реализации на языке ассемблера.
8. Система по п.7, в которой проверка функциональной правильности системы программного обеспечения включает в себя проверку свойств информационного потока системы программного обеспечения.
9. Система по п.7, в которой действия дополнительно содержат сертификацию через подтверждение того, что:
открытый ключ соответствует секретному ключу; и
секретный ключ известен только системе программного обеспечения.
10. Система по п.7, в которой действия дополнительно содержат проверку правильности системы программного обеспечения посредством проверки каждого компонента системы программного обеспечения.
11. Система по п.7, в которой действия дополнительно содержат проверку, что первый компонент системы программного обеспечения неспособен к вмешательству во вторую спецификацию второго компонента системы программного обеспечения.
12. Система по любому из пп.7-11, в которой действия дополнительно содержат демонстрацию удаленной эквивалентности системы программного обеспечения.
13. Система по любому из пп.7-11, в которой:
высокоуровневая спецификация соответствует варианту реализации на высокоуровневом языке системы программного обеспечения; и
высокоуровневая спецификация выражена по меньшей мере одной машиной с конечным числом состояний.
14. Система по любому из пп.7-11, дополнительно содержащая определение того, что вариант реализации на языке ассемблера реализует функционально правильную версию низкоуровневой спецификации.
15. Система по любому из пп.7-11, дополнительно содержащая:
создание варианта реализации на машинном коде на основе варианта реализации на языке ассемблера; и
исполнение варианта реализации на машинном коде на доверенной платформе аппаратного обеспечения.