Современные и промышленные формальные / строгие методы разработки программного обеспечения

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

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

Недавно я узнал, что существуют формальные методы для проектирования, спецификации и проверки программного обеспечения, такие как нотация и язык Z, венский метод разработки и язык B.

но каково состояние дел в этой области и как их может использовать средний инженер (например, в моей команде)?


architecture formal-methods
person mohamedrashad    schedule 15.10.2019    source источник

Ответы (2)


arrow_upward
2
arrow_downward

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

Некоторые методы обеспечения выполнения требований к программному продукту, которые я видел до сих пор:

Для каждого из этих действий доступно множество инструментов для поддержки разработки.

Типичные проблемы:

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

person Gerd    schedule 18.10.2019

arrow_upward
1
arrow_downward

«Современное состояние» формальных методов спецификации и проверки (FM) является достаточным для значительного улучшения качества разрабатываемых систем, однако самая большая проблема - это не технологический (в большинстве случаев), а, скорее, бизнес-решение - обычно это сводится к времени и деньгам.

Среднестатистический разработчик программного обеспечения не обучен тому, как эффективно использовать FM, и графики проекта (как правило) не таковы, что вы можете внедрить множество действий по моделированию, не влияя на сроки.

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

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

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

person John Carter    schedule 15.04.2020