Формальные методы и предприятия [закрыто]

Question

Так...

Я преподаю формальные методы разработки программного обеспечения.Я также преподаю «гибкие методологии».Большинство людей, кажется, думают, что это противоречиво.Я думаю, это имеет большой смысл...Я также работаю в компании, где нам нужно действительно что-то делать :) Хотя я могу применять свои заработанные очки навыков в «спецификациях» в повседневной жизни, мои коллеги обычно избегают слова «формальный».

Раньше я думал, что это связано с тем, как мы учимся программировать:обычно мы стремимся найти работающее решение, а не понять проблему.Тогда я подумал, что это связано с тем, что большинство людей в формальном сообществе — не инженеры, а математики или компьютерщики.Сегодня мне интересно, не потому ли это, что сообщество формальных методов прикрывается каким-то законом «обфускации», чтобы использовать все доступные символы UNICODE, активно разрабатывать грубые, неэстетичные инструменты и смеяться над стандартами.

Да, я перешел от точки зрения «винить их» к точке зрения «винить нас» ;-)

Итак, мой вопрос:Используете ли вы какие-либо формальные методы в своей компании?Вы их представили или это были предпосылки?Какие методы вы используете, чтобы очистить туман математики от страхов людей и побудить их использовать формальные методы?Чего, по вашему мнению, не хватает современным инструментам для более широкого использования?

Answer 1

Ключ к тому, чтобы заставить людей покупать любой методы или методологии — показать им, как они решают проблемы, с которыми они сталкиваются.Если они увидят, что это улучшит их жизнь, у вас будет гораздо больше шансов убедить их освоить эти методы.

И если вы не мочь покажите им, что, возможно, вы хотели принять методы, основанные на философии, а не на практике.Если другие не разделят вашу философию, вы никуда не добьетесь.И, возможно, вам не следует.

За прошедшие десятилетия появилось очень много методологий.Новые проекты всегда устраняют недостатки старых, однако проекты по-прежнему сталкиваются с проблемами и терпят неудачу.Почему?Потому что рок-звезды, придумывающие новые методологии, являются рок-звездами и создали новую методологию именно потому, что понимают основные проблемы и способы их применения.Те, кто приходят после, склонны слепо следовать рецепту, и он работает не так хорошо.

Поэтому я думаю, что лучше всего рассказать об основных проблемах, а затем показать, как различные методы пытаются справиться с этими проблемами.Различия между компаниями, проектами и командами настолько велики, что ни одну методологию нельзя успешно применить ко всем комбинациям.Крайне важно научиться выбирать подходящий инструмент и правильно его применять.

Answer 2

Спасибо за все вклады.Они очень проницательны.Позвольте мне немного погорячиться (но не принимайте это на свой счёт :-)

Большинство людей, похоже, думают, что формальные методы — это всего лишь проверка программы.Или критические системы.Это может быть правдой, если мы будем следовать окончательному клише:чтобы доказать, что мы делаем программу правильно (т.валидация, которая, как сказал один из участников, спрашивает, правильно ли мы выполняем программу).

Но рассмотрите инструменты поиска/проверки моделей, такие как Alloy.Обучение использованию такого инструмента занимает незначительное количество времени для любого, кто привык к UML и ОО.Тем не менее, это может дать вам немедленное представление о вашей модели.Обычно поиск контрпримера для достаточно небольшого подмножества модели, которую вы пытаетесь использовать, занимает не более 10 минут (включая в первую очередь описание модели в Alloy).

Возьмем, к примеру, разработку требований.Обычно рисуют много UML.Однако мало кто использует OCL, и многие бизнес-правила неформально аннотированы на естественном языке.Почему?Временные ограничения?

Теперь учтите тот факт, что большинство просто использует свое интуитивное чутье, чтобы доказать, что модель выполнима.Опять же, почему?Я могу потратить столько же времени (возможно, даже меньше, поскольку мне не нужно заботиться об эстетике рисования), чтобы написать эту модель в Alloy и просто проверить ее выполнимость?И какая математика мне теперь нужна?«Предикаты»?Причудливое название для IF и логических значений ;-) Кванторы?Причудливые имена для ForEachs()...

А как насчет больших информационных систем?Им не нужна критика...Просто попробуйте проанализировать в уме концептуальную (не реализационную!) диаграмму, содержащую более 600 классов.Я вижу, как многие люди бьются головой о стену из-за легко допущенных ошибок модели, потому что они упустили какое-то ограничение или модель допускает глупые вещи.

Дело в том, что не нужно использовать формальные подходы с головы до хвоста.Конечно, я мог бы проверить все приложение в Coq и подтвердить, что оно на 100% соответствует некоторой спецификации.Это может быть подход компьютерного ученого/математика.

Тем не менее, с философией GTD, почему я не могу делегировать некоторые задачи компьютеру и позволить ему улучшить мое развитие?Действительно ли это вопрос «времени» или просто отсутствие технических способностей и желания учиться/вводить инновации?

Answer 3

Работа над развитием ИТ-направления на предприятии означает необходимость передачи знаний о бизнесе от реальных деловых людей в головы разработчиков.Хотя я сам считаю абстрактную математику одним из величайших развлечений, это ужасный инструмент общения.А коммуникация – это то, о чем идет речь.Хотя я мог бы добиться определенного успеха в том, чтобы убедить ИТ-специалистов использовать более абстрактные обозначения, у меня практически нет шансов с деловыми людьми.

Хотя есть некоторые области, в которых я вижу роль формальных методов на предприятии (специальное программное обеспечение, требующее больших математических и логических операций, значительная потребность в доказуемых свойствах, как в программном обеспечении, критически важном для безопасности), они мало помогают в получении правильных требований, например.как выполнить заказ клиента, выдав один или несколько заказов на поставку множеству возможных внешних или внутренних поставщиков.

Я думаю, что еще не решен вопрос о подходах, основанных на моделях, и языках, специфичных для предметной области.Я думаю, что они добьются успеха или потерпят неудачу в зависимости от того, предоставят ли они более быструю обратную связь от ИТ с пожеланиями и потребностями бизнеса и предполагают ли они, что деловым людям придется провести какое-либо существенное исследование.

Технология проста.Общение затруднено.Формальные методы могут помочь нам поступать правильно, но те, которые я видел, не помогают нам поступать правильно.(Да, это клише, но это потому, что они неизбежно и до боли правдивы.)

Answer 4

Я прохожу курс «Спецификация и проверка».В рамках структуры курса мы делаем следующее- 1.Инструменты обучения, такие как PVS (система проверки прототипов) http://pvs.csl.sri.com/ и SMV (Моделирование и проверка программного обеспечения) http://www.cs.cmu.edu/~modelcheck/smv.html2.Кроме того, мы анализируем аварии, произошедшие из-за сбоев программного обеспечения.Например,- Провал Арианы V

Я считаю, что формальные методы более применимы к сценариям, где стоимость отказа превышает стоимость проектирования.И кажется целесообразным использовать их для программного обеспечения, используемого в критических системах.Я предполагаю, что он используется в авионике, проектировании чипов и т. д.и нынешняя автомобильная промышленность также реализует это на практике.

Answer 5

Я несколько раз пытался убедить людей принять методы формальной спецификации (Z и Alloy) и получил тот же опыт, что и вы:Большинству людей, хотя и кажется, что они служат полезной цели, очень неудобно использовать их для реальной работы.

Как ни странно, одни и те же люди более чем счастливы создавать совершенно бесполезные UML-диаграммы в огромных количествах.

Я думаю, что для этого есть две основные причины:

а.) Многим разработчикам не нравится уровень абстракции, требуемый формальным подходом.Тот факт, что большая часть математического образования начального уровня представляет собой исключительно исчисление, а не дискретную математику, возможно, имеет какое-то отношение к этому.

б.) Формальные методы требуют подхода к проектированию «снизу вверх», при котором вы проектируете свою базовую модель с нуля, делаете ее герметичной, а затем подключаете ее к реальным требованиям пользователя, предоставляя поверх нее интерфейс.Поскольку мы склонны считать, что усилия по разработке определяются требованиями, нисходящий подход кажется более естественным, хотя он часто приводит к противоречивым моделям.Это похоже на переоборудование подвала под вашим домом после того, как он уже построен.

Answer 6

Формальные методы не имеют смысла в системах, где цена отказа невелика.

В рабочем веб-приложении у вас есть несколько внешних блоков, несколько серверных блоков, несколько блоков баз данных — если программа на любом из них выходит из строя, это не событие.Аппаратное обеспечение настолько дешево, что вы можете построить эти системы гораздо дешевле, чем стоимость формального определения всего вашего программного обеспечения.