Insertion modeling in distributed system design

Insertion modeling in distributed system design

The paper describes insertion modeling methodology, its implementation and applications. Insertion modeling is a methodology of model driven distributed system design. It is based on the model of interaction of agents and environments [1-2] and use Basic Protocol Specification Language (BPSL) for...

Повний опис

Збережено в:
Бібліографічні деталі
Видавець:Інститут програмних систем НАН України
Дата:2008
Автори: Letichevsky, A.A., Kapitonova, J.V., Letichevsky Jr, A.A., Kotlyarov, V.P., Nikitchenko, N.S., Volkov, V.A., Weigert, T.
Формат: Стаття
Мова:English
Опубліковано: Інститут програмних систем НАН України 2008
Теми:
Теоретичні та методологічні основи програмування
Онлайн доступ:http://dspace.nbuv.gov.ua/handle/123456789/2599
Теги: Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
Цитувати:Insertion modeling in distributed system design / A.A. Letichevsky, J.V. Kapitonova, V.P. Kotlyarov, A.A. Letichevsky Jr., N.S. Nikitchenko, V.A. Volkov, T. Weigert // Проблеми програмування. — 2008. — № 4. — С. 13-38. — Бібліогр.: 28 назв. — англ.

Репозиторії

Digital Library of Periodicals of National Academy of Sciences of Ukraine
id irk-123456789-2599
record_format dspace
institution Digital Library of Periodicals of National Academy of Sciences of Ukraine
collection DSpace DC
language English
topic Теоретичні та методологічні основи програмування
Теоретичні та методологічні основи програмування
spellingShingle Теоретичні та методологічні основи програмування
Теоретичні та методологічні основи програмування
Letichevsky, A.A.
Kapitonova, J.V.
Letichevsky Jr, A.A.
Kotlyarov, V.P.
Nikitchenko, N.S.
Volkov, V.A.
Weigert, T.
Insertion modeling in distributed system design
description The paper describes insertion modeling methodology, its implementation and applications. Insertion modeling is a methodology of model driven distributed system design. It is based on the model of interaction of agents and environments [1-2] and use Basic Protocol Specification Language (BPSL) for the representation of requirement specifications of distributed systems [3-6]. The central notion of this language is the notion of basic protocol – a sequencing diagram with pre- and postconditions, logic formulas interpreted by environment description. Semantics of BPSL allows concrete and abstract models on different levels of abstraction. Models defined by Basic Protocol Specifications (BPS) can be used for verification of requirement specifications as well as for generation of test cases for testing products, developed on the basis of BPS. Insertion modeling is supported by the system VRS (Verification of Requirement Specifications), developed for Motorola by Kiev VRS group in cooperation with Motorola GSG Russia. The system provides static requirement checking on the base of automatic theorem proving, symbolic and deductive model checking, and generation of traces for testing with different coverage criteria. All tools have been developed on a base of formal semantics of BPSL constructed according to insertion modeling methodology. The VRS has been successfully applied to a number of industrial projects from different domains including Telecommunications, Telematics and real time applications.----------------
format Article
author Letichevsky, A.A.
Kapitonova, J.V.
Letichevsky Jr, A.A.
Kotlyarov, V.P.
Nikitchenko, N.S.
Volkov, V.A.
Weigert, T.
author_facet Letichevsky, A.A.
Kapitonova, J.V.
Letichevsky Jr, A.A.
Kotlyarov, V.P.
Nikitchenko, N.S.
Volkov, V.A.
Weigert, T.
author_sort Letichevsky, A.A.
title Insertion modeling in distributed system design
title_short Insertion modeling in distributed system design
title_full Insertion modeling in distributed system design
title_fullStr Insertion modeling in distributed system design
title_full_unstemmed Insertion modeling in distributed system design
title_sort insertion modeling in distributed system design
publisher Інститут програмних систем НАН України
publishDate 2008
topic_facet Теоретичні та методологічні основи програмування
url http://dspace.nbuv.gov.ua/handle/123456789/2599
citation_txt Insertion modeling in distributed system design / A.A. Letichevsky, J.V. Kapitonova, V.P. Kotlyarov, A.A. Letichevsky Jr., N.S. Nikitchenko, V.A. Volkov, T. Weigert // Проблеми програмування. — 2008. — № 4. — С. 13-38. — Бібліогр.: 28 назв. — англ.
work_keys_str_mv AT letichevskyaa insertionmodelingindistributedsystemdesign
AT kapitonovajv insertionmodelingindistributedsystemdesign
AT letichevskyjraa insertionmodelingindistributedsystemdesign
AT kotlyarovvp insertionmodelingindistributedsystemdesign
AT nikitchenkons insertionmodelingindistributedsystemdesign
AT volkovva insertionmodelingindistributedsystemdesign
AT weigertt insertionmodelingindistributedsystemdesign
first_indexed 2023-03-24T08:25:23Z
last_indexed 2023-03-24T08:25:23Z
_version_ 1796139002292600832
spelling irk-123456789-25992009-01-14T12:00:15Z Insertion modeling in distributed system design Letichevsky, A.A. Kapitonova, J.V. Letichevsky Jr, A.A. Kotlyarov, V.P. Nikitchenko, N.S. Volkov, V.A. Weigert, T. Теоретичні та методологічні основи програмування The paper describes insertion modeling methodology, its implementation and applications. Insertion modeling is a methodology of model driven distributed system design. It is based on the model of interaction of agents and environments [1-2] and use Basic Protocol Specification Language (BPSL) for the representation of requirement specifications of distributed systems [3-6]. The central notion of this language is the notion of basic protocol – a sequencing diagram with pre- and postconditions, logic formulas interpreted by environment description. Semantics of BPSL allows concrete and abstract models on different levels of abstraction. Models defined by Basic Protocol Specifications (BPS) can be used for verification of requirement specifications as well as for generation of test cases for testing products, developed on the basis of BPS. Insertion modeling is supported by the system VRS (Verification of Requirement Specifications), developed for Motorola by Kiev VRS group in cooperation with Motorola GSG Russia. The system provides static requirement checking on the base of automatic theorem proving, symbolic and deductive model checking, and generation of traces for testing with different coverage criteria. All tools have been developed on a base of formal semantics of BPSL constructed according to insertion modeling methodology. The VRS has been successfully applied to a number of industrial projects from different domains including Telecommunications, Telematics and real time applications.---------------- Стаття описує методологію інсерційного моделювання, її реалізацію та застосування. Інсерційне моделювання являє собою методологію проектування розподілених систем, що управляється моделлю. Ця методологія базується на теорії взаємодіючих агентів та середовищ [1-2] та використовує Basic Protocol Specification Language (BPSL) для представлення специфікацій вимог до розподілених систем. [3-6]. Діаграма Послідовності з пре- та постумовами (логічними формулами, що інтерпретуються відповідно до опису середовища) – Базовий Протокол є центральним поняттям цієї мови. Семантика BPSL дозволяє конкретні та абстракті моделі рівних рівнів абстрактності. Моделі визначені як Basic Protocol Specifications (BPS) можуть у подальшому бути використані як для верифікація специфікацій вимог та і для генерації тестових наборів. Інсерційне моделювання підтримується системою VRS (Verification of Requirement Specifications), створеною для компанії Моторола київською групою VRS у співробітництві із ЗАТ Моторола-Санкт-Петербург. Система дозволяє статичний аналіз вимог на основі автоматичного доведення теорем, символьної та дедуктивної перевірки моделей та породження трас для тестування із заданими критеріями покриття. Всі засоби були розроблені на базі формальної семантики BPSL, побудованої відповідно до методології інсерційного моделювання VRS була успішно застосована у великій кількості індустріальних проектів із різних галузей, включаючи телекомунікації, телематику та системи реального часу.---------------- Статья описывает методологию инсерционного моделирования, ее реализацию и применения. Инсерционное моделирование представляет собой методологию проектирования распределенных систем, управляемых[ моделью. Эта методология базируется на теории взаимодействующих агентов и сред [1-2] и использует Basic Protocol Specification Language (BPSL) для представления спецификаций требований к распределенным системам. [3-6]. Диаграма Последовательности с пред- и пост-условиями (логическими формулами, интерпретируемыми соответственно описания среды), называемая Базовый Протокол, – центральное понятие этого языка. Семантика BPSL позволяет конкретные и абстрактные модели разных уровней абстрактности. Модели заданные Basic Protocol Specifications (BPS) могут в дальнейшем быть использованы как для верификации спецификаций требований так и для генерации тестовых наборов. Инсерционное моделирование поддерживается системой VRS (Verification of Requirement Specifications), созданной для компании Моторола киевской группой VRS в сотрудничестве с ЗАО Моторола-Санкт-Петербург. Система позволяет статический анализ требований на основе автоматического доказательства теорем, символьной и дедуктивной проверки моделей и порождения трасс для тестирования с заданными критериями покрытия. Всеі средства были разработаны на базе формальной семантики BPSL, построенной соответственно методологии инсерционного моделирования. VRS была успешно применена в большом количестве индустриальных проектов из разных областей, включая телекоммуникации, телематику и системы реального времени. 2008 Article Insertion modeling in distributed system design / A.A. Letichevsky, J.V. Kapitonova, V.P. Kotlyarov, A.A. Letichevsky Jr., N.S. Nikitchenko, V.A. Volkov, T. Weigert // Проблеми програмування. — 2008. — № 4. — С. 13-38. — Бібліогр.: 28 назв. — англ. 1727-4907 http://dspace.nbuv.gov.ua/handle/123456789/2599 623/518.3/517.5 en Інститут програмних систем НАН України

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