Формальные методы ( англ. Formal methods ) - в компьютерных науках, построенные на математике методы написания спецификаций, разработки и проверки ( англ.verification ) программного обеспечения и компьютерного оборудования. Этот подход особенно важен для встроенных систем , для которых важны надежность или безопасность, для защиты от ошибок в процессе разработки. Применение формальных методов особенно эффективно на ранних этапах написания требований и спецификаций, но они также могут применяться для полностью формальной разработки реализации (например, программы).
Таксономия
Формальные методы могут быть применены на нескольких уровнях:
- Уровень 0
- Написание формальной спецификации и неформализованная разработка, на ее основе, программы . Такой подход, также, называется упрощенные формальные методы. Он может быть самым оптимальным подходом с точки зрения затрат во многих случаях.
- Уровень 1
- Формальный подход к разработке и проверки программного обеспечения может использоваться для более формально реализации программы. Например, может выполняться доведение свойств или уточнения ( англ. refinement ) с формальной спецификации в программе. Такой подход наиболее оптимальный во встроенных системах, которые должны иметь высокий уровень безопасности или надежности.
- Уровень 2
- Возможно применение систем автоматического доказательства теорем для проведения полностью автоматизированной проверки доказательства теорем. Это может быть слишком дорого, и, на практике, применяется в случаях, когда цена ошибки может быть слишком высокой (например, в критически важных частях схемы микропроцессоров ).
