Верификация спецификаций в языке L относительно темпоральных свойств, не выразимых в этом языке
Розглянуто методи верифікації специфікацій реактивних алгоритмів у мові L. Верифікація здійснюється відносно властивостей, поданих у вигляді формул класу GR(1) темпоральної логіки LTL, і зводиться до перевірки виконуваності формул у мові L Verification methods for reactive algorithms specifications...
Saved in:
| Published in: | Кибернетика и системный анализ |
|---|---|
| Date: | 2009 |
| Main Author: | |
| Format: | Article |
| Language: | Russian |
| Published: |
Інститут кібернетики ім. В.М. Глушкова НАН України
2009
|
| Subjects: | |
| Online Access: | https://nasplib.isofts.kiev.ua/handle/123456789/44396 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Journal Title: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Cite this: | Верификация спецификаций в языке L относительно темпоральных свойств, не выразимых в этом языке / А.Н. Чеботарев // Кибернетика и системный анализ. — 2009. — № 5. — С. 3-12. — Бібліогр.: 8 назв. — рос. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| Summary: | Розглянуто методи верифікації специфікацій реактивних алгоритмів у мові 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.
|
|---|---|
| ISSN: | 0023-1274 |