Methods of forward and backward symbolic modeling of systems specified by basic protocols

S.V. Potienko

Abstract


The paper considers methods of forward and backward symbolic modeling which are used for solution of verification tasks for basic protocols systems. Besides of algorithms for state space search detailed in model checking works, the main task of symbolic modeling is implementation of transition from one state class to the next. Such a transformation is realized by predicate transformers. In the current work, algorithms of forward and backward predicate transformers have been built for numeric, symbolic, and lists data structures. Transformers are considered as functions which derive from given formula a new one that defines state class of the system after transition made by given basic protocol.

Problems in programming 2008; 4: 39-44


References


Letichevsky and D. Gilbert. A Model for Interac­tion of Agents and Environments // In D. Bert, C. Choppy, P. Moses, editors. Recent Trends in Al­gebraic Development Techniques. Lecture Notes in Computer Science 1827, Springer. –1999.

A. Letichevsky, J. Kapitonova, A. Letichevsky Jr., V. Volkov, S. Baranov, V. Kotlyarov, T. Weigert. Basic Protocols, Message Sequence Charts, and the Verification of Requirements Specifications // Proc. International Workshop, WITUL’04. Rennes (France). –2004.

J. Kapitonova, A. Letichevsky, V. Volkov, and T. Weigert. Validation of Embedded Systems // In R. Zurawski, editor. The Embedded Systems Hand­book. CRC Press, Miami. – 2005.

А.А.Летичевский (мл.). Об одном классе базо­вых протоколов // Проблеми програмування, №4. – 2005 - С. 3-21.

О.О.Летичевський, І.А.Левченко. Символьна трасова генерація // Тези доп. міжнар. конф. «Теоретичні та прикладні аспекти побудови програмних систем TAAPSD'2005» – Київ. На­УКМА, національний ун-т ім. Т.Г. Шевченка, ін-т програмних систем НАН України. – 2005.

Колчин А.В. Направленный поиск в верифика­ции формальных моделей // Тези доп. міжнар. конф. «Теоретичні та прикладні аспекти побу­дови програмних систем TAAPSD'2007» – Бер­дянськ. НаУКМА, національний ун-т ім. Т.Г. Шевченка, ін-т програмних систем НАН України. – 2007. – С. 256–258.

Letichevsky A., Kapitonova J., Letichevsky A. Jr., Volkov V., Baranov S., Kotlyarov V., Weigert T. Basic Protocols, Message Sequence Charts, and the Verification of Requirements Specifications // Proc. International Workshop, WITUL’04. Rennes (France). – 2004. – P. 30–38.

Kapitonova J., Letichevsky A., Volkov V., and Weigert T. Validation of Embedded Systems // In R. Zurawski, editor. The Embedded Systems

Handbook. CRC Press, Miami. – 2005. – 51 p.


Refbacks

  • There are currently no refbacks.