Insertion modeling in distributed system design

• Datum: 2026
• Hauptverfasser: Letichevsky, A.A., Kapitonova, J.V., Kotlyarov, V.P., Letichevsky Jr., A.A., Nikitchenko, N.S., Volkov, V.A., Weigert, T.
• Format: Artikel
• Sprache: Englisch
• Veröffentlicht: PROBLEMS IN PROGRAMMING 2026
• Schlagworte: UDC 623/518.3/517.5
• Online Zugang: https://pp.isofts.kiev.ua/index.php/ojs1/article/view/1013
• Назва журналу: Problems in programming

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.Problems in programming 2008; 4: 13-38