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...
Gespeichert in:
| Datum: | 2008 |
|---|---|
| Hauptverfasser: | , , , , , , |
| Format: | Artikel |
| Sprache: | English |
| Veröffentlicht: |
Інститут програмних систем НАН України
2008
|
| Schlagworte: | |
| Online Zugang: | https://nasplib.isofts.kiev.ua/handle/123456789/2599 |
| 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: | 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 назв. — англ. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| id |
nasplib_isofts_kiev_ua-123456789-2599 |
|---|---|
| record_format |
dspace |
| spelling |
Letichevsky, A.A. Kapitonova, J.V. Letichevsky Jr, A.A. Kotlyarov, V.P. Nikitchenko, N.S. Volkov, V.A. Weigert, T. 2008-12-15T13:20:45Z 2008-12-15T13:20:45Z 2008 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 https://nasplib.isofts.kiev.ua/handle/123456789/2599 623/518.3/517.5 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 была успешно применена в большом количестве индустриальных проектов из разных областей, включая телекоммуникации, телематику и системы реального времени. en Інститут програмних систем НАН України Теоретичні та методологічні основи програмування Insertion modeling in distributed system design Інсерційне моделювання в проектуванні розподілених систем Insertion modeling in distributed system design Article published earlier |
| institution |
Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| collection |
DSpace DC |
| title |
Insertion modeling in distributed system design |
| spellingShingle |
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. Теоретичні та методологічні основи програмування |
| 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 |
| 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. |
| topic |
Теоретичні та методологічні основи програмування |
| topic_facet |
Теоретичні та методологічні основи програмування |
| publishDate |
2008 |
| language |
English |
| publisher |
Інститут програмних систем НАН України |
| format |
Article |
| title_alt |
Інсерційне моделювання в проектуванні розподілених систем Insertion modeling in distributed system design |
| issn |
1727-4907 |
| url |
https://nasplib.isofts.kiev.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 AT letichevskyaa ínsercíinemodelûvannâvproektuvannírozpodílenihsistem AT kapitonovajv ínsercíinemodelûvannâvproektuvannírozpodílenihsistem AT letichevskyjraa ínsercíinemodelûvannâvproektuvannírozpodílenihsistem AT kotlyarovvp ínsercíinemodelûvannâvproektuvannírozpodílenihsistem AT nikitchenkons ínsercíinemodelûvannâvproektuvannírozpodílenihsistem AT volkovva ínsercíinemodelûvannâvproektuvannírozpodílenihsistem AT weigertt ínsercíinemodelûvannâvproektuvannírozpodílenihsistem |
| first_indexed |
2025-12-07T15:31:39Z |
| last_indexed |
2025-12-07T15:31:39Z |
| _version_ |
1850864041814130688 |
| 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.----------------
Стаття описує методологію інсерційного моделювання, її реалізацію та застосування. Інсерційне моделювання являє собою методологію проектування розподілених систем, що управляється моделлю. Ця методологія базується на теорії взаємодіючих агентів та середовищ [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 была успешно применена в большом количестве индустриальных проектов из разных областей, включая телекоммуникации, телематику и системы реального времени.
|