Satisfiability For Symbolic Verification in VRS

Satisfiability For Symbolic Verification in VRS

Рассмотрены использование логики первого порядка в символьной верификации спецификаций требований программного обеспечения, символьные модели систем, которые есть транзиционными системами с символьными состояниями представленных формулой логики первого порядка. Использованы методы Satisfiability Mod...

Повний опис

Збережено в:
Бібліографічні деталі
Опубліковано в: :Управляющие системы и машины
Дата:2013
Автори: Letichevsky, A., Letichevskyi, A., Weigert, T., Peschanenko, V.
Формат: Стаття
Мова:English
Опубліковано: Міжнародний науково-навчальний центр інформаційних технологій і систем НАН та МОН України 2013
Теми:
Информационные технологии и системы
Онлайн доступ:https://nasplib.isofts.kiev.ua/handle/123456789/83170
Теги: Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
Назва журналу:Digital Library of Periodicals of National Academy of Sciences of Ukraine
Цитувати:Satisfiability For Symbolic Verification in VRS / A. Letichevsky, A. Letichevskyi, T. Weigert, V. Peschanenko // Управляющие системы и машины. — 2013. — № 3. — С. 81-87. — Бібліогр.: 26 назв. — англ.

Репозитарії

Digital Library of Periodicals of National Academy of Sciences of Ukraine
id nasplib_isofts_kiev_ua-123456789-83170
record_format dspace
spelling Letichevsky, A.
Letichevskyi, A.
Weigert, T.
Peschanenko, V.
2015-06-16T14:12:04Z
2015-06-16T14:12:04Z
2013
Satisfiability For Symbolic Verification in VRS / A. Letichevsky, A. Letichevskyi, T. Weigert, V. Peschanenko // Управляющие системы и машины. — 2013. — № 3. — С. 81-87. — Бібліогр.: 26 назв. — англ.
0130-5395
https://nasplib.isofts.kiev.ua/handle/123456789/83170
519.686.2
Рассмотрены использование логики первого порядка в символьной верификации спецификаций требований программного обеспечения, символьные модели систем, которые есть транзиционными системами с символьными состояниями представленных формулой логики первого порядка. Использованы методы Satisfiability Modulo Theory вместо логического вывода в соответствующем исчислении для эффективных вычислений в предикатных трансформерах.
This paper demonstrates the use of the first order logic in symbolic verification of the requirement specifications of reactive software systems. We consider symbolic models of a specified system which are transition systems with symbolic states represented by formulae of the first order logic. To efficiently compute predicate transformers the Satisfiability Modulo Theory methods are used instead of the logical inference in the corresponding calculi.
Розглянуто використання логіки першого порядку у символьній верифікації специфікацій вимог програмного забезпечення, символьні моделі систем, які є транзиційними системами з символьними станами представленими формулою логіки першого порядку. Використано методи Satisfiability Modulo Theory замість логічного виводу у відповідних численнях для ефективного обчислення у предикатних трансформерах.
en
Міжнародний науково-навчальний центр інформаційних технологій і систем НАН та МОН України
Управляющие системы и машины
Информационные технологии и системы
Satisfiability For Symbolic Verification in VRS
Выполнимость для символьной верификации VRS
Здійсненість для символьної верифікації VRS
Article
published earlier
institution Digital Library of Periodicals of National Academy of Sciences of Ukraine
collection DSpace DC
title Satisfiability For Symbolic Verification in VRS
spellingShingle Satisfiability For Symbolic Verification in VRS
Letichevsky, A.
Letichevskyi, A.
Weigert, T.
Peschanenko, V.
Информационные технологии и системы
title_short Satisfiability For Symbolic Verification in VRS
title_full Satisfiability For Symbolic Verification in VRS
title_fullStr Satisfiability For Symbolic Verification in VRS
title_full_unstemmed Satisfiability For Symbolic Verification in VRS
title_sort satisfiability for symbolic verification in vrs
author Letichevsky, A.
Letichevskyi, A.
Weigert, T.
Peschanenko, V.
author_facet Letichevsky, A.
Letichevskyi, A.
Weigert, T.
Peschanenko, V.
topic Информационные технологии и системы
topic_facet Информационные технологии и системы
publishDate 2013
language English
container_title Управляющие системы и машины
publisher Міжнародний науково-навчальний центр інформаційних технологій і систем НАН та МОН України
format Article
title_alt Выполнимость для символьной верификации VRS
Здійсненість для символьної верифікації VRS
description Рассмотрены использование логики первого порядка в символьной верификации спецификаций требований программного обеспечения, символьные модели систем, которые есть транзиционными системами с символьными состояниями представленных формулой логики первого порядка. Использованы методы Satisfiability Modulo Theory вместо логического вывода в соответствующем исчислении для эффективных вычислений в предикатных трансформерах. This paper demonstrates the use of the first order logic in symbolic verification of the requirement specifications of reactive software systems. We consider symbolic models of a specified system which are transition systems with symbolic states represented by formulae of the first order logic. To efficiently compute predicate transformers the Satisfiability Modulo Theory methods are used instead of the logical inference in the corresponding calculi. Розглянуто використання логіки першого порядку у символьній верифікації специфікацій вимог програмного забезпечення, символьні моделі систем, які є транзиційними системами з символьними станами представленими формулою логіки першого порядку. Використано методи Satisfiability Modulo Theory замість логічного виводу у відповідних численнях для ефективного обчислення у предикатних трансформерах.
issn 0130-5395
url https://nasplib.isofts.kiev.ua/handle/123456789/83170
citation_txt Satisfiability For Symbolic Verification in VRS / A. Letichevsky, A. Letichevskyi, T. Weigert, V. Peschanenko // Управляющие системы и машины. — 2013. — № 3. — С. 81-87. — Бібліогр.: 26 назв. — англ.
work_keys_str_mv AT letichevskya satisfiabilityforsymbolicverificationinvrs
AT letichevskyia satisfiabilityforsymbolicverificationinvrs
AT weigertt satisfiabilityforsymbolicverificationinvrs
AT peschanenkov satisfiabilityforsymbolicverificationinvrs
AT letichevskya vypolnimostʹdlâsimvolʹnoiverifikaciivrs
AT letichevskyia vypolnimostʹdlâsimvolʹnoiverifikaciivrs
AT weigertt vypolnimostʹdlâsimvolʹnoiverifikaciivrs
AT peschanenkov vypolnimostʹdlâsimvolʹnoiverifikaciivrs
AT letichevskya zdíisnenístʹdlâsimvolʹnoíverifíkacíívrs
AT letichevskyia zdíisnenístʹdlâsimvolʹnoíverifíkacíívrs
AT weigertt zdíisnenístʹdlâsimvolʹnoíverifíkacíívrs
AT peschanenkov zdíisnenístʹdlâsimvolʹnoíverifíkacíívrs
first_indexed 2025-12-07T17:50:43Z
last_indexed 2025-12-07T17:50:43Z
_version_ 1850872790938288128

Схожі ресурси