Хорошо известно, что методы формальных спецификаций позволяют [1, 2]:

• документировать и досконально описывать поведения систем;
• более детально анализировать и, следовательно, лучше понимать системы;
• облегчить проверку, обслуживание и развитие системы;
• сократить количество ошибок.

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

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

Рис. 1 – Относительная стоимость исправления дефектов [3]

Но всегда ли оправдываются усилия при формальной спецификации системы на ранних стадиях разработки? В работе [1] настаивается на том, что переход с неформальных требований к формальным спецификациям не следует делать слишком рано из-за того, что большая степень детализации усложняет спецификацию.

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

Такой же подход применяется при использовании UML (Unified Modeling Language, [4]) – унифицированного языка моделирования. Но этот язык семи – формален даже в случае аннотации моделей OCL-выражениями (Object Constraint Language, [5]), хотя, без сомнений, на сегодняшний день он является самым используемым в отрасли ИТ.

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

Литература

1. Heisel M., A pragmatic approach to formal specification, (Eds.) Haim Kilov, William Harvey, Object-Oriented Behavioral Specifications, Kluwer Academic Publishers, pp41-63, 1996;
2. Hall A., Realising the Benefits of Formal Methods, (Eds.) Kung-Kiu Lau, Richard Banach, Formal Methods and Software Engineering, LNCS 3785, Springer, pp1 – 4, 2005;
3. Schwalbe K., Information Technology Project Management, Cengage Learning, p180, 2009;
4. OMG, The Unified Modeling Language™ – UML, [www.uml.org]
5. OMG, Object Constraint Language – OCL, Available Specification, Version 2.0, 2006 [http://www.omg.org/spec/OCL/2.0/]