Формальные методы - Formal methods

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

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

Фон

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

Таксономия

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

Уровень 0: Может быть предпринята формальная спецификация , а затем на ее основе неформально разработана программа. Это было названо упрощенными формальными методами . Во многих случаях это может быть наиболее рентабельным вариантом.

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

Уровень 2: Средства доказательства теорем могут использоваться для проведения полностью формальных доказательств, проверенных машиной. Несмотря на улучшение инструментов и снижение затрат, это может быть очень дорогостоящим и практически оправданным только в том случае, если цена ошибок очень высока (например, в критических частях операционной системы или конструкции микропроцессора).

Дополнительная информация об этом раскрыта ниже .

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

  • Денотационная семантика , в которой значение системы выражается в математической теории областей . Сторонники таких методов полагаются на хорошо понятную природу доменов, чтобы придать смысл системе; критики отмечают, что не каждую систему можно интуитивно или естественно рассматривать как функцию.
  • Операционная семантика , в которой значение системы выражается как последовательность действий (предположительно) более простой вычислительной модели. Сторонники таких методов указывают на простоту своих моделей как средство выразительной ясности; критики возражают, что проблема семантики только что отложена (кто определяет семантику более простой модели?).
  • Аксиоматическая семантика , в которой значение системы выражается в терминах предусловий и постусловий, которые выполняются до и после того, как система выполнит задачу, соответственно. Сторонники отмечают связь с классической логикой ; критики отмечают, что такая семантика на самом деле никогда не описывает то, что делает система (только то, что верно до и после).

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

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

Использует

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

Технические характеристики

Формальные методы могут использоваться для описания разрабатываемой системы на любом желаемом уровне (ах) детализации. Это формальное описание можно использовать для руководства дальнейшими разработками (см. Следующие разделы); кроме того, его можно использовать для проверки того, что требования к разрабатываемой системе были полностью и точно определены, или для формализации требований к системе, выражая их на формальном языке с точным и однозначно определенным синтаксисом и семантикой.

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

Разработка

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

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

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

Проверка

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

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

Подтверждение подписи

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

Доказательство, направленное человеком

Иногда мотивацией для доказательства правильности системы является не очевидная потребность в подтверждении правильности системы, а желание лучше понять систему. Следовательно, некоторые доказательства правильности производятся в стиле математических доказательств : рукописные (или набранные) с использованием естественного языка с использованием уровня неформальности, общего для таких доказательств. «Хорошее» доказательство - это такое, которое читают и понимают другие люди.

Критики таких подходов указывают, что неоднозначность, присущая естественному языку, позволяет не обнаруживать ошибки в таких доказательствах; часто тонкие ошибки могут присутствовать в деталях низкого уровня, которые обычно упускаются из виду при таких доказательствах. Кроме того, работа, связанная с созданием такого хорошего доказательства, требует высокого уровня математической сложности и опыта.

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

Напротив, растет интерес к получению доказательств правильности таких систем с помощью автоматизированных средств. Автоматизированные методы делятся на три основные категории:

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

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

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

Критики отмечают, что некоторые из этих систем подобны оракулам : они заявляют истину, но не объясняют эту истину. Также существует проблема « проверки верификатора »; если программа, которая помогает в проверке, сама по себе не доказана, могут быть основания сомневаться в достоверности полученных результатов. Некоторые современные инструменты проверки моделей создают «журнал проверки», в котором подробно описывается каждый этап проверки, что позволяет выполнять независимую проверку при наличии подходящих инструментов.

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

Приложения

Формальные методы применяются в различных областях аппаратного и программного обеспечения, включая маршрутизаторы, коммутаторы Ethernet, протоколы маршрутизации, приложения безопасности и микроядра операционной системы, такие как seL4 . Есть несколько примеров, в которых они использовались для проверки функциональности аппаратного и программного обеспечения, используемого в контроллерах домена. IBM использовала ACL2 , средство доказательства теорем, в процессе разработки процессоров AMD x86. Intel использует такие методы для проверки своего оборудования и прошивки (постоянное программное обеспечение, запрограммированное в постоянную память). Dansk Datamatik Center использовал формальные методы в 1980-х годах для разработки системы компиляции для языка программирования Ada, которая впоследствии стала долгоживущим коммерческим продуктом.

Есть несколько других проектов НАСА, в которых применяются формальные методы, такие как система воздушного транспорта нового поколения , интеграция системы беспилотных летательных аппаратов в национальную систему воздушного пространства и скоординированное разрешение и обнаружение конфликтов с помощью воздушных судов (ACCoRD). Метод B с Atelier B используется для разработки автоматов безопасности для различных метрополитенов, установленных по всему миру компаниями Alstom и Siemens , а также для сертификации Common Criteria и разработки моделей систем ATMEL и STMicroelectronics .

Формальная проверка часто используется в оборудовании большинства известных поставщиков оборудования, таких как IBM, Intel и AMD. Есть много областей аппаратного обеспечения, в которых Intel использовала FM для проверки работы продуктов, таких как параметризованная проверка согласованного с кешем протокола, проверка механизма выполнения процессора Intel Core i7 (с использованием доказательства теорем, BDD и символьной оценки), оптимизация для архитектуры Intel IA-64 с использованием светового средства доказательства теорем HOL и проверки высокопроизводительного двухпортового контроллера Gigabit Ethernet с поддержкой протокола PCI Express и усовершенствованной технологии управления Intel с использованием Cadence. Аналогичным образом IBM использовала формальные методы для проверки силовых вентилей, регистров и функциональной проверки микропроцессора IBM Power7.

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

В разработке программного обеспечения формальные методы - это математические подходы к решению программных (и аппаратных) проблем на уровнях требований, спецификаций и проектирования. Формальные методы, скорее всего, будут применяться к критически важному для безопасности или критически важному для безопасности программному обеспечению и системам, таким как программное обеспечение авионики . Стандарты обеспечения безопасности программного обеспечения, такие как DO-178C, допускают использование формальных методов посредством дополнений, а Common Criteria предписывает формальные методы на самых высоких уровнях категоризации.

Для последовательного программного обеспечения примеры формальных методов включают B-метод , языки спецификации, используемые в автоматическом доказательстве теорем , RAISE и Z-нотацию .

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

Язык объектных ограничений (и такие специализации, как язык моделирования Java ) позволил формально определять объектно-ориентированные системы, если не обязательно формально подтверждать их.

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

Другой подход к формальным методам в разработке программного обеспечения - это написать спецификацию в некоторой форме логики - обычно это вариант логики первого порядка (FOL) - а затем напрямую выполнять логику, как если бы это была программа. OWL язык, основанный на Описание Logic (DL), является примером. Также ведется работа по автоматическому отображению некоторой версии английского (или другого естественного языка) на логику и обратно, а также непосредственное выполнение логики. Примерами являются Attempto Controlled English и Internet Business Logic, которые не стремятся контролировать словарный запас или синтаксис. Особенностью систем, поддерживающих двунаправленное отображение логики на английском языке и прямое выполнение логики, является то, что их можно заставить объяснять свои результаты на английском языке на деловом или научном уровне.

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

Доступно множество формальных методов и обозначений.

Языки спецификаций

Модельные шашки

  • ESBMC
  • MALPAS Software Static Analysis Toolset - средство проверки промышленных моделей, используемое для формального подтверждения критических с точки зрения безопасности систем.
  • PAT - бесплатная программа проверки модели, симулятора и средства проверки уточнения для параллельных систем и расширений CSP (например, общих переменных, массивов, справедливости)
  • ВРАЩАТЬСЯ
  • UPPAAL

Организации

Смотрите также

использованная литература

дальнейшее чтение

внешние ссылки

Архивные материалы