К сожалению да, бумажный вариант думаю уже тяжело будет найти (хотя ещё относительно недавно видел его в продаже).
Но есть возможность электронного варианта: www.ozon.ru/context/detail/id/32561151
У меня была (и есть) немного другая идея: по спеке генерить код, который можно было вставлять в код рабочего продукта и снимать трассу выполнения. И эту трассу отправлять в параллельно бегущий model-checker (например, TLC), который бы сравнивал трассу на соответствие модели.
Либо по LTL и др. формулам из модели генерить проверяющий автомат, который бы работал по трассе событий из ПО и анализировал бы эту трассу на корректность.
Это позволило бы быстро ловить ошибки в логике ПО, где эта логика расходится с моделью.
И, кажется на первый взгляд, это вполне можно применять даже в продакшн-коде (зависит от величины модели и её детализации), когда рядом с боевым кодом всегда бежит проверяющий автомат и сразу сигнализирует, если вдруг что пошло не так (например, может приостановить боевой экземпляр ПО, запустить gdb attach, закрыть машину от нагрузки и позвать службу поддержки для решения проблемы).
Таким образом можно будет ловить проблемы на очень ранних стадиях, до того, как эффект от проблемы стал существенным (например, до того как положили в БД некорректные данные).
Одна из существенных проблем современной индустрии ПО, что разработка начинается намного раньше даже нормального осмысления требований, не говоря уже про полноту.
В результате — забиваем гвозди микроскопами, пытаемся ломом починить микросхемы и пр. Получаем в результате больших плохоподдерживаемых монстров из сильносвязанного спагетти-кода и пр.
Хотя весьма хорошо развивается область Requirements Management, есть хорошая литература по проблематике анализа и разработки требований (например, уже упомянутая в статье «Problem Frames») и тд. То есть, есть методики, инструменты и пр. для того, чтобы и к разработке требований подходить профессионально и серьёзно.
Причем современные инструменты позволяют серьёзно уменьшить затраты усилий на хорошую проработку требований. С требованиями сейчас тоже можно работать итеративно в стиле agile.
Очень интересный пример, когда сначала проанализировали требования, затем написали спеки и потом только стали кодить: OpenCOM RTOS. В итоге объем кода, по сравнению с предшествующим вариантом ПО, уменьшился на порядок (в 10 раз, как пишут в книге). Что было удивительно даже для самих авторов проекта, они даже не предполагали настолько сильный эффект.
Изначально статья была чуть больше (раза в два :) ), но для публикации это показалось слишком объёмным и поэтому оставлено было только самое интересное с точки зрения разработчиков. Вот в первоначально варианте и была большая мотивировочная часть, где как раз и писалось про то, что везде нужен разумный подход и нет смысла очередную игру «тетрис» для мобильников разрабатывать используя, например, формальные методы.
В целом, сейчас моделирование вполне доступно для широкого применения даже в повседневной работе. Например, когда встаёт вопрос по оптимизациям логики работы с базой данных многих потребителей, как сократить количество блокировок и безопасно часть работы сделать асинхронной и тд.
Рекомендую посмотреть примеры в блоге Hillel Wayne, там видно, что моделирование можно легко и малозатратно применять даже для моделирования логики UI (в статье есть ссылка на это).
Одна из целей данной статьи — показать, что моделирование (поиск и проверка моделей) сейчас стало весьма дешёвым и удобным в использовании и его вполне можно применять в весьма широком классе задач.
Естественно, нужно разумно подходить ко всем используемым инструментам и хорошо понимать, где и какие инструменты стоит использовать. Но для этого нужно минимальное знакомство с инструментами, на что и направлена данная (и последующие) статья.
В следующих статьях (надеюсь, что будет возможность продолжить цикл статей в нормальном темпе) я планирую вернуться к вопросам применимости разных методов для разных задач, там более подробно будут рассмотрены классы задач и применимость различных методов для этих классов, соотношение усилий применения методов и полученного результата с реальными примерами из промышленности.
Данная статья эти вопросы оставила в стороне, так как в основном такие вопросы для разработчиков существенно менее интересны, чем технические подробности и примеры применения.
Да не за что.
Рад, что статья понравилась.
К сожалению да, бумажный вариант думаю уже тяжело будет найти (хотя ещё относительно недавно видел его в продаже).
Но есть возможность электронного варианта: www.ozon.ru/context/detail/id/32561151
Либо по LTL и др. формулам из модели генерить проверяющий автомат, который бы работал по трассе событий из ПО и анализировал бы эту трассу на корректность.
Это позволило бы быстро ловить ошибки в логике ПО, где эта логика расходится с моделью.
И, кажется на первый взгляд, это вполне можно применять даже в продакшн-коде (зависит от величины модели и её детализации), когда рядом с боевым кодом всегда бежит проверяющий автомат и сразу сигнализирует, если вдруг что пошло не так (например, может приостановить боевой экземпляр ПО, запустить gdb attach, закрыть машину от нагрузки и позвать службу поддержки для решения проблемы).
Таким образом можно будет ловить проблемы на очень ранних стадиях, до того, как эффект от проблемы стал существенным (например, до того как положили в БД некорректные данные).
Одна из существенных проблем современной индустрии ПО, что разработка начинается намного раньше даже нормального осмысления требований, не говоря уже про полноту.
В результате — забиваем гвозди микроскопами, пытаемся ломом починить микросхемы и пр. Получаем в результате больших плохоподдерживаемых монстров из сильносвязанного спагетти-кода и пр.
Хотя весьма хорошо развивается область Requirements Management, есть хорошая литература по проблематике анализа и разработки требований (например, уже упомянутая в статье «Problem Frames») и тд. То есть, есть методики, инструменты и пр. для того, чтобы и к разработке требований подходить профессионально и серьёзно.
Причем современные инструменты позволяют серьёзно уменьшить затраты усилий на хорошую проработку требований. С требованиями сейчас тоже можно работать итеративно в стиле agile.
Очень интересный пример, когда сначала проанализировали требования, затем написали спеки и потом только стали кодить: OpenCOM RTOS. В итоге объем кода, по сравнению с предшествующим вариантом ПО, уменьшился на порядок (в 10 раз, как пишут в книге). Что было удивительно даже для самих авторов проекта, они даже не предполагали настолько сильный эффект.
В целом, сейчас моделирование вполне доступно для широкого применения даже в повседневной работе. Например, когда встаёт вопрос по оптимизациям логики работы с базой данных многих потребителей, как сократить количество блокировок и безопасно часть работы сделать асинхронной и тд.
Рекомендую посмотреть примеры в блоге Hillel Wayne, там видно, что моделирование можно легко и малозатратно применять даже для моделирования логики UI (в статье есть ссылка на это).
Одна из целей данной статьи — показать, что моделирование (поиск и проверка моделей) сейчас стало весьма дешёвым и удобным в использовании и его вполне можно применять в весьма широком классе задач.
Естественно, нужно разумно подходить ко всем используемым инструментам и хорошо понимать, где и какие инструменты стоит использовать. Но для этого нужно минимальное знакомство с инструментами, на что и направлена данная (и последующие) статья.
В следующих статьях (надеюсь, что будет возможность продолжить цикл статей в нормальном темпе) я планирую вернуться к вопросам применимости разных методов для разных задач, там более подробно будут рассмотрены классы задач и применимость различных методов для этих классов, соотношение усилий применения методов и полученного результата с реальными примерами из промышленности.
Данная статья эти вопросы оставила в стороне, так как в основном такие вопросы для разработчиков существенно менее интересны, чем технические подробности и примеры применения.