Интернет магазин китайских планшетных компьютеров



Компьютеры - Формальные методы - Критика формальных методов

22 января 2011


Оглавление:
1. Формальные методы
2. Разновидности формальных методов
3. Использование формальных методов
4. Критика формальных методов



Легко догадаться, какие претензии предъявляются к формальным методам: доказательства вручную требуют серьёзных вложений времени и не дают никакой выгоды, кроме подтверждения правильности. В результате формальные методы используются или в тех областях, где доказательства можно получить автоматически программным путём, или в тех, где цена ошибки слишком высока. Например, при создании космических аппаратов или магнитно-резонансных томографов необнаруженные ошибки приводят к гибели людей, а при проектировании интерфейсов пользователя или браузеров — в худшем случае к порче настроения, поэтому в первых двух случаях формальные методы будут применяться, а в последних — нет.

Абстракции, нотации и языки формальных методов

  • Абстрактная интерпретация 
  • Абстрактный автомат
    • Конечный автомат
    • Машина Тьюринга
    • Модель Крипке
  • Автомат Бюхи 
  • Alloy Analyzer 
  • Анализ программного кода и построенных по нему графов:
    • Анализ потока данных 
    • Анализ потока управления 
    • Динамический анализ кода
    • Статический анализ кода
  • B-метод 
  • Венский метод разработки 
  • Единый язык алгебраических спецификаций  и программа Hets
  • Исчисления процессов:
    • Алгебра общающихся систем 
    • Взаимодействующие последовательные процессы  Хоара
    • Исчисление общающихся систем
    • пи-исчисление
    • Язык спецификации временного упорядочивания 
  • Lustre 
  • Лямбда-исчисление, включая типизированное
  • Модель акторов
  • Переписывание
  • Промела  и верификатор моделей SPIN 
  • Ребека 
  • Сети Петри
  • Создание и анализ распределённых процессов 
  • Темпоральная логика
  • Универсальный язык систем 
  • Эстерел 
  • Язык спецификации ANSI/ISO C  и верификатор Frama-C
  • Язык спецификации и описания 
  • Z-нотация


Просмотров: 3570


<<< Философия UNIX
Функциональная спецификация >>>