ISSN 0236-235X (P)
ISSN 2311-2735 (E)

Публикационная активность

(сведения по итогам 2016 г.)
2-летний импакт-фактор РИНЦ: 0,493
2-летний импакт-фактор РИНЦ без самоцитирования: 0,389
Двухлетний импакт-фактор РИНЦ с учетом цитирования из всех
источников: 0,732
5-летний импакт-фактор РИНЦ: 0,364
5-летний импакт-фактор РИНЦ без самоцитирования: 0,303
Суммарное число цитирований журнала в РИНЦ: 5022
Пятилетний индекс Херфиндаля по цитирующим журналам: 355
Индекс Херфиндаля по организациям авторов: 499
Десятилетний индекс Хирша: 11
Место в общем рейтинге SCIENCE INDEX за 2016 год: 304
Место в рейтинге SCIENCE INDEX за 2016 год по тематике "Автоматика. Вычислительная техника": 11

Больше данных по публикационной активности нашего журнале за 2008-2016 гг. на сайте РИНЦ

Вход


Забыли пароль? / Регистрация

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

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

1
Ожидается:
16 Марта 2018

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

15.11.2017

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

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

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