Рассматривается проблема включения метода формальной верификации - проверки модели - в процесс проектирования сложных распределенных программных систем. В качестве центрального объекта проектирования предлагается использовать платформенно-независимую модель, которая строится на основе ядра системы, отвечающего за логическое управление всей системой как единым целым. Подход позволяет повысить качество разрабатываемого программного обеспечения и гарантировать соответствие задаваемой спецификации. Предлагаемая методика опробована на реальной системе управления энергоснабжением судна.
We consider a problem of integrating a formal method of verification (model checking) into the process of designing complex distributed software systems to improve the quality of software. We use an approach based on the Model-Driven Engineering. It allows us to structure the design process by selecting and verifying a system core, consisting of independent subsystems and being responsible for logical management of the entire system as a whole. The proposed method was tested on a real control system of vessel power supply.
The authors declare that there are no conflicts of interest present.