В течение почти трех десятилетий было предложено большое количество формальных методов, их цель состоит в том, чтобы снизить стоимость строительства компьютерных систем и улучшить их качество. Неофициально, формальный метод - это математическая техника или инструмент, который полезен в разработке аппаратного или программного обеспечения. В последнее время формальные методы сыграли значительно активную роль в проектировании аппаратных средств. Все больше и больше компаний, которые продают микропроцессоры и аппаратные чипы, такие как Intel, IBM, и Motorola, используют инструменты на основе формальных методов, например, модели контроллеров [1] и программы автоматического доказательства теорем [2], для обнаружения дефектов в проектах.
Формальные методы всѐ реже применяются в разработке программного обеспечения, однако в недавних случаях, были обнаружены ранее неизвестные дефекты в программах. Один из ярких примеров является результат исследований в SLAM проекта от Microsoft, в котором Болл и Раджамани разработали несколько формальных методов для автоматического обнаружения дефектов в драйверах устройств [3]. В 2006 году Microsoft выпустила Статическую проверку драйверов (SDV-Static Driver Verifier) [4] в рамках Windows Vista, SDV использует SLAM программную модель для проверки двигателя, выявляя драйверы устройств, нарушающие правила из набора правил интерфейса. Таким образом SDV помогает раскрыть дефекты в драйверах устройств.
Разделы знаний
- Архитектура
- Биология
- Военное дело
- Востоковедение
- География
- Журналистика
- Инженерное дело
- Информатика
- Ипотека, кредиты, залоги
- История
- Культурология
- Литература
- Математика
- Медицина
- Международные отношения
- Педагогика
- Политика
- Политология
- Психология
- Религиоведение
- Сельское хозяйство
- Социология
- Технические науки
- Физика
- Физическая культура
- Филология
- Философия
- Химия
- Экология
- Экономика
- Этнология
- Юриспруденция