Формальная верификация диаграммы классов
В статье описываются наиболее популярные из существующих подходов к верификации наиболее часто используемой UML-диаграммы - диаграммы классов. Указывается, что данные методы позволяют оценить ее корректность только в отдельных аспектах, и наиболее эффективным является комплексное применение данных м...
Saved in:
| Published in: | Математичні машини і системи |
|---|---|
| Date: | 2013 |
| Main Authors: | , |
| Format: | Article |
| Language: | Russian |
| Published: |
Інститут проблем математичних машин і систем НАН України
2013
|
| Subjects: | |
| Online Access: | https://nasplib.isofts.kiev.ua/handle/123456789/83837 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Journal Title: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Cite this: | Формальная верификация диаграммы классов / В.В. Литвинов, И.В. Богдан // Мат. машини і системи. — 2013. — № 2. — С. 41-47. — Бібліогр.: 6 назв. — рос. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1860236128307642368 |
|---|---|
| author | Литвинов, В.В. Богдан, И.В. |
| author_facet | Литвинов, В.В. Богдан, И.В. |
| citation_txt | Формальная верификация диаграммы классов / В.В. Литвинов, И.В. Богдан // Мат. машини і системи. — 2013. — № 2. — С. 41-47. — Бібліогр.: 6 назв. — рос. |
| collection | DSpace DC |
| container_title | Математичні машини і системи |
| description | В статье описываются наиболее популярные из существующих подходов к верификации наиболее часто используемой UML-диаграммы - диаграммы классов. Указывается, что данные методы позволяют оценить ее корректность только в отдельных аспектах, и наиболее эффективным является комплексное применение данных методов.
У статті описуються найбільш популярні серед існуючих підходів до проведення верифікації UML-діаграми, що використовується частіше за все - діаграми класів. Вказується, що дані методи дають можливість оцінити її коректність лише в окремих аспектах, і найбільш ефективним являється комплексне використання даних методів.
The article describes the most popular of the existing approaches to verification of the most frequently used UML-diagram – the class diagram. It is indicated that these methods allow us to estimate its correctness only in certain aspects and integrated application of these methods is considered to be the most effective.
|
| first_indexed | 2025-12-07T18:24:37Z |
| format | Article |
| fulltext |
© Литвинов В.В., Богдан И.В., 2013 41
ISSN 1028-9763. Математичні машини і системи, 2013, № 2
УДК 004.031.6
В.В. ЛИТВИНОВ*, И.В. БОГДАН**
ФОРМАЛЬНАЯ ВЕРИФИКАЦИЯ ДИАГРАММЫ КЛАССОВ
*
Черниговский государственный технологический университет, Чернигов, Украина
**
Черниговский государственный технологический университет, Чернигов, Украина
Анотація. У статті описуються найбільш популярні серед існуючих підходів до проведення вери-
фікації UML-діаграми, що використовується частіше за все – діаграми класів. Вказується, що да-
ні методи дають можливість оцінити її коректність лише в окремих аспектах, і найбільш ефек-
тивним являється комплексне використання даних методів.
Ключові слова: верифікація, шаблон, UML-діаграма, модель, коректність, діаграма класів.
Аннотация. В статье описываются наиболее популярные из существующих подходов к верифи-
кации наиболее часто используемой UML-диаграммы – диаграммы классов. Указывается, что
данные методы позволяют оценить ее корректность только в отдельных аспектах, и наиболее
эффективным является комплексное применение данных методов.
Ключевые слова: верификация, шаблон, UML-диаграмма, модель, корректность, диаграмма клас-
сов.
Abstract. The article describes the most popular of the existing approaches to verification of the most fre-
quently used UML-diagram – the class diagram. It is indicated that these methods allow us to estimate its
correctness only in certain aspects and integrated application of these methods is considered to be the
most effective.
Keywords: verification, pattern, UML-diagram, model, correctness, class diagram.
1. Введение
Формальная верификация программного обеспечения – это приемы и методы формального
доказательства (или опровержения) того, что модель программного обеспечения удовле-
творяет заданной формальной спецификации [1]. Для того, чтобы доказать формально ка-
кое-либо утверждение относительно работы реальной программы, анализируемое про-
граммное обеспечение должно быть представлено формальной моделью. Формальная мо-
дель обычно проще самой проверяемой программы. Это абстракция, в которой отражены
наиболее существенные характеристики программного обеспечения. Таким образом, про-
цесс создания любого программного обеспечения начинается с создания его модели, кото-
рой для эффективного дальнейшего использования необходимо пройти формальную вери-
фикацию.
Диаграмма классов является одной из основных составляющих модели любого про-
граммного обеспечения [2]. Именно поэтому особенно важное значение имеет верифика-
ция диаграмм классов. На данный момент существует достаточно большое количество
различных подходов к верификации диаграмм классов. Большинство из них позволяют
оценить корректность диаграммы классов с различной точки зрения.
2. Построение драйвера
Так, наиболее простым является подход, связанный с построением драйвера [3]. Данный
подход позволяет формально оценить правильность создания диаграммы классов и вы-
явить наиболее характерные ошибки. Прежде чем приступать к созданию драйвера, необ-
ходимо определить, следует ли выполнять верификацию каждого конкретного класса в ав-
тономном режиме, представляя его как отдельный модуль, или же необходимо восприни-
42 ISSN 1028-9763. Математичні машини і системи, 2013, № 2
мать класс как более крупный компонент системы. Решение принимается на основании
следующих факторов:
– роль данного класса в системе, в частности, степень связанного с ним риска;
– сложность класса, измеряемая количеством состояний, операций и связей с дру-
гими классами;
– объем трудозатрат, связанных с разработкой драйвера для верификации класса.
Если какой-либо класс должен стать частью некоторой библиотеки классов, то наи-
более оптимальной является всесторонняя верификация классов, причем, даже в том слу-
чае, если затраты на разработку драйвера окажутся высокими, поскольку очень важным
является его корректное функционирование.
Верификация классов из диаграммы классов чаще всего выполняется путем разра-
ботки драйвера, который создает экземпляры каждого класса и окружает эти классы соот-
ветствующей средой. Таким образом, становится возможным выполнение драйвера. Драй-
вер посылает одно или большее количество сообщений экземпляру класса в соответствии
со спецификацией тестового случая, затем проверяет исход этих сообщений на основании
значений ответа, изменения экземпляра и (или) один или большее число параметров сооб-
щения. В обязанности драйвера чаще всего входит удаление любого созданного им экзем-
пляра в том случае, если в языке программирования, таком как С++, имеет место управ-
ляемое программистом распределение памяти.
Если для конкретного класса характерны статические элементы данных и (или)
операции, то для них также необходимо выполнять верификацию. Такие элементы данных
и методы принадлежат самому классу, но не каждому экземпляру этого класса. Класс
можно рассматривать как объект. Например, в Java – это экземпляр класса Class.
Если поведение экземпляров класса базируется на значениях атрибутов уровня
класса, то все случаи, предназначенные для верификации этих атрибутов уровня класса,
должны рассматриваться как расширение состояний этих экземпляров.
Если между двумя и более классами на диаграмме классов присутствует связь «на-
следование» (обобщение), то драйверу необходимо проверить отсутствие множественного
наследования для языка Java, а также отсутствие двунаправленного наследования, при ко-
тором каждый из двух классов является и родительским, и дочерним одновременно для
всех объектно-ориентированных языков программирования.
Если между классом и интерфейсом на диаграмме классов присутствует связь «реа-
лизация», то драйверу необходимо проверить, реализует ли класс все те методы, сигнату-
ры которых указаны в интерфейсе.
Если в классе присутствует хотя бы один абстрактный метод, то драйверу необхо-
димо проверить, чтобы и класс был абстрактным.
3. Метод шаблонов
Еще одним подходом к верификации диаграммы классов является метод шаблонов. Дан-
ный метод предложила в 2004 году Мира Балабан [4]. Понятие шаблона в данном подходе
отличается от хорошо известного и понятного понятия шаблона проектирования, который
предоставляет собой формализованное описание часто встречающейся задачи проектиро-
вания, удачное решение данной задачи, а также рекомендации по применению этого реше-
ния в различных ситуациях. Шаблон, согласно методу Мира Балабан, напротив, является
примером ошибок при построении диаграммы классов.
Mira Balaban предложила несколько шаблонов.
Один из самых популярных шаблонов носит название Цикл множественной иерар-
хии (Multiplicity Hierarchy Cycle).
Согласно данному шаблону, если между двумя классами имеется связь «наследова-
ние» (обобщение), которая означает наличие между ними отношения один-к-одному или
ISSN 1028-9763. Математичні машини і системи, 2013, № 2 43
Рис. 1. Пример шаблона: Цикл
множественной иерархии
Рис. 2. Пример шаблона: Взаимодействие циклов
множественной иерархии
же несколько дочерних классов к одному родительскому классу, то и любая другая связь
между данными классами также должна указывать на наличие отношения один-к-одному
или же несколько дочерних классов к одному родительскому классу.
На рис. 1 представлен пример данного
шаблона – диаграмма классов, на которой
имеется класс Ученый и классы Кандидат на-
ук и Профессор, которые наследуются от
данного класса. Таким образом, класс Канди-
дат наук связан с классом Ученый отношени-
ем один-к-одному или же несколько объектов
класса Кандидат наук к одному классу объек-
та Ученый, точно так же класс Профессор
связан с классом Ученый отношением один-
к-одному или же несколько объектов класса
Профессор к одному классу объекта Ученый.
Но при этом класс Ученый связан с классом
Профессор ассоциативной связью в соотно-
шении: два объекта класса Ученый к одному классу объекта Профессор. Таким образом,
между двумя классами имеются две различные связи, одна из которых указывает на нали-
чие отношения: два объекта класса Ученый к одному классу объекта Профессор, а вторая
на наличие отношения: один-к-одному или же несколько объектов класса Профессор к од-
ному классу объекта Ученый, что противоречит друг другу и шаблону Цикл множествен-
ной иерархии.
Подразновидностью шаблона Цикл множественной иерархии является шаблон
Взаимодействие циклов множественной иерархии (Interaction of multiplicity and inter-
association hierarchy constraints).
Согласно данному шаблону, если между двумя классами имеется связь «наследова-
ние» (обобщение), которая означает наличие между ними отношения один-к-одному или
же несколько дочерних классов к одному родительскому классу, и каждый из них ассоциа-
тивно связан с третьим классом, то данные связи должны указывать на наличие одинако-
вых отношений.
На рис. 2 представлен
пример данного шаблона – диа-
грамма классов, на которой
представлен класс Ученый и
классы Кандидат наук и Про-
фессор, которые наследуются
от данного класса, а также
класс Читатель, который ассо-
циативно связан с классом
Ученый и классом Профессор.
Таким образом, класс Профес-
сор связан с классом Ученый
отношением один-к-одному, но
при этом он может быть связан с количеством от 2 до бесконечности объектами класса Чи-
татель. В то же время класс Ученый может быть связан с количеством от 1 до 3 объектов
класса Читатель. Так как отношения 1 и 1 со стороны классов Ученый и Профессор удов-
летворяют условию 1=1, но отношения 1...3 и 2..* со стороны класса Читатель не удовле-
творяют условию (1..3)=(2..*), то связи противоречат друг другу и шаблону Простой мно-
жественный цикл.
44 ISSN 1028-9763. Математичні машини і системи, 2013, № 2
Рис. 4. Простейшая диаграмма классов
Не менее популярный и часто встречаемый шаблон носит название Простой множе-
ственный цикл (Pure Multiplicity Cycle).
Согласно данному шаблону, если между двумя классами имеется несколько ассо-
циативных связей и каждая связь имеет свое отношение, то все отношения со стороны од-
ного и того же класса должны либо быть равными, либо же включать друг друга.
Рис. 3. Пример шаблона: Простой множественный цикл
На рис. 3 представлен пример данного шаблона – диаграмма классов, на которой
представлены три класса: класс Деканат, класс Преподаватель и класс Студент. Класс Де-
канат связан двумя «ассоциациями» с классом Преподаватель, причем в одной «ассоциа-
ции» от 0 до бесконечности объектов класса Деканат связаны с любым числом от 0 до бес-
конечности объектов класса Преподаватель, а во второй – от 1 до бесконечности объектов
класса Деканат связаны с 0 или 1 объектом класса Преподаватель. Так как отношения 0...*
и 1..* со стороны класса Деканат удовлетворяют условию (1..*) Є (0..*), и отношения 0...*
и 0..1 со стороны класса Преподаватель удовлетворяют условию (0..1) Є (0..*), то связи не
противоречат друг другу и шаблону Простой множественный цикл.
В то же время класс Преподаватель связан двумя «ассоциациями» с классом Сту-
дент, причем в одной «ассоциации» 1 объект класса Преподаватель связан с 1 объектом
класса Студент, а во второй – 1 объект класса Преподаватель связан с 3 объектами класса
Студент. Так как отношения 1 и 1 со стороны класса Преподаватель удовлетворяют усло-
вию 1=1, но отношения 1 и 3 со стороны класса Студент не удовлетворяют ни условию
1=3, ни условию 1 Є 3, то связи противоречат друг другу и шаблону Простой множест-
венный цикл.
4. Подход, основанный на построении идентификационного графа
Еще один подход к верификации диаграммы классов основан на построении идентифика-
ционного графа. Разработкой данного метода в период с 1990 по 2001 год занимались аме-
риканские ученые Hartmann, Lenzerini, Nobili и Thalheim [5].
Суть данного метода состоит в построении идентификационного графа, представ-
ляющего собой ориентированный граф. Узлами данного графа являются классы, а также
ассоциативные связи между ними, а дуги связывают ассоциации с теми классами, между
которыми на диаграмме классов и указаны соответствующие ассоциативные связи. В каче-
стве весов дуг используются отношения, которыми ассоциативно связаны классы. Как и в
обычном графе, в идентификационном графе вес пути вычисляется как произведение весов
всех дуг, входящих в состав данного пути.
Основным предназначением идентификационного графа является определение при-
чины нарушения конечной
выполнимости диаграммы
классов. Так же, как и ме-
тод шаблонов, данный ме-
тод позволяет выявить про-
тиворечивые связи, так на-
зываемые критические
ISSN 1028-9763. Математичні машини і системи, 2013, № 2 45
Рис. 5. Идентификационный граф для
диаграммы классов с рис. 4
Рис. 6. Пример использования метода
идентификационного графа
Рис. 7. Идентификационный граф для диаграммы
классов с рис. 6
циклы.
Суть данного метода представлена на рис. 4 и 5.
На рис. 4 представлена простейшая диаграмма классов с двумя классами: Class 1 и
Class 2, между которыми имеется ассоциативная связь С в отношении: от min1 до max1
объектов класса Class 1 связаны с количеством от min2 до max2 объектов класса Class 2.
Идентификационный граф для этой про-
стейшей диаграммы классов, построен-
ный согласно данному методу, представ-
лен на рис. 5. Граф имеет три узла: Class
1, Class 2 и С, а также четыре дуги, кото-
рые их связывают. Вес дуг слева направо
и сверху вниз составляет соответственно
max2, 1/min1, max1, 1/min2. Согласно
данному методу, критическим, указы-
вающим на нарушение конечной выпол-
нимости, является цикл, вес которого меньше 1. Таким образом, если
1)2min/1*1max*1min/1*2(max < , (1)
то «ассоциация» содержит нарушение конечной выполнимости.
На рис. 6 пред-
ставлен пример исполь-
зования метода иденти-
фикационного графа для
определения причины
нарушения конечной
выполнимости диаграм-
мы классов. На данной
диаграмме представле-
ны два класса: класс
Преподаватель и класс Студент, при-
чем от 1 до 5 объектов класса Препо-
даватель «ассоциацией» Информация
об успешности связаны с количеством
от 1 до 30 объектов класса Студент.
Идентификационный граф для данной
диаграммы классов представлен на
рис. 7.
Тогда, согласно данному мето-
ду, критический цикл для этого иден-
тификационного графа выглядит сле-
дующим образом:
1)1/1*5*1/1*30( > . (2)
Поэтому «ассоциация» не содержит нарушения конечной выполнимости.
5. Метод, основанный на представлении классов в качестве множеств
Еще один подход к верификации диаграммы классов основан на представлении класса в
качестве множества. Данный метод был предложен Calvanese и Lenzerini [6] и позволяет
оценить корректность прежде всего иерархий классов.
46 ISSN 1028-9763. Математичні машини і системи, 2013, № 2
Рис. 8. Диаграмма классов, представляющая собой
иерархию классов
Согласно данному методу, каждый класс, входящий в состав иерархии, представля-
ется в виде множества. Далее создается система неравенств, в которую включаются все
возможные неравенства и равенства, если такие имеются, между классами-множествами.
Затем необходимо решить сис-
тему неравенств и, если резуль-
татом станет не пустое под-
множество, то данная иерархия
классов построена корректно,
если же пустое множество, ие-
рархия классов не корректна.
На рис. 8 представлена
диаграмма классов, которая яв-
ляется иерархией классов. В
этой иерархии классы Роза, Ор-
хидея и Кактус наследуются от
класса Растение, в то же время
классы Роза и Орхидея насле-
дуются от класса Цветок, а
класс Цветок ассоциативно свя-
зан с классом Орхидея отноше-
нием один-к-одному. Таким об-
разом, к данной диаграмме мо-
жет быть применен метод множеств. Система неравенств для данной иерархии выглядит
следующим образом:
=
⊂
⊆∪
=∩∩
.||||
,
,
,0
ZO
ZO
ZOP
OPK
(3)
Последние два неравенства в данной системе противоречат друг другу, поэтому
решением данной системы неравенств является пустое множество и, согласно данному ме-
тоду, иерархия классов не корректна.
6. Выводы
В статье описано несколько наиболее часто используемых в верификации диаграмм клас-
сов. Все они позволяют оценить корректность диаграммы классов с разной точки зрения.
Так, метод, основанный на построении драйвера, позволяет выявить только наиболее ха-
рактерные ошибки на диаграмме. Метод шаблонов позволяет оценить корректность ассо-
циативных связей и связей типа «обобщение». Метод, связанный с построением иденти-
фикационного графа, позволяет оценить корректность исключительно ассоциативных свя-
зей. Метод, основанный на представлении классов в качестве множеств, позволяет оценить
корректность исключительно иерархий классов. Таким образом, наиболее эффективным
является комплексное использование данных методов.
СПИСОК ЛИТЕРАТУРЫ
1. OMG. Architecture Board ORMSC // Model Driven Architecture (MDA). – ormsc/2001-07-01, 2001. –
July 9. – 28 р.
ISSN 1028-9763. Математичні машини і системи, 2013, № 2 47
2. Буч Г. UML. Классика CS / Буч Г., Якобсон А., Рамбо Дж.; пер. с англ.; под общей ред. проф.
С. Орлова. – СПб.: Питер, 2006. – [2-е изд.]. – 736 с.
3. Макгрегор Дж. Тестирование объектно-ориентированного программного обеспечения: практ.
пособ. / Дж. Макгрегор, Д. Сайкс; пер. с англ. – К.: ООО «ТИД «ДС»», 2002. – 432 с.
4. Balaban М. Management of Correctness Problems in UML Class Diagrams – Towards a Pattern-based
Approach / М. Balaban, А. Maraee, А. Stur // Beer Sheva: Department of Computer Science, Ben-Gurion
University of the Negev. – 2002. – 33 р.
5. Fundamentals of Entity-Relationship Modeling / S. Hartmann, M. Lenzerini, P. Nobili [et al.] // Annals
Mathematics and Artificial Intelligence. – 1993. – N 7. – P. 197 – 256.
6. Calvanese D. On the Interaction between ISA and Cardinality Constraints / D. Calvanese, M. Lenzerini
// Proc. of the 10th IEEE International Conference on Data Engineering. – Houston, Texas, USA. IEEE
Computer Society. – Washington, DC, USA, 1994. – P. 204 – 213.
Стаття надійшла до редакції 26.03.2013
|
| id | nasplib_isofts_kiev_ua-123456789-83837 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 1028-9763 |
| language | Russian |
| last_indexed | 2025-12-07T18:24:37Z |
| publishDate | 2013 |
| publisher | Інститут проблем математичних машин і систем НАН України |
| record_format | dspace |
| spelling | Литвинов, В.В. Богдан, И.В. 2015-06-26T07:12:26Z 2015-06-26T07:12:26Z 2013 Формальная верификация диаграммы классов / В.В. Литвинов, И.В. Богдан // Мат. машини і системи. — 2013. — № 2. — С. 41-47. — Бібліогр.: 6 назв. — рос. 1028-9763 https://nasplib.isofts.kiev.ua/handle/123456789/83837 004.031.6 В статье описываются наиболее популярные из существующих подходов к верификации наиболее часто используемой UML-диаграммы - диаграммы классов. Указывается, что данные методы позволяют оценить ее корректность только в отдельных аспектах, и наиболее эффективным является комплексное применение данных методов. У статті описуються найбільш популярні серед існуючих підходів до проведення верифікації UML-діаграми, що використовується частіше за все - діаграми класів. Вказується, що дані методи дають можливість оцінити її коректність лише в окремих аспектах, і найбільш ефективним являється комплексне використання даних методів. The article describes the most popular of the existing approaches to verification of the most frequently used UML-diagram – the class diagram. It is indicated that these methods allow us to estimate its correctness only in certain aspects and integrated application of these methods is considered to be the most effective. ru Інститут проблем математичних машин і систем НАН України Математичні машини і системи Інформаційні і телекомунікаційні технології Формальная верификация диаграммы классов Формальна верифікація діаграми класів Formal verification of class diagram Article published earlier |
| spellingShingle | Формальная верификация диаграммы классов Литвинов, В.В. Богдан, И.В. Інформаційні і телекомунікаційні технології |
| title | Формальная верификация диаграммы классов |
| title_alt | Формальна верифікація діаграми класів Formal verification of class diagram |
| title_full | Формальная верификация диаграммы классов |
| title_fullStr | Формальная верификация диаграммы классов |
| title_full_unstemmed | Формальная верификация диаграммы классов |
| title_short | Формальная верификация диаграммы классов |
| title_sort | формальная верификация диаграммы классов |
| topic | Інформаційні і телекомунікаційні технології |
| topic_facet | Інформаційні і телекомунікаційні технології |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/83837 |
| work_keys_str_mv | AT litvinovvv formalʹnaâverifikaciâdiagrammyklassov AT bogdaniv formalʹnaâverifikaciâdiagrammyklassov AT litvinovvv formalʹnaverifíkacíâdíagramiklasív AT bogdaniv formalʹnaverifíkacíâdíagramiklasív AT litvinovvv formalverificationofclassdiagram AT bogdaniv formalverificationofclassdiagram |