"Формальные методы необходимы, но не обязательны". Это, в общем, мнение большинства предприятий, так как эта технология, при её применении, немного "мешает". Она заставляет пересмотреть обычный процесс разработки и так же может оставить программистов без работы. В результате - не большая революция. Если пользователи будут продолжать довольствоваться предлагаемыми продуктами, ситуация поменяется не скоро.
Формальные методы повышают надёжность программного обеспечения, но их использование не распространено. Как вы это объясните?
Возможно, некоторые производители софта не заинтересованны в том чтобы он корректно работал. Что действительно происходит в реальности с широко используемыми программными продуктами. Ко всему прочему ещё потому, что много юзеров любят возится (с софтом) и если что-то хорошо работает, это для них не интересно. Таким образом дисфункционирование программного обеспечения может быть желаемым и рассматриваться как плюс. Но здесь я привожу только положительные стороны. Я не имею в виду профессионалов, которые делают это специально, чтобы затем клиент платил за поддержку. Использование формальных методов с подобными идеями не представляет интереса, так как программа будет работать корректно. Тогда как использование этих методов для гарантии того, что автоматический безшоферный поезд или спутник выполнят правильно свои миссии имеет смысл.
Формальные методы подразумевают затраты большего времени на спецификацию, чем на тесты. Не ставит ли это под сомнение обычный цикл разработки?
В других инженерных дисциплинах, такиь как авиаконструкция или гражданское строительство существуют эквиваленты формальных методов - это понятие конструкторского бюро. Сначала рисуют модель будущего объекта, над которым рассуждают при помощи различных теорий. Идея долгого размышления до реализации есть часть современной инженерии. Использование формальных методов есть конструкторское бюро программного обеспечения: рисунок софта это формальный объект который мы не можем запустить, но над которым мы можем размышлять, моделировать. Большинство программистов считают, что достаточно запустить программу и провести тесты для того чтобы убедится в правильном функционировании. Как, если бы для создания самолета, вы производите что-то похожее на утюг с крыльями и который затем тестируете. Этот способ практиковался в истории технологий, но это примитивный подход. С момента как технология набирает ответственности, применяются работа с моделями или рисунками.
В чем сложность использования формальных методов?
Не легко продвинуть технологии там, где в них не нуждаются. Разработчик для индустрии, не встретивший больших проблем в ходе разработки софта, редко решается изменить этот процесс. Формальные методы хорошо распространяются среди тех кто имеет с этим (процессом разработки) затруднения. Их интеграция в промышленной среде сталкивается с двумя основными затруднениями. Необходимо пересмотреть процесс разработки, для того что бы включить в него базовые элементы формальных методов (уточнение (откладка) и доказательство), а так же это меняет план финансирования. Вместо кульминации затрат в момент тестов, не малые инвестиции необходимы в момент спецификации и концепции. Эти финансовые вложения имеют свойство расти, выбор не прост. Сами же формальные методы не доставляют особых трудностей.
В каких случаях формальные методы наиболее применимы?
Их достаточно много. Например концепция распределенных систем: проблема в том, что в них не существует "главного". В протоколе маршрутизации узел сети не предпринимает решений за другие узлы. Информация меняется и на каждом узле заново определяется дальнейший маршрут, в зависимости от особенностей локальной сети. Таким образом, очень трудно проводить тесты в подобных условиях, так как эти условия исполнения никогда не повторяются. Формальные методы, отчасти, используются для разработки протоколов передачи, маршрутизации и криптографии. Эти методы все больше и больше применяются в задачах, которые неограниченны лишь разработкой софта. В частности, при изучении сложных систем. Необходимо реализовать объект, над которым будет производится дальнейшее размышление, строго соответствующее модели объекта.
В каких странах более всего используются формальные методы?
Европа немного впереди планеты всей. В частности Франция, Англия и Германия. Что же касается американцев, то и них много денег и хорошие методы работы. Люди, участвующие в проекте, очень ответственны. Это компенсирует часть проблемы. В профессиональном отношении, они придают огромное значение качеству специалистов. Кстати, в больших компаниях можно часто встретить высокопоставленных работников, которые являются специалистами (в тексте техниками). Технические знания высоко ценятся, это позволяет создавать качественные системы.
Являются ли формальные методы панацеей?
Сто процентное качество не существует, всегда что-то может произойти. Ели мы установим компьютер в туннеле с множеством электрических помех, значение бита может спонтанно поменяться. Те, кто считают что могут достигнуть отсутствие дефектов не есть настоящие инженеры. Но к этой цели мы можем приблизится. Инженер всегда размышляет с учётом вероятности и в сознании этого он учитывает любой риск, каким бы минимальным он не был.
Jean-Raymond Abrial, независимый консультант и "изобретатель" формального метода B.