Skip to main content
SpringerLink
Log in

Insertion Modeling and Symbolic Verification of Large Systems

  • Conference paper
  • First Online:
SDL 2015: Model-Driven Engineering for Smart Cities (SDL 2015)

Part of the book series: Lecture Notes in Computer Science ((LNCCN,volume 9369))

Included in the following conference series:

Abstract

Insertion modeling has been developed over the last decade as an approach to a general theory of interaction between agents and an environment in complex distributed multiagent systems. The original work in this direction proposed a model of interaction between agents and environments based on an insertion function and the algebra of behaviors (similar to process algebra). Over the recent years, insertion modeling has been applied to the verification of requirement specifications of distributed interacting systems and to the generation of tests from such requirements. Our system, VRS (Verification of Requirements Specifications), has successfully verified specifications in the field of telecommunication systems, embedded systems, and real-time systems. Formal requirements in VRS are presented by means of local descriptions with a succession relation. Formalized requirements are represented in a formalism that combines logical specifications with control descriptions provided by the graphical syntax of UCM (Use Case Map) diagrams. This paper overviews the main concepts of insertion modeling, presents new algorithms developed for symbolic verification, especially a new predicate transformer for local descriptions, and provides a formal description of the method of generating traces from such specifications (which is the key technology used to verify requirements and derive test suites).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Baranov, S., Jervis, C., Kotlyarov, V.P., Letichevsky, A.A., Weigert, T.: Leveraging UML to deliver correct telecom applications in UML for real. In: Lavagno, L., Martin, G., Selic, B. (eds.) Design of Embedded Real-Time Systems, pp. 323–342. Springer, Heidelberg (2003)

    Google Scholar 

  2. Bergstra, J.A., Klop, J.W.: Process algebra for synchronous communications. Inf. Control 60(1/3), 109–137 (1984). Elsevier

    Article  MathSciNet  MATH  Google Scholar 

  3. Cardelli, L., Gordon, A.D.: Mobile ambients. In: Nivat, M. (ed.) FOSSACS 1998. LNCS, vol. 1378, p. 140. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  4. Cousot, P., Cousot, R.: Abstract interpretation frameworks. J. Logic Comput. 2(4), 511–547 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  5. Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. CACM 18(8), 453–457 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  6. Hewitt, C., Bishop, P., Steiger, R.: A universal modular actor formalism for artificial intelligence. In: IJCA (1973)

    Google Scholar 

  7. Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, London (1985)

    MATH  Google Scholar 

  8. International Telecommunication Union: Recommendation Z.151 - User Requirements Notation (2008)

    Google Scholar 

  9. Letichevsky, A.A., Weigert, T., Kapitonova, J.V., Volkov, V.A.: Systems validation. In: Zurawski, R. (ed.) Embedded Systems Handbook. CRC Press, Boca Raton (2005)

    Google Scholar 

  10. Letichevsky, A.A.: About one approach to program analysis. Cybernetics 6, 1–8 (1979)

    Google Scholar 

  11. Letichevsky, A.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)

    Chapter  Google Scholar 

  12. Letichevsky, A.A., Gilbert, D.: A universal interpreter for nondeterministic concurrent programming languages. In: Fifth Compulog Network Area Meeting on Language Design and Semantic Analysis Methods (1996)

    Google Scholar 

  13. Letichevsky, A.A., Gilbert, D.: A general theory of action languages. Cybern. Syst. Anal. 34(1), 1230 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  14. Letichevsky, A.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)

    Chapter  Google Scholar 

  15. Letichevsky, A.A., Kapitonova, J.V., Kotlyarov, V.P., Volkov, V.A., Letichevsky Jr., A.A., Weigert, T.: Semantics of message sequence charts. In: Prinz, A., Reed, R., Reed, J. (eds.) SDL 2005. LNCS, vol. 3530, pp. 117–132. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  16. Letichevsky, A.A., Letichevsky Jr., A.A., Kapitonova, J.V., Volkov, V.A., Baranov, S., Kotlyarov, V.P., Weigert, T.: Basic protocols, message sequence charts, and the verification of requirements specifications. In: ISSRE (2004)

    Google Scholar 

  17. Letichevsky, A.A., Kapitonova, J.V., Letichevsky Jr., A.A., Volkov, V.A., Baranov, S., Kotlyarov, V.P., Weigert, T.: Basic protocols, message sequence charts, and the verification of requirements specifications. Comput. Netw. 47, 662–675 (2005)

    MATH  Google Scholar 

  18. Letichevsky, A.A., Kapitonova, J.V., Volkov, V.A., Letichevsky Jr., A.A., Baranov, S., Kotlyarov, V.P., Weigert, T.: System specification by basic protocols. Cybern. Syst. Anal. 41(4), 479493 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  19. Letichevsky, A.A., Letychevskyi, O.A., Peschanenko, V.S.: Insertion modeling system. In: Clarke, E., Virbitskaite, I., Voronkov, A. (eds.) PSI 2011. LNCS, vol. 7162, pp. 262–273. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  20. Letichevsky, A.A., Kapitonova, J.V., Kotlyarov, V.P., Letichevsky Jr., A.A., Nikitchenko, N.S., Volkov, V.A., Weigert, T.: Insertion modeling in distributed system design. Probl. Program. 4, 13–38 (2008). Institute of Programming Systems

    Google Scholar 

  21. Letichevsky, A.A., Godlevsky, A.B., Letichevsky Jr., A.A., Potienko, S.V., Peschanenko, V.A.: The properties of predicate transformer of the VRS system. Cybern. Syst. Anal. 4, 3–16 (2010)

    MathSciNet  MATH  Google Scholar 

  22. Letichevsky, A.A., Letichevsky Jr., A.A., Peschanenko, V., Huba, A., Weigert, T.: Symbolic traces generation in the system of insertion modelling. Cybern. Syst. Anal. 1, 3–19 (2015)

    MATH  Google Scholar 

  23. McCarthy, J.: Notes on formalizing context. In: IJCAI, pp. 555–562 (1993)

    Google Scholar 

  24. Milner, R. (ed.): A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Heidelberg (1980)

    MATH  Google Scholar 

  25. Milner, R.: Communication and Concurrency. Prentice Hall, Upper Saddle River (1989)

    MATH  Google Scholar 

  26. Milner, R.: The polyadic \(\pi \)-calculus: a tutorial. Technical report, ECS-LFCS-91-180. Laboratory for Foundations of Computer Science, Department of Computer Science. University of Edinburgh (1991)

    Google Scholar 

  27. Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104. Springer, Heidelberg (1981)

    Chapter  Google Scholar 

  28. Petri, C.A.: Kommunikation mit Automaten. Bonn: Institut fur Instrumentelle Mathematik, Schriften des IIM Nr. 2 (1962)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Glushkov Institute of Cybernetics, Academy of Sciences of Ukraine, Kyiv, Ukraine

    Alexander Letichevsky & Oleksandr Letychevskyi

  2. Kherson State University, Kherson, Ukraine

    Volodymyr Peschanenko

  3. UniqueSoft LLC, Palatine, IL, USA

    Thomas Weigert

Authors
  1. Alexander Letichevsky
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Oleksandr Letychevskyi
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Volodymyr Peschanenko
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Thomas Weigert
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Thomas Weigert .

Editor information

Editors and Affiliations

  1. Humboldt-Universität zu Berlin, Berlin, Germany

    Joachim Fischer

  2. Humboldt-Universität zu Berlin, Berlin, Germany

    Markus Scheidgen

  3. Fraunhofer FOKUS, Berlin, Germany

    Ina Schieferdecker

  4. Telecommunications Software Engineering, Windermere, United Kingdom

    Rick Reed

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Letichevsky, A., Letychevskyi, O., Peschanenko, V., Weigert, T. (2015). Insertion Modeling and Symbolic Verification of Large Systems. In: Fischer, J., Scheidgen, M., Schieferdecker, I., Reed, R. (eds) SDL 2015: Model-Driven Engineering for Smart Cities. SDL 2015. Lecture Notes in Computer Science(), vol 9369. Springer, Cham. https://doi.org/10.1007/978-3-319-24912-4_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-24912-4_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-24911-7

  • Online ISBN: 978-3-319-24912-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation