Приемы описания модели управления доступом ОССН Astra Linux Special Edition на формализованном языке метода Event-B для обеспечения ее верификации инструментами Rodin и ProB

doi:10.17223/20710410/52/5

Эндаумент фонд ТГУ!
Впиши своё имя в историю университета
- Сделать пожертвование -

Add to "Quick Collection"

Description	Size	Format
Приемы описания модели управления доступом OCCH Astra Linux Special Edition на формализованном языке метода Event-B для обеспечения её верификации инструментами Rodin и ProB	1 MB	Adobe Acrobat PDF	Read	Download
DOI Доступ к ресурсу на сайте издателя			10.17223/20710410/52/5

#модель управления доступом

#дедуктивная верификация

#метод проверки моделей

Title: Приемы описания модели управления доступом ОССН Astra Linux Special Edition на формализованном языке метода Event-B для обеспечения ее верификации инструментами Rodin и ProB
Title: The techniques of formalization of OS Astra linux special edition access control model using Event-B formal method for verification using Rodin and ProB
Creator: Девянин, Петр Николаевич
|
Леонова, Мария Александровна
Date: 2021
DOI: 10.17223/20710410/52/5
Description: Рассматриваются приёмы по доработке описания модели управления доступом отечественной защищённой операционной системы специального назначения Astra Linux Special Edition (МРОСЛ ДП-модели) в формализованной нотации (на формализованном языке метода Event-B), основанные на использовании нескольких глобальных типов, разделении общих тотальных функций на частные тотальные функции и сокращении числа инвариантов и охранных условий событий, предполагающих перебор подмножеств некоторого множества. Результатом их применения стало упрощение автоматизированной дедуктивной верификации модели с применением инструмента Rodin и её адаптация к верификации с использованием инструмента проверки моделей ProB. Данные приёмы могут быть полезны при разработке других моделей управления доступом и их верификации с применением соответствующих инструментов.

Relationships: Show Relationship Browser for this Object
collection(s): Журналы ТГУ
Identifier: смотреть в электронном каталоге НБ ТГУ
Type: статьи в журналах
Source: Прикладная дискретная математика. 2021. № 52. С. 83-96
Language: rus

Created: 30-08-2021

619 Visitors

399 Hits

242 Downloads

Журналы ТГУ Приемы описания модели управления доступом ОССН Astra Linux Special Edition на формализованном языке метода Event-B для обеспечения ее верификации инструментами Rodin и ProB