Верификация спецификаций в языке L относительно темпоральных свойств, не выразимых в этом языке

Домашня сторінка
→
Фізико-технічні та математичні науки
→
Відділення інформатики
→
Кибернетика и системный анализ
→
Кибернетика и системный анализ, 2009, том 45
→
Кибернетика и системный анализ, 2009, № 5
→
Переглянути статтю

Верификация спецификаций в языке L относительно темпоральных свойств, не выразимых в этом языке

Інші назви: Верифікація специфікацій у мові L відносно темпоральних властивостей, які не можуть бути специфікованими цією мовою
Verifying specifications in the language L against temporal properties non-expressible in this language

Тема: Кибернетика

УДК: 519.713.1

URI: http://dspace.nbuv.gov.ua/handle/123456789/44396

Посилання: Верификация спецификаций в языке L относительно темпоральных свойств, не выразимых в этом языке / А.Н. Чеботарев // Кибернетика и системный анализ. — 2009. — № 5. — С. 3-12. — Бібліогр.: 8 назв. — рос.

Дата: 2009

Завантажень: 396

Верификация спецификаций в языке L относительно темпоральных свойств, не выразимых в этом языке

Анотація:

Розглянуто методи верифікації специфікацій реактивних алгоритмів у мові L. Верифікація здійснюється відносно властивостей, поданих у вигляді формул класу GR(1) темпоральної логіки LTL, і зводиться до перевірки виконуваності формул у мові L

Verification methods for reactive algorithms specifications in the language L are considered. The verification is performed with respect to properties expressed in the GR(1) class of the temporal logic LTL and is reduced to checking the satisfiability of formulas in the language L.

Показати повний запис статті