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 |
| Автори: | , , , , , , |
| Формат: | Стаття |
| Мова: | 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| Резюме: | 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.---------------- |
|---|