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