Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Cover of the book

2015 | OriginalPaper | Chapter

Insertion Modeling and Symbolic Verification of Large Systems

Authors : Alexander Letichevsky, Oleksandr Letychevskyi, Volodymyr Peschanenko, Thomas Weigert

Published in: SDL 2015: Model-Driven Engineering for Smart Cities

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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).

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
next chapter A Model-Based Framework for SLA Management and Dynamic Reconfiguration
Literature
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)
2.
3.
Cardelli, L., Gordon, A.D.: Mobile ambients. In: Nivat, M. (ed.) FOSSACS 1998. LNCS, vol. 1378, p. 140. Springer, Heidelberg (1998) CrossRef
4.
5.
6.
Hewitt, C., Bishop, P., Steiger, R.: A universal modular actor formalism for artificial intelligence. In: IJCA (1973)
7.
Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, London (1985) MATH
8.
International Telecommunication Union: Recommendation Z.151 - User Requirements Notation (2008)
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)
10.
Letichevsky, A.A.: About one approach to program analysis. Cybernetics 6, 1–8 (1979)
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)CrossRef
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)
13.
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) CrossRef
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) CrossRef
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)
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
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)MathSciNetCrossRefMATH
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) CrossRef
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
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)MathSciNetMATH
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
23.
McCarthy, J.: Notes on formalizing context. In: IJCAI, pp. 555–562 (1993)
24.
Milner, R. (ed.): A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Heidelberg (1980)MATH
25.
Milner, R.: Communication and Concurrency. Prentice Hall, Upper Saddle River (1989)MATH
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)
27.
Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104. Springer, Heidelberg (1981) CrossRef
28.
Petri, C.A.: Kommunikation mit Automaten. Bonn: Institut fur Instrumentelle Mathematik, Schriften des IIM Nr. 2 (1962)
Metadata
Title
Insertion Modeling and Symbolic Verification of Large Systems
Authors
Alexander Letichevsky
Oleksandr Letychevskyi
Volodymyr Peschanenko
Thomas Weigert
Copyright Year
2015
Book
SDL 2015: Model-Driven Engineering for Smart Cities

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

Electronic ISBN: 978-3-319-24912-4

Copyright Year: 2015

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

Premium Partner

    Image Credits