Preprints of IIS SB RAS, 2011
Preprint 161
V.A. Nepomniaschy, E.V. Bodin, S.O. Veretnov
Application of Dynamic-REAL language for analysis and verification of distributed systems specified in the language SDL

A new version of the program complex SRDSV2 (SDL/REAL Distributed Systems Verifier) intended for modeling, analysis and verification of SDLspecifications of distributed systems is described. This complex includes a translator from the SDL language into the Dynamic-REAL language (dREAL), a tool for automatic modeling of dREAL- specifications and a translator from dREAL into the input language Promela of the SPIN verifier. In the SRDSV2 version dREAL has been extended by introducing procedures. This extension allows to reduce the amount of dREAL- specifications and their models in Promela. An application of the SRDSV2 tool-set to analysis and verification of a dynamic system for control of booking terminals net is described.

Download the text in PDF (In Russian)
Preprint 160
I.V. Maryasov
The mixed axiomatic semantics method

This work represents a mixed axiomatic semantics method suggested for Clight program verification. This semantics has the unambiguity of inference (i. e. one and only one inference rule is allowed at each step) and also has special variants of inference rules for the same program statement which are applied depending on the variable type and static information. This approach allows significant simplification of verification conditions.

This work was partially supported by Russian Foundation for Basic Research under grant 11-01-00028.

Download the text in PDF (In Russian)



You are reporting a typo in the following text:
Simply click the "Send typo report" button to complete the report. You can also include a comment.