Satisfiability For Symbolic Verification in VRS
Vernadsky National Library of Ukraine
Переглянути архів ІнформаціяПоле | Співвідношення | |
Title |
Satisfiability For Symbolic Verification in VRS
|
|
Creator |
Letichevsky, A.
Letichevskiy, A. Weigert, T. Peschanenko, V. |
|
Subject |
Информационные технологии и системы
|
|
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 замість логічного виводу у відповідних численнях для ефективного обчислення у предикатних трансформерах. |
|
Date |
2015-06-16T14:12:04Z
2015-06-16T14:12:04Z 2013 |
|
Type |
Article
|
|
Identifier |
Satisfiability For Symbolic Verification in VRS / A. Letichevsky, A. Letichevskyi, T. Weigert, V. Peschanenko // Управляющие системы и машины. — 2013. — № 3. — С. 81-87. — Бібліогр.: 26 назв. — англ.
0130-5395 http://dspace.nbuv.gov.ua/handle/123456789/83170 519.686.2 |
|
Language |
en
|
|
Relation |
Управляющие системы и машины
|
|
Publisher |
Міжнародний науково-навчальний центр інформаційних технологій і систем НАН та МОН України
|
|