Насколько формальны формальные методы?

В статье анализируются проблемы, связанные с развитием и внедрением формальных методов при разработке и верификации программного обеспечения и компьютерных систем. Дается классификация инвариантов. Уточняются понятие и процедура синтеза системы инвариантов и ее оптимизации по некоторым критериям. Пр...

Повний опис

Збережено в:
Бібліографічні деталі
Опубліковано в: :Математичні машини і системи
Дата:2011
Автори: Тарасюк, О.М., Горбенко, А.В., Харченко, В.С.
Формат: Стаття
Мова:Російська
Опубліковано: Інститут проблем математичних машин і систем НАН України 2011
Теми:
Онлайн доступ:https://nasplib.isofts.kiev.ua/handle/123456789/83406
Теги: Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
Назва журналу:Digital Library of Periodicals of National Academy of Sciences of Ukraine
Цитувати:Насколько формальны формальные методы? / О.М. Тарасюк, А.В. Горбенко, В.С. Харченко // Мат. машини і системи. — 2011. — № 1. — С. 154-167. — Бібліогр.: 25 назв. — рос.

Репозитарії

Digital Library of Periodicals of National Academy of Sciences of Ukraine
_version_ 1862742495003148288
author Тарасюк, О.М.
Горбенко, А.В.
Харченко, В.С.
author_facet Тарасюк, О.М.
Горбенко, А.В.
Харченко, В.С.
citation_txt Насколько формальны формальные методы? / О.М. Тарасюк, А.В. Горбенко, В.С. Харченко // Мат. машини і системи. — 2011. — № 1. — С. 154-167. — Бібліогр.: 25 назв. — рос.
collection DSpace DC
container_title Математичні машини і системи
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.
first_indexed 2025-12-07T20:25:22Z
format Article
fulltext
id nasplib_isofts_kiev_ua-123456789-83406
institution Digital Library of Periodicals of National Academy of Sciences of Ukraine
issn 1028-9763
language Russian
last_indexed 2025-12-07T20:25:22Z
publishDate 2011
publisher Інститут проблем математичних машин і систем НАН України
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
spellingShingle Насколько формальны формальные методы?
Тарасюк, О.М.
Горбенко, А.В.
Харченко, В.С.
Дискусійні повідомлення
title Насколько формальны формальные методы?
title_alt Наскільки формальні формальні методи?
How formal methods are formal?
title_full Насколько формальны формальные методы?
title_fullStr Насколько формальны формальные методы?
title_full_unstemmed Насколько формальны формальные методы?
title_short Насколько формальны формальные методы?
title_sort насколько формальны формальные методы?
topic Дискусійні повідомлення
topic_facet Дискусійні повідомлення
url https://nasplib.isofts.kiev.ua/handle/123456789/83406
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