Simple non-deterministic rewriting in verification

A.A. Letichevsky, V.S. Peschanenko

Abstract


Abstract. We discuss the non-deterministic rewriting in application for engine functions of Verification of Formal Specification (VFS) system in this paper. VFS – are tools to prove properties of systems described as formal specifications (basic protocols), such as the completeness (the system behavior has a possible continuation at each of its stages) and consistency (the system behavior is deterministic at each stage), safety (something bad will never happened), or the correspondence of the specified behavior to given scenarios. Together these tools constitute a powerful environment for the formal verification of formal specifications expressed through message sequence charts.

Problems in programming 2010; 2-3: 98-101


Full Text:

PDF

References


Algebraic Programming System site [http://apsystem.org.ua]

Letichevsky A.A., Kapitonova J.V., Kotlyarov V.P., Letichevsky A.A. Jr., Nikitchenko N.S., Volkov V.A. and Weigert T. Insertion modeling in

distributed system design // Programs Systems, 4: 198: 228, 2008.

Letichevsky A.A., Gilbert D.R. A Model for Interaction of Agents and Environments. In: Selected papers from the 14th International Workshop on Recent Trends in Algebraic Development Techniques. Lecture Notes in Computer Science, 1827, 311–328, 1999.

Milner R. Communication and Concurrency. Prentice Hall, 1989.

Hoare C.A.R. Communicating Sequential Processes. Prentice Hall, 1985.

Bergstra J.A., Klop J.W. Process algebra for synchronous communication. Information and Control, 60(1): 109–137, 1984.

Bergstra J.A., Ponse A., Smolka S.A., Editors. Handbook of Process Algebra. Elsevier, 2001.

Gilbert D.R., Letichevsky A.A A universal interpreter for nondeterministic concurrent programming languages. In M. Gabbrielli (editor), Fifth Compulog network area meeting on language design and semantic analysis methods, Sep. 1996.

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, ISSRE 2004, WITUL (Workshop on Integrated reliability with Telecommunications and UML Languages) , Rennes, 4 November 2005.

Letichevsky A.A., Kapitonova J.V., Kotlyarov V.P., Volkov V.A., Letichevsky A.A.Jr, and Weigert T. Semantics of Message Sequence Charts, SDL Forum, 2005.

Kapitonova J.V., A.A. Letichevsky, and S.V. Konozenko. Computations in APS. Theoretical Computer Science, 119:145–171, 1993.

Letichevsky A.A., Kapitonova Y.V., Volkov V.A., Vyshemirsky V.V. and Letichevsky A.A.Jr. Insertion Programming. Cybernetics and System Analysis, Kiev, 1, 2003.

Letichevsky A.A. and Gilbert D.R. A general theory of action languages. Cybernetics and System Analysis, (1):16–36, Feb. 1998.

Reniers M.A. Message Sequence Chart: Syntax and Semantics. Eindhoven, Eindhoven, University of Technology, 1998.


Refbacks

  • There are currently no refbacks.