Insertion Modeling System

  • Alexander A. Letichevsky
  • Olexandr A. Letychevskyi
  • Vladimir S. Peschanenko
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7162)


The paper relates to practical aspects of insertion modeling. Insertion modeling system is an environment for the development of insertion machines, used to represent insertion models of distributed systems. The architecture of insertion machines and insertion modeling system IMS is presented. Insertion machine for program verification is specified as an example, and as a starting point of ‘verifiable programming’ project.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Gilbert, D.R., Letichevsky, A.A.: A universal interpreter for nondeterministic concurrent programming languages. In: Gabbrielli, M. (ed.) Fifth Compulog Network Area Meeting on Language Design and Semantic Analysis Methods (September 1996)Google Scholar
  2. 2.
    Letichevsky, A., Gilbert, D.: A general theory of action languages. Cybernetics and System Analyses 1 (1998)Google Scholar
  3. 3.
    Letichevsky, A., Gilbert, D.: A Model for Interaction of Agents and Environments. In: Bert, D., Choppy, C., Mosses, P.D. (eds.) WADT 1999. LNCS, vol. 1827, pp. 311–328. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  4. 4.
    Letichevsky, A.: Algebra of behavior transformations and its applications. In: Kudryavtsev, V.B., Rosenberg, I.G. (eds.) Structural Theory of Automata, Semigroups, and Universal Algebra. NATO Science Series II. Mathematics, Physics and Chemistry, vol. 207, pp. 241–272. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  5. 5.
    Baranov, S., Jervis, C., Kotlyarov, V., Letichevsky, A., Weigert, T.: Leveraging UML to Deliver Correct Telecom Applications. In: Lavagno, L., Martin, G., Selic, B. (eds.) UML for Real: Design of Embedded Real-Time Systems. Kluwer Academic Publishers, Amsterdam (2003)Google Scholar
  6. 6.
    Letichevsky, A., Kapitonova, J., Letichevsky Jr., A., Volkov, V., Baranov, S., Kotlyarov, V., Weigert, T.: Basic Protocols, Message Sequence Charts, and the Verification of Requirements Specifications. Computer Networks 47, 662–675 (2005)Google Scholar
  7. 7.
    Kapitonova, J., Letichevsky, A., Volkov, V., Weigert, T.: Validation of Embedded Systems. In: Zurawski, R. (ed.) The Embedded Systems Handbook. CRC Press, Miami (2005)Google Scholar
  8. 8.
    Letichevsky, A., Kapitonova, J., Volkov, V., Letichevsky Jr., A., Baranov, S., Kotlyarov, V., Weigert, T.: System Specification with Basic Protocols. Cybernetics and System Analyses 4 (2005)Google Scholar
  9. 9.
    Letichevsky, A., Kapitonova, J., Kotlyarov, V., Letichevsky Jr, A., Nikitchenko, N., Volkov, V., Weigert, T.: Insertion modeling in distributed system design. Problems of Programming 4, 13–39 (2008) ISSN 1727-4907Google Scholar
  10. 10.
    Milner, R.: Communication and Concurrency. Prentice Hall (1989)Google Scholar
  11. 11.
    Milner, R.: Communicating and Mobile Systems: the Pi Calculus. Cambridge University Press (1999)Google Scholar
  12. 12.
    Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall (1985)Google Scholar
  13. 13.
    Cardelli, L., Gordon, A.D.: Mobile Ambients. In: Nivat, M. (ed.) FOSSACS 1998. LNCS, vol. 1378, pp. 140–155. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  14. 14.
    Gurevich, Y.: Evolving Algebras 1993: Lipari Guide. In: Borger, E. (ed.) Specification and Validation Methods, pp. 9–36. Oxford University Press (1995) ISBN 0-19-853854-5Google Scholar
  15. 15.
    Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall International Series in Computer Science (1998) ISBN 0-13-458761-8. OCLC 38199961Google Scholar
  16. 16.
    Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96, 73–155 (1992)MathSciNetzbMATHCrossRefGoogle Scholar
  17. 17.
    Letichevsky, A., Kapitonova, J., Volkov, V., Vyshemirsky, V., Letichevsky Jr., A.: Insertion programming. Cybernetics and System Analyses 1 (2003)Google Scholar
  18. 18.
    Kapitonova, J.V., Letichevsky, A.A., Konozenko, S.V.: Computations in APS. Theoretical Computer Science 119, 145–171 (1993)MathSciNetzbMATHCrossRefGoogle Scholar
  19. 19.
  20. 20.
    Kozen, D., Harel, D., Tiuryn, J.: Dynamic Logic, p. 400 (2000)Google Scholar
  21. 21.
    Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM 12(10), 576–580, 583 (1969)zbMATHCrossRefGoogle Scholar
  22. 22.
    Floyd, R.W.: Assigning meanings to programs. In: Proceedings of the American Mathematical Society Symposia on Applied Mathematics, vol. 19, pp. 19–31 (1967)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Alexander A. Letichevsky
    • 1
  • Olexandr A. Letychevskyi
    • 1
  • Vladimir S. Peschanenko
    • 2
  1. 1.Glushkov Institute of CyberneticsAcademy of Sciences of UkraineUkraine
  2. 2.Kherson State UniversityUkraine

Personalised recommendations