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 deï¬ned in terms of the algebra of behavior transformations. Arbitrary continuous functions can be used as insertion functions and rewriting logic is used to deï¬ne computable ones. The theory has applications for studying distributed computations, multi agent systems and semantics of speciï¬cation 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. Prof Alexander Letichevsky is a member of the National Academy of Sciences of Ukraine, and is a famous computer scientist of the former Soviet Union. He graduated from Kiev State University in 1957 and till now works for Glushkov Institute of Cybernetics (before 1961 it was Computational Centre, then Institute of Cybernetics and from 1982 Glushkov Institute of Cybernetics) of the National Academy of Sciences of Ukraine.
Scientific interests of Prof Letichevsky were changing during his scientific life and include automata theory, theory of programming, formal methods in software and hardware design, computer algebra, automatic reasoning, parallel computation, and software verification.
Prof Letichevsky took part in many industrial projects including computers MIR with hardware implementation of high level programming languages, computer algebra system Analytic (1960), Macroconveyer computers (multiprocessor MIMD computing systems with distributed memory, 1980) and many other projects.
published on: 15th March 2011