Satisfiability For Symbolic Verification in VRS
Рассмотрены использование логики первого порядка в символьной верификации спецификаций требований программного обеспечения, символьные модели систем, которые есть транзиционными системами с символьными состояниями представленных формулой логики первого порядка. Использованы методы Satisfiability Mod...
Gespeichert in:
| Veröffentlicht in: | Управляющие системы и машины |
|---|---|
| Datum: | 2013 |
| Hauptverfasser: | , , , |
| Format: | Artikel |
| Sprache: | Englisch |
| Veröffentlicht: |
Міжнародний науково-навчальний центр інформаційних технологій і систем НАН та МОН України
2013
|
| Schlagworte: | |
| Online Zugang: | https://nasplib.isofts.kiev.ua/handle/123456789/83170 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Zitieren: | Satisfiability For Symbolic Verification in VRS / A. Letichevsky, A. Letichevskyi, T. Weigert, V. Peschanenko // Управляющие системы и машины. — 2013. — № 3. — С. 81-87. — Бібліогр.: 26 назв. — англ. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1862714463245828096 |
|---|---|
| author | Letichevsky, A. Letichevskyi, A. Weigert, T. Peschanenko, V. |
| author_facet | Letichevsky, A. Letichevskyi, A. Weigert, T. Peschanenko, V. |
| citation_txt | Satisfiability For Symbolic Verification in VRS / A. Letichevsky, A. Letichevskyi, T. Weigert, V. Peschanenko // Управляющие системы и машины. — 2013. — № 3. — С. 81-87. — Бібліогр.: 26 назв. — англ. |
| collection | DSpace DC |
| container_title | Управляющие системы и машины |
| 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 замість логічного виводу у відповідних численнях для ефективного обчислення у предикатних трансформерах.
|
| first_indexed | 2025-12-07T17:50:43Z |
| format | Article |
| fulltext | |
| id | nasplib_isofts_kiev_ua-123456789-83170 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 0130-5395 |
| language | English |
| last_indexed | 2025-12-07T17:50:43Z |
| publishDate | 2013 |
| publisher | Міжнародний науково-навчальний центр інформаційних технологій і систем НАН та МОН України |
| 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 |
| spellingShingle | Satisfiability For Symbolic Verification in VRS Letichevsky, A. Letichevskyi, A. Weigert, T. Peschanenko, V. Информационные технологии и системы |
| title | Satisfiability For Symbolic Verification in VRS |
| title_alt | Выполнимость для символьной верификации VRS Здійсненість для символьної верифікації 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_short | Satisfiability For Symbolic Verification in VRS |
| title_sort | satisfiability for symbolic verification in vrs |
| topic | Информационные технологии и системы |
| topic_facet | Информационные технологии и системы |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/83170 |
| 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 |