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

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

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

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

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

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

В Российском государственном социальном университете рассмотрена проблема формулирования сложных верифицируемых свойств.

19.02.2016

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

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