Формальные методы в разработке программного обеспечения

Введение

Спецификации математических программ

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

Предыстория

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

Легкие формальные методы

Некоторые практики полагают, что сообщество формальных методов чрезмерно акцентирует внимание на полной формализации спецификации или проекта. Они утверждают, что выразительность используемых языков, а также сложность моделируемых систем делают полную формализацию трудной и дорогостоящей задачей. В качестве альтернативы были предложены различные облегченные формальные методы, которые делают упор на частичную спецификацию и целенаправленное применение. Примеры такого облегченного подхода к формальным методам включают нотацию объектного моделирования Alloy, синтез Денни некоторых аспектов нотации Z с разработкой, управляемой вариантами использования, и инструменты CSK VDM.

Применение

Формальные методы могут применяться на различных этапах процесса разработки.

Спецификация

Формальные методы могут использоваться для описания разрабатываемой системы на любом необходимом уровне детализации. Это формальное описание может служить руководством для дальнейшей разработки (см. следующие разделы); кроме того, оно может быть использовано для проверки полноты и точности спецификации требований к разрабатываемой системе, или для формализации этих требований путем выражения их на формальном языке с чётко и однозначно определённым синтаксисом и семантикой. Необходимость в формальных системах спецификаций отмечалась на протяжении многих лет. В отчёте ALGOL 58 Джон Бэкус представил формальную нотацию для описания синтаксиса языка программирования, впоследствии названную нормальной формой Бэкуса, а затем переименованную в форму Бэкуса — Наура (BNF). Бэкус также отметил, что формальное описание смысла синтаксически корректных программ ALGOL не было завершено к моменту публикации отчёта. «Поэтому формальное рассмотрение семантики допустимых программ будет представлено в последующей статье». Однако эта статья так и не была опубликована.

Разработка

Формальная разработка — это использование формальных методов как неотъемлемой части процесса разработки системы, поддерживаемого инструментами. После создания формальной спецификации она может служить руководством при разработке конкретной системы в процессе проектирования (то есть реализации, как правило, в программном обеспечении, но также и в аппаратном обеспечении). Например:

Если формальная спецификация представлена в операционной семантике, наблюдаемое поведение конкретной системы можно сравнить с поведением спецификации (которая сама должна быть исполняемой или моделируемой). Кроме того, операционные команды спецификации могут быть непосредственно преобразованы в исполняемый код. Если формальная спецификация основана на аксиоматической семантике, предусловия и постусловия спецификации могут быть использованы в качестве утверждений в исполняемом коде.

Проверка

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

Проверка отпуска

Подтверждение с использованием подписи — это применение формального инструмента верификации, заслуживающего высокой степени доверия. Такой инструмент может заменить традиционные методы верификации (сам инструмент может быть даже сертифицирован).

Человекоуправляемое доказательство

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

Автоматическое доказательство

Напротив, растет интерес к созданию доказательств корректности таких систем автоматизированными средствами. Автоматизированные методы делятся на три основные категории: автоматическое доказательство теорем, при котором система пытается построить формальное доказательство с нуля, опираясь на описание системы, набор логических аксиом и набор правил вывода. Проверка моделей, при которой система проверяет определенные свойства путем исчерпывающего поиска всех возможных состояний, в которые система может перейти в процессе выполнения. Абстрактная интерпретация, при которой система проверяет верхнюю аппроксимацию поведенческого свойства программы, используя вычисление неподвижной точки над (возможно, полной) решеткой, представляющей это свойство. Некоторые автоматические доказывающие теоремы требуют указания на то, какие свойства достаточно "интересны" для исследования, в то время как другие работают без вмешательства человека. Проверочные системы (model checkers) могут быстро "застрять" в проверке миллионов неинтересных состояний, если им не предоставлена достаточно абстрактная модель. Сторонники таких систем утверждают, что результаты обладают большей математической строгостью, чем доказательства, полученные человеком, поскольку все утомительные детали были алгоритмически проверены. Обучение, необходимое для использования таких систем, также меньше, чем для создания качественных математических доказательств вручную, что делает эти методы доступными для более широкого круга специалистов. Критики отмечают, что некоторые из этих систем похожи на оракулов: они выдают вердикт об истинности, но не предоставляют объяснения этой истинности. Существует также проблема "проверки верификатора"; если программа, помогающая в верификации, сама не является доказанной, есть основания сомневаться в надежности полученных результатов. Некоторые современные инструменты проверки моделей создают "журнал доказательств", подробно описывающий каждый шаг их доказательства, что позволяет, при наличии соответствующих инструментов, проводить независимую верификацию. Главная особенность подхода абстрактной интерпретации заключается в том, что он обеспечивает надежный анализ, то есть не возвращает ложных отрицательных результатов. Кроме того, он эффективно масштабируется за счет настройки абстрактной области, представляющей анализируемое свойство, и применения операторов расширения для достижения быстрой сходимости.

In contrast, there is increasing interest in producing proofs of correctness of such systems by automated means. Automated techniques fall into three general categories:
Automated theorem proving, in which a system attempts to produce a formal proof from scratch, given a description of the system, a set of logical axioms, and a set of inference rules. Model checking, in which a system verifies certain properties by means of an exhaustive search of all possible states that a system could enter during its execution. Abstract interpretation, in which a system verifies an over approximation of a behavioural property of the program, using a fixpoint computation over a (possibly complete) lattice representing it. Some automated theorem provers require guidance as to which properties are "interesting" enough to pursue, while others work without human intervention. Model checkers can quickly get bogged down in checking millions of uninteresting states if not given a sufficiently abstract model. Proponents of such systems argue that the results have greater mathematical certainty than human produced proofs, since all the tedious details have been algorithmically verified. The training required to use such systems is also less than that required to produce good mathematical proofs by hand, making the techniques accessible to a wider variety of practitioners. Critics note that some of those systems are like oracles: they make a pronouncement of truth, yet give no explanation of that truth. There is also the problem of "verifying the verifier"; if the program that aids in the verification is itself unproven, there may be reason to doubt the soundness of the produced results. Some modern model checking tools produce a "proof log" detailing each step in their proof, making it possible to perform, given suitable tools, independent verification. The main feature of the abstract interpretation approach is that it provides a sound analysis, i. e. no false negatives are returned. Moreover, it is efficiently scalable, by tuning the abstract domain representing the property to be analyzed, and by applying widening operators to get fast convergence.

Приложения

Формальные методы применяются в различных областях аппаратного и программного обеспечения, включая маршрутизаторы, коммутаторы Ethernet, протоколы маршрутизации, приложения безопасности и микроядра операционных систем, такие как seL4. Есть несколько примеров их использования для верификации функциональности аппаратного и программного обеспечения, применяемого в центрах обработки данных. IBM использовала ACL2, систему доказательства теорем, в процессе разработки процессоров AMD x86. Intel применяет подобные методы для верификации своего оборудования и прошивки (постоянного программного обеспечения, записанного в постоянную память). Dansk Datamatik Center использовал формальные методы в 1980-х годах для разработки компиляторной системы для языка программирования Ada, которая впоследствии стала коммерчески успешным продуктом с длительным сроком службы. Существует ряд других проектов NASA, в которых применяются формальные методы, например, система воздушного транспорта нового поколения, интеграция систем беспилотных летательных аппаратов в национальное воздушное пространство и система координированного разрешения и обнаружения конфликтов в воздухе (ACCoRD). Метод B с Atelier B используется для разработки систем автоматической безопасности для различных метрополитенов, установленных по всему миру компаниями Alstom и Siemens, а также для сертификации по стандарту Common Criteria и разработки системных моделей компаниями ATMEL и STMicroelectronics. Формальная верификация широко используется в аппаратном обеспечении большинством известных производителей, таких как IBM, Intel и AMD. Intel применяет формальные методы для верификации работы своих продуктов во многих областях аппаратного обеспечения, включая параметрическую верификацию протокола когерентности кэша, валидацию исполнительного устройства процессора Intel Core i7 (с использованием доказательства теорем, BDD и символической оценки), оптимизацию для архитектуры Intel IA 64 с использованием системы доказательства теорем HOL light и верификацию высокопроизводительного двухпортового гигабитного контроллера Ethernet с поддержкой протокола PCI Express и технологии Intel Advanced Management Technology с использованием Cadence. Аналогично, IBM использовала формальные методы для верификации силовых затворов, регистров и функциональной верификации микропроцессора IBM Power7.

Formal methods are applied in different areas of hardware and software, including routers, Ethernet switches, routing protocols, security applications, and operating system microkernels such as seL4. There are several examples in which they have been used to verify the functionality of the hardware and software used in data centres. IBM used ACL2, a theorem prover, in the AMD x86 processor development process. Intel uses such methods to verify its hardware and firmware (permanent software programmed into a read only memory). Dansk Datamatik Center used formal methods in the 1980s to develop a compiler system for the Ada programming language that went on to become a long lived commercial product. There are several other projects of NASA in which formal methods are applied, such as Next Generation Air Transportation System, Unmanned Aircraft System integration in National Airspace System, and Airborne Coordinated Conflict Resolution and Detection (ACCoRD). B Method with Atelier B, is used to develop safety automatisms for the various subways installed throughout the world by Alstom and Siemens, and also for Common Criteria certification and the development of system models by ATMEL and STMicroelectronics. Formal verification has been frequently used in hardware by most of the well known hardware vendors, such as IBM, Intel, and AMD. There are many areas of hardware, where Intel have used formal methods to verify the working of the products, such as parameterized verification of cache coherent protocol, Intel Core i7 processor execution engine validation (using theorem proving, BDDs, and symbolic evaluation), optimization for Intel IA 64 architecture using HOL light theorem prover, and verification of high performance dual port gigabit Ethernet controller with support for PCI express protocol and Intel advance management technology using Cadence. Similarly, IBM has used formal methods in the verification of power gates, registers, and functional verification of the IBM Power7 microprocessor.

В разработке программного обеспечения

В разработке программного обеспечения формальные методы — это математические подходы к решению программных (и аппаратных) проблем на уровнях требований, спецификаций и проектирования. Формальные методы наиболее часто применяются к критически важному для безопасности или критически важному для надёжности программному обеспечению и системам, таким как программное обеспечение для авиационной техники. Стандарты обеспечения безопасности программного обеспечения, такие как DO 178C, допускают использование формальных методов в качестве дополнения, а Common Criteria предписывает их использование на высших уровнях категоризации. Для последовательного программного обеспечения примерами формальных методов являются метод B, языки спецификаций, используемые в автоматическом доказательстве теорем, RAISE и нотация Z. В функциональном программировании тестирование на основе свойств позволило математически задать и проверить (хотя и не обязательно исчерпывающе) ожидаемое поведение отдельных функций. Язык ограничений объектов (и его специализации, такие как Java Modeling Language) позволяет формально специфицировать объектно-ориентированные системы, хотя и не обязательно формально верифицировать их. Для параллельного программного обеспечения и систем сети Петри, алгебра процессов и конечные автоматы (основанные на теории автоматов; см. также виртуальный конечный автомат или автомат, управляемый событиями) позволяют создавать исполняемые спецификации программного обеспечения и могут использоваться для построения и проверки поведения приложений. Другой подход к формальным методам в разработке программного обеспечения — это написание спецификации на некоторой форме логики, обычно варианте логики первого порядка, и последующее непосредственное выполнение этой логики как программы. Язык OWL, основанный на дескриптивной логике, является примером такого подхода. Ведутся также работы по автоматическому отображению английского (или другого естественного языка) в логику и обратно, а также по непосредственному выполнению логики. Примерами являются Attempto Controlled English и Internet Business Logic, которые не стремятся контролировать словарный запас или синтаксис. Особенностью систем, поддерживающих двунаправленное отображение между английским языком и логикой, а также непосредственное выполнение логики, является возможность объяснять свои результаты на английском языке на уровне бизнеса или науки.

In software development, formal methods are mathematical approaches to solving software (and hardware) problems at the requirements, specification, and design levels. Formal methods are most likely to be applied to safety critical or security critical software and systems, such as avionics software. Software safety assurance standards, such as DO 178C allows the usage of formal methods through supplementation, and Common Criteria mandates formal methods at the highest levels of categorization. For sequential software, examples of formal methods include the B Method, the specification languages used in automated theorem proving, RAISE, and the Z notation. In functional programming, property based testing has allowed the mathematical specification and testing (if not exhaustive testing) of the expected behaviour of individual functions. The Object Constraint Language (and specializations such as Java Modeling Language) has allowed object oriented systems to be formally specified, if not necessarily formally verified. For concurrent software and systems, Petri nets, process algebra, and finite state machines (which are based on automata theory; see also virtual finite state machine or event driven finite state machine) allow executable software specification and can be used to build up and validate application behaviour. Another approach to formal methods in software development is to write a specification in some form of logic—usually a variation of first order logic—and then to directly execute the logic as though it were a program. The OWL language, based on description logic, is an example. There is also work on mapping some version of English (or another natural language) automatically to and from logic, as well as executing the logic directly. Examples are Attempto Controlled English, and Internet Business Logic, which do not seek to control the vocabulary or syntax. A feature of systems that support bidirectional English–logic mapping and direct execution of the logic is that they can be made to explain their results, in English, at the business or scientific level.

Формальные методы и обозначения

Существует множество формальных методов и нотаций.

Решающие и конкурсы

Многие задачи в формальных методах являются NP-трудными, но могут быть решены для случаев, возникающих на практике. Например, задача булевой выполнимости является NP-полной согласно теореме Кука — Левина, но решатели SAT способны решать множество больших экземпляров. Существуют "решатели" для различных задач, возникающих в формальных методах, и регулярно проводятся соревнования для оценки современного уровня развития методов решения таких задач. Конкурс SAT — это ежегодное соревнование, сравнивающее решатели SAT. Решатели SAT используются в инструментах формальных методов, таких как Alloy. CASC — это ежегодный конкурс автоматических доказателей теорем. SMT COMP — это ежегодный конкурс решателей SMT, применяемых для формальной верификации. CHC COMP — это ежегодный конкурс решателей для ограниченных клауз Хорна, которые находят применение в формальной верификации. QBFEVAL — это двухгодичный конкурс решателей для квантифицированных булевых формул, которые применяются при проверке моделей. SV COMP — это ежегодный конкурс инструментов верификации программного обеспечения. SyGuS COMP — это ежегодный конкурс инструментов синтеза программ.