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