The language dynamic-real and its application for verification of SDL-specified distributed systems

摘要

A distributed systems specification language Dynamic-REAL (dREAL) which extends the language Basic-REAL developed previously by dynamic constructs for generating and removing process instances is presented. A tool-set SRDSV2 (SDL/REAL Distributed Systems Verifier) intended for modeling, analysis and verification of SDL-specifications of distributed systems is described. This tool-set includes a translator from the SDL language into the dREAL language, a tool for automatic modeling of dREAL-specifications and a translator from dREAL into the input language Promela of the SPIN verifier. An application of SRDSV2 to verification of a dynamic system for booking terminals network control is described.