Должен ли я использовать формальные методы в моем программном проекте?

Question

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

Я думал об использовании формальных методов, чтобы прояснить требования к инструменту как для моего клиента, так и для разработчиков. Под формальными методами я подразумеваю некоторую форму моделирования, возможно, что-то математическое. Некоторые из вещей, о которых я читал и которые рассматривают, включают Z (http://en.wikipedia.org/wiki/Z_notation), конечные автоматы, UML 2.0 (возможно, с расширениями, такими как OCL ), сети Петри , и некоторые вещи уровня кодирования, такие как контракты, предварительные и последующие условия. Есть ли что-то еще, что я должен рассмотреть?

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

Я пытаюсь определить, стоит ли мне использовать формальные методы в этом проекте, и если да, то в какой степени. Я знаю, «это зависит», поэтому наиболее полезные ответы для меня - это да / нет и аргументы в поддержку.

Вы бы использовали формальные методы, если бы были в этом проекте?

Answer 1

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

Очень немногие разработчики имеют опыт формальных методов. Единственный раз, когда я видел клиентов с формальным обучением методам, были членами ZUG, когда мы портировали CADiZ на Windows.

Под формальными методами я имею в виду некоторую форму моделирования, возможно, что-то математическое. Некоторые из вещей, о которых я читал и которые рассматривают, включают Z (http://en.wikipedia.org/wiki/Z_notation), конечные автоматы, UML 2.0 (возможно, с расширениями, такими как OCL), сети Петри и некоторые вещи уровня кодирования, такие как контракты, а также пре и пост. условия. Есть ли что-то еще, что я должен рассмотреть?

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

Некоторым техническим клиентам, которые вы ожидаете найти с помощью инструмента требований к программному обеспечению, довольно удобно работать с UML.

Может иметь смысл создание Z-модели вашего домена, и может иметь значение создание модели пи-исчисления для обмена сообщениями между клиентом и сервером (или petri-net, но я считаю, что pi и проще, и мощнее ).

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

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

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

Специалисты по Z, с которыми я работал в 90-х годах, сочли идею задания CASE GUI для Z нелепой. Создание модели UML для такого графического интерфейса является обычным делом.

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

Answer 2

Есть несколько успешных примеров использования ACSL (языка спецификаций ANSI C), который имеет зрелый набор инструментов, большинство из которых с открытым исходным кодом, например, почему платформа, Frama-C. Для Java аналогичная технология называется JML (Java Modeling Language). Я думаю, что оба используются для небольших и средних проектов для встроенных приложений, и они помогают добавить некоторые гарантии в ваш код, но не направлены на проверку спецификаций. Z абсолютно не удобен для пользователя и не имеет адекватной поддержки инструментов IMHO.

Среди коммерческих инструментов, которые можно использовать на этапах спецификации, я бы обратился к платформе Rodin, основанной на B-методе.

Answer 3

Позднее в игре здесь, но вы можете рассмотреть что-то вроде тестируемой архитектуры через Savara , которую мы используем для многих проектов, где преобладает взаимодействие или взаимодействие между компонентами. Это чаще всего наблюдается в любом бэкэнде SOA для веб-интерфейса.

Он формально основан на пи-исчислении, и вам не нужно понимать пи-исчисление, чтобы использовать его.

Answer 4

Я рассматривал несколько подходов к «легким» формальным методам, для приложений, которые могут быть критически важными, но не жизненно важными. Некоторые идеи:

• Сплав
• SysML
• SPIN
• Другие ???

Answer 5

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

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

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

Answer 6

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

Перевесят ли производительность и результат сложность и необходимые знания?

Answer 7

Я согласен с Томом и Абуфардехом - перевесят ли производительность и результат сложность и необходимые знания?

Кроме того, лучше ли использовать этот метод для получения ВСЕХ требований перед разработкой (и гарантировать, что эти требования и четко определены, и проверены)? Получение всех требований сначала кажется здравым смыслом, но большой процент программ делает вещи параллельно, думая, что это не проблема - получить некоторые требования позже. Требования ползучести это кошмар! Фильм «Войны Пентагона» откроет глаза любому, кто не согласен.

Answer 8

Я полностью согласен с Томом и задаю тот же вопрос,

Перевесят ли производительность и результат сложность и необходимые знания?

По моему мнению, если система / программное обеспечение не может быть идентифицировано как «критическое для безопасности», формальные методы не нужны.

Что означает критический для безопасности:

Когда сбой компьютерной системы может привести к катастрофическим последствиям, таким как гибель людей, ущерб окружающей среде или повреждение самой системы, такая система называется «критической для безопасности». *