=Paper=
{{Paper
|id=None
|storemode=property
|title=Insertion Modeling and its Applications
|pdfUrl=https://ceur-ws.org/Vol-716/ICTERI-2011-CEUR-WS-Invited-3-p-24-24.pdf
|volume=Vol-716
|dblpUrl=https://dblp.org/rec/conf/icteri/Letichevsky11
}}
==Insertion Modeling and its Applications==
<pdf width="1500px">https://ceur-ws.org/Vol-716/ICTERI-2011-CEUR-WS-Invited-3-p-24-24.pdf</pdf>
<pre>
       Insertion Modeling and its Applications

                         Alexander A. Letichevsky

       Glushkov Institute of Cybernetics, Academy of Sciences of Ukraine,
                                let@cyfra.net



Abstract: The talk describes insertion modeling methodology, its theory,
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. Both agents and environments are characterized by
their behaviors represented as the elements of continuous behavior algebra, a
kind of the ACP with approximation relation, but in addition each environment
is supplied by an insertion function, which takes the behavior of an agent and
the behavior of an environment as arguments and returns a new behavior of this
environment. Each agent can be considered as a transformer of environment
behaviors and a new kind of equivalence of agents weaker than bisimulation is
defined in terms of the algebra of behavior transformations. Arbitrary
continuous functions can be used as insertion functions and rewriting logic is
used to define computable ones. The theory has applications for studying
distributed computations, multi agent systems and semantics of specification
languages.
In applications to distributed system design we use Basic Protocol Specification
Language (BPSL) for the representation of requirement specifications of
distributed systems. The central notion of this language is the notion of basic
protocol – a sequencing diagram with pre- and postconditions represented as
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. 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.

</pre>