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 гг. на сайте РИНЦ

Вход


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

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

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

4
Ожидается:
16 Декабря 2017

В Российском государственном социальном университете совместно с Московским технологическим университетом (МИРЭА) рассмотрена RLTL-нотация в качестве новой структуры данных для задания моделей систем.

03.05.2017

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

Технология процесса верификации программных и технических систем методом проверки на моделях подразумевает создание моделей систем, свойства которых требуется проверить. Так, например, модель системы может быть задана с помощью различных структур данных, в частности таких, как структура Крипке, язык асинхронных процессов Promela, в виде конечного автомата и т.д. Однако независимо от представления модели системы и верифицируемых свойств, заданных на базе логики линейного времени (LTL), необходим, как правило, процесс их преобразования к автоматам Бюхи. При этом алгоритмы преобразования формул LTL в автоматы Бюхи являются нетривиальными, а принципы их функционирования непонятны на интуитивном уровне.

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