Разработка методов и инструментальных средств верификации моделей объектно-ориентированных программ

Abstract

В работе сформулирована проблема нахождения ошибок в объектно- ориентированном программном обеспечении на максимально ранних этапах его создания и необходимости повышения качества программ в целом, что достигается прежде всего за счет выполнения верификации еще на этапе создания модели программного обеспечения. Так как в большинстве случаев модель объектно- ориентированного программного обеспечения представляется в виде множества UML-диаграмм, то были проанализированы существующие методы верификации UML-диаграмм, а также проведены исследования существующих инструментальных средств верификации, которые показали, что не существует ни инструментальных средств, ни методов верификации, которые бы позволили выявить все группы ошибок на UML-диаграммах. В результате была предложена собственная классификация ошибок на UML- диаграммах, что дало возможность определить какие именно группы ошибок не находят существующие методы и инструменты верификации, и модифицировать существующие или же предложить собственные методы. Предложен метод верификации диаграммы последовательности, который основан на представлении данной диаграммы в виде абстрактного цифрового автомата, и, в отличие от существующих методов верификации данной диаграммы, позволяет находить ошибки в ветвлениях на ней. Предложен метод верификации диаграммы последовательности, который основан на анализе отношения сущность-связь, и, в отличие от существующих, позволяет находить ошибки отправки синхронных сообщений и ошибки отправки сообщений не существующим объектам на данной диаграмме. Так, предложенный метод проверяет, что уничтожение или создание объектов, которые создаются на время выполнения своих действий, происходит корректно и для них предусмотрены явные сообщение. Также он проверяет выполняет ли объект-отправитель проверку предпосылок объекта-получателя, прежде чем отправлять заранее неприемлемо сообщения. Одновременно с этим проверяется, корректно объект-отправитель прекращает свою деятельность. Так, согласно определению синхронного сообщения действия отправителя блокируются до тех пор, пока он не получит ответ. Предложен метод верификации диаграммы компонентов, который основан на анализе отношения сущность-связь, и позволяет находить ошибки связи между компонентами на данной диаграмме. Усовершенствован путем введения новых ограничений существующий метод антипаттернов верификации диаграммы классов, что позволило находить ошибки в описаниях абстрактных классов и ошибки в описаниях вложенных классов на данной диаграмме. Так, доработанный метод выполняет проверку если в классе присутствует хотя бы один абстрактный метод, то чтобы и класс был абстрактным. Также если класс является вложенным, то данный метод выполняет проверку правильности описания вложенного класса. Усовершенствован путем введения новых ограничений являющийся одним из самых эффективных алгоритм Брона-Кербоша поиска клик на графах, что дало возможность использовать его при поиске особенных конструкций - антипаттернов на диаграммах классов. Для этого каждый антипаттерн был представлен в виде одной или нескольких клик на графе, где графом являлась вся диаграмма классов, а в сам алгоритм было добавлено новое условие, которое проверяет все имеющиеся на графе клики на совпадение с заданными. Разработана автоматизированная система верификации моделей объектно- ориентированного программного обеспечения, в которой комплексно используются существующие и предложенные подходы и методы верификации, что позволяет найти большее количество ошибок на UML-диаграммах.