Должен ли я использовать формальные методы в своем программном проекте?
https://stackoverflow.com/questions/735609
italiano
english
français
española
中国
日本の
العربية
Deutsch
한국어
Português
RussianВопрос
Наш клиент хочет, чтобы мы создали веб-приложение для сбора требований к программному обеспечению.По сути, это веб-кейсовый инструмент, который следует определенному процессу получения требований от заинтересованных сторон.Я руководитель проекта, и мы все еще находимся на ранней стадии проекта.
Я думал об использовании формальных методов, которые помогли бы прояснить требования к инструменту как для моего клиента, так и для разработчиков.Под формальными методами я подразумеваю некоторую форму моделирования, возможно, что-то математически обоснованное.Некоторые из вещей, о которых я читал и которые рассматриваю, включают Z (http://en.wikipedia.org/wiki/Z_notation), конечные автоматы, UML 2.0 (возможно, с такими расширениями, как OCL), Сети Петри, и некоторые вещи на уровне кодирования, такие как контракты и предварительные и последующие условия.Есть ли что-нибудь еще, что я должен рассмотреть?
Разработчики опытны, но в зависимости от используемого формализма им, возможно, придется немного подучить математику.
Я пытаюсь определить, стоит ли мне использовать формальные методы в этом проекте, и если да, то в какой степени.Я знаю, что "это зависит", поэтому самые полезные ответы для меня - это "да" / "нет" и подтверждающие аргументы.
Стали бы вы использовать формальные методы, если бы участвовали в этом проекте?
Решение
Я думал об использовании формальных методов, которые помогли бы прояснить требования к инструменту как для моего клиента, так и для разработчиков.
Очень немногие разработчики имеют опыт работы с формальными методами.Единственный раз, когда я видел клиентов, обучающихся формальным методам, были члены ZUG, когда мы занимались портированием КАДиС к Окнам.
Под формальными методами я подразумеваю некоторую форму моделирования, возможно, что-то математически обоснованное.Некоторые из вещей, о которых я читал и которые рассматриваю, включают Z (http://en.wikipedia.org/wiki/Z_notation), конечные автоматы, UML 2.0 (возможно, с расширениями, такими как OCL), сети Петри и некоторые вещи на уровне кодирования, такие как контракты и предварительные и последующие условия.Есть ли что-нибудь еще, что я должен рассмотреть?
Существует очень большой разрыв между Z, который является формальным методом, основанным на теории множеств, и UML, который представляет собой неформальную нотацию с некоторыми полуформальными обозначениями (конечными автоматами), помеченными тегами.
Некоторые технические клиенты, которых вы ожидаете найти, используя инструмент требований к программному обеспечению, вполне комфортно работают с UML.
Может быть полезно создать Z-модель вашего домена, и может быть полезно создать модель обмена сообщениями между клиентом и сервером на основе pi-исчисления (или petri-net, но я считаю, что pi одновременно проще и мощнее).
То, что дала бы Z-модель вашего домена, - это независимый от реализации набор ограничений типов, выраженный более мощно, чем система типов любого распространенного языка реализации.
Формальная модель обмена сообщениями дала бы вам возможность выполнять анализ, чтобы убедиться, что вы не теряете обновления, не получаете конфликтов или взаимоблокировок.
Модель UML дает вам обозначение для разбиения большой системы на функциональные области (диаграммы пакетов), показывающее, как классы в этих областях статически связаны друг с другом (диаграммы классов), показывающее, как экземпляры этих классов связаны динамически (диаграммы последовательности, активности и взаимодействия), и показывающее, как пакеты развертываются (диаграммы компонентов и развертывания).Они полезны для общения в команде и для того, чтобы немного конкретизировать идеи, но не имеют формально определенной семантики, которая допускает очень сложный анализ.
Специалисты по Z, с которыми я работал в 90-х, считали идею указания графического интерфейса CASE в Z нелепой.Создание UML-модели для такого графического интерфейса является обычным делом.
Я не использовал формальные предварительные и последующие условия разработки по контракту, хотя иногда добавляю их в комментарии и часто в утверждениях, а также выполняю модульные тесты условий, которые могут их нарушать.
Другие советы
Истинный вопрос, который следует задать здесь, заключается не в том, использовать их или нет, а в том, что приобретается и теряется.
Перевесят ли производительность и конечный результат сложность и необходимость обучения?
В общем, вы должны использовать то, что удобно команде.С новыми предметами придется учиться, а это значит, что возникнут вопросы о процессе и допущенных ошибках.Часть вашего графика разработки будет использована для исправления этих проблем, и если вы не планируете использовать их с этой командой в будущем, на самом деле у вас не будет долгосрочного выигрыша от внедрения чего-то нового.Процесс изменений занимает много времени и кропотливой работы.
Если у вас есть достаточно времени, чтобы справиться с этими проблемами, возможно, все будет в порядке ... если ваша оценка верна.Учитывая, что вы не работали с этими людьми (по крайней мере, так звучит ваш пост), скорее всего, ваш график не будет таким точным, как следовало бы, а это значит, что вы могли не выделить достаточно времени для завершения проекта, не говоря уже о внедрении нового процесса.
Другой вопрос, который вы должны задать себе, звучит так: "насколько вам комфортно в процессе, который вы хотите внедрить?" Я никогда не пытаюсь внедрить новый процесс в проекте, если не знаю, что смогу провести команду через это, если потребуется.Пробовать что-то новое время от времени - это хорошо, но вам нужна команда, с которой вам комфортно, чтобы знать, как выйти из сложной ситуации.
Есть несколько успешных примеров использования ACSL (ANSI C Specification Language), который имеет зрелый набор инструментов, большинство из которых с открытым исходным кодом, таких как Why platform, Frama-C.Для Java аналогичная технология называется JML (язык моделирования Java).Я думаю, что оба используются для проектов малого и среднего размера для встраиваемых приложений, и они помогают добавить некоторые гарантии в ваш код, но не направлены на проверку спецификаций.Z абсолютно не удобен в использовании и не имеет адекватной инструментальной поддержки, ИМХО.
Среди коммерческих инструментов, которые могут быть использованы на этапах спецификации, я бы рассмотрел платформу Rodin, основанную на B-методе.
Здесь уже поздно играть, но вы могли бы подумать о чем-то вроде тестируемая архитектура с помощью Savara который мы используем для многих проектов, где преобладает коммуникация или взаимодействие между компонентами.Чаще всего это наблюдается в любом SOA-бэкэнде веб-интерфейса.
Формально он основан на pi-исчислении, и вам не нужно понимать pi-исчисление, чтобы использовать его.
Я полностью согласен с Томом и задаю тот же вопрос,
Перевесят ли производительность и конечный результат сложность и необходимость обучения?
На мой взгляд, если только система / программное обеспечение не может быть идентифицировано как “критичное к безопасности”, формальные методы не нужны.
Что означает критическое значение для безопасности:
Когда сбой компьютерной системы может привести к катастрофическим последствиям, таким как гибель людей, ущерб окружающей среде или повреждение самой системы, такая система называется “критичной к безопасности”.
Я согласен и с Томом, и с Абуфардехом - перевесят ли производительность и результат сложность и необходимость обучения?
Кроме того, является ли этот метод лучшим для получения ВСЕХ требований перед разработкой (и обеспечения того, чтобы эти требования были четко определены и поддавались тестированию)?Получение всех требований сначала кажется здравым смыслом, но большой процент программ выполняет что-то параллельно, думая, что нет проблем получить некоторые требования позже.Ползучие требования - это кошмар!Фильм "Войны Пентагона" открывает глаза любому, кто с этим не согласен.
