Насколько формальны формальные методы?
В статье анализируются проблемы, связанные с развитием и внедрением формальных методов при разработке и верификации программного обеспечения и компьютерных систем. Дается классификация инвариантов. Уточняются понятие и процедура синтеза системы инвариантов и ее оптимизации по некоторым критериям. Пр...
Saved in:
| Published in: | Математичні машини і системи |
|---|---|
| Date: | 2011 |
| Main Authors: | , , |
| Format: | Article |
| Language: | Russian |
| Published: |
Інститут проблем математичних машин і систем НАН України
2011
|
| Subjects: | |
| Online Access: | https://nasplib.isofts.kiev.ua/handle/123456789/83406 |
| 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: | Насколько формальны формальные методы? / О.М. Тарасюк, А.В. Горбенко, В.С. Харченко // Мат. машини і системи. — 2011. — № 1. — С. 154-167. — Бібліогр.: 25 назв. — рос. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| id |
nasplib_isofts_kiev_ua-123456789-83406 |
|---|---|
| record_format |
dspace |
| spelling |
Тарасюк, О.М. Горбенко, А.В. Харченко, В.С. 2015-06-19T12:15:21Z 2015-06-19T12:15:21Z 2011 Насколько формальны формальные методы? / О.М. Тарасюк, А.В. Горбенко, В.С. Харченко // Мат. машини і системи. — 2011. — № 1. — С. 154-167. — Бібліогр.: 25 назв. — рос. 1028-9763 https://nasplib.isofts.kiev.ua/handle/123456789/83406 004.052 В статье анализируются проблемы, связанные с развитием и внедрением формальных методов при разработке и верификации программного обеспечения и компьютерных систем. Дается классификация инвариантов. Уточняются понятие и процедура синтеза системы инвариантов и ее оптимизации по некоторым критериям. Предлагаются модели жизненного цикла программного обеспечения при использовании формальных методов Event-B и Model Checking. Анализируются их особенности и ограничения. Формулируются направления дальнейших исследований в этой области. У статті аналізуються проблеми, пов'язані з розвитком та застосуванням формальних методів під час створення й верифікації програмного забезпечення та комп'ютерних систем. Дається класифікація інваріантів. Уточнюються поняття й процедура синтезу системи інваріантів та її оптимізація за певними критеріями. Розглянуто моделі життєвого циклу за умов використання формальних методів Event-B та Model Checking, їх особливості та обмеження. Сформульовано напрямки подальших досліджень у цій області. The paper analyses existing problems associated with the development and practical application of formal methods in the design and verification of software and computer systems. The classification of invariants is given in the paper. We specify a concept of the system of invariants and discuss a procedure of its synthesis and optimization. The changes in the software life cycle caused by applying formal methods Event-B and Model Checking are discussed. The directions of further research in this area are also given. ru Інститут проблем математичних машин і систем НАН України Математичні машини і системи Дискусійні повідомлення Насколько формальны формальные методы? Наскільки формальні формальні методи? How formal methods are formal? Article published earlier |
| institution |
Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| collection |
DSpace DC |
| title |
Насколько формальны формальные методы? |
| spellingShingle |
Насколько формальны формальные методы? Тарасюк, О.М. Горбенко, А.В. Харченко, В.С. Дискусійні повідомлення |
| title_short |
Насколько формальны формальные методы? |
| title_full |
Насколько формальны формальные методы? |
| title_fullStr |
Насколько формальны формальные методы? |
| title_full_unstemmed |
Насколько формальны формальные методы? |
| title_sort |
насколько формальны формальные методы? |
| author |
Тарасюк, О.М. Горбенко, А.В. Харченко, В.С. |
| author_facet |
Тарасюк, О.М. Горбенко, А.В. Харченко, В.С. |
| topic |
Дискусійні повідомлення |
| topic_facet |
Дискусійні повідомлення |
| publishDate |
2011 |
| language |
Russian |
| container_title |
Математичні машини і системи |
| publisher |
Інститут проблем математичних машин і систем НАН України |
| format |
Article |
| title_alt |
Наскільки формальні формальні методи? How formal methods are formal? |
| description |
В статье анализируются проблемы, связанные с развитием и внедрением формальных методов при разработке и верификации программного обеспечения и компьютерных систем. Дается классификация инвариантов. Уточняются понятие и процедура синтеза системы инвариантов и ее оптимизации по некоторым критериям. Предлагаются модели жизненного цикла программного обеспечения при использовании формальных методов Event-B и Model Checking. Анализируются их особенности и ограничения. Формулируются направления дальнейших исследований в этой области.
У статті аналізуються проблеми, пов'язані з розвитком та застосуванням формальних методів під час створення й верифікації програмного забезпечення та комп'ютерних систем. Дається класифікація інваріантів. Уточнюються поняття й процедура синтезу системи інваріантів та її оптимізація за певними критеріями. Розглянуто моделі життєвого циклу за умов використання формальних методів Event-B та Model Checking, їх особливості та обмеження. Сформульовано напрямки подальших досліджень у цій області.
The paper analyses existing problems associated with the development and practical application of formal methods in the design and verification of software and computer systems. The classification of invariants is given in the paper. We specify a concept of the system of invariants and discuss a procedure of its synthesis and optimization. The changes in the software life cycle caused by applying formal methods Event-B and Model Checking are discussed. The directions of further research in this area are also given.
|
| issn |
1028-9763 |
| url |
https://nasplib.isofts.kiev.ua/handle/123456789/83406 |
| citation_txt |
Насколько формальны формальные методы? / О.М. Тарасюк, А.В. Горбенко, В.С. Харченко // Мат. машини і системи. — 2011. — № 1. — С. 154-167. — Бібліогр.: 25 назв. — рос. |
| work_keys_str_mv |
AT tarasûkom naskolʹkoformalʹnyformalʹnyemetody AT gorbenkoav naskolʹkoformalʹnyformalʹnyemetody AT harčenkovs naskolʹkoformalʹnyformalʹnyemetody AT tarasûkom naskílʹkiformalʹníformalʹnímetodi AT gorbenkoav naskílʹkiformalʹníformalʹnímetodi AT harčenkovs naskílʹkiformalʹníformalʹnímetodi AT tarasûkom howformalmethodsareformal AT gorbenkoav howformalmethodsareformal AT harčenkovs howformalmethodsareformal |
| first_indexed |
2025-12-07T20:25:22Z |
| last_indexed |
2025-12-07T20:25:22Z |
| _version_ |
1850882520600543232 |