На правах рекламы:
ISSN 0236-235X (P)
ISSN 2311-2735 (E)

Авторитетность издания

ВАК - К1
RSCI, ядро РИНЦ

Добавить в закладки

Следующий номер на сайте

2
Ожидается:
16 Июня 2024

В Российском государственном социальном университете рассматривалась реализация алгоритма верификации метода Model Checking для формул логики линейного времени LTL на базе новой нотации RLTL.

15.11.2017

Новый алгоритм верификации для метода Model Checking на базе нотации RLTL для верификации формул логики линейного времени во многом схож с алгоритмом верификации формул LTL, поскольку использует аналогичные принципы и подход к решению задачи верификации. Однако он имеет особенность – позволяет сократить число подготовительных этапов, необходимых для верификации, тем самым способствуя повышению производительности метода.

Работа предложенного алгоритма подробно рассмотрена на конкретных примерах с описанием всех этапов и их теоретической базы. Он может выступить в качестве более производительной альтернативы существующему, а RLTL-нотация может использоваться в качестве основной структуры данных, на базе которой будут задаваться как модели верифицируемых систем, так и требования к ним. В целом же такой подход должен способствовать общему повышению быстродействия метода Model Checking за счет снижения сложности алгоритма верификации и использования единой структуры данных.

Подробное описание дается в статье «Верификация моделей систем на базе эквациональной характеристики формул LTL», авторы: Кораблин Ю.П., Кочергин А.С., Шипов А.А. (Российский государственный социальный университет, Москва).