The analysis and verification of SDL-specifications of distributed systems using Dynamic-REAL Language

At present, the role of formal methods used to develop distributed systems, such as control systems and communication protocols, is quite significant. SDL language is widely used to specify distributed systems. Therefore, the problem of analysis and verification of SDL-specifications of distributed systems is actual. This problem has been considered in a number of publications where the use of the well-known SPIN system for verification of SDL specifications using IF language as the intermediate language is described. In contrast to that approach, along with the SPIN verification system, we use a system for modeling the behavior of SDL specifications, as well as a system for finding errors in SDL specifications with the help of the obtained counterexamples. This allows us to analyze the SDL-specifications even when the SPIN system is not applicable. This paper describes the new software package SRDSVer3 (SDL / REAL Distributed Systems Verifier), intended for modeling, analysis and verification of SDL-specifications. The input language of the software package SRDSVer3 includes the basic base constructs of the SDL-2010 language, such as BLOCK, PROCESS, SIGNALROUTE, CHANNEL, SAVE, SIGNAL. To describe the properties of SDL-specifications, an SDL Properties Language (SPLan) was developed, based on linear time logic (LTL), extended by quantifiers for process instances. For modeling and analysis of SDL-specifications, a query language was developed. This software package uses the intermediate specification language Dynamic-REAL (dREAL), which is a combined specification language for both distributed systems and their properties. The advantages of dREAL are caused by its syntax for textual and graphical presentation of specifications, formal operational semantics and expressive language for representing properties. The developed software package SRDSVer3 is a powerful tool that includes a translator from language SDL to language dREAL and two tools for analysis and verification. The first tool includes a translator from language dREAL to the input language Promela of the SPIN verification system, a converter of properties of SDL-specifications to LTL formulas, and a SPIN verification system. The second tool consists of a tool for simulation and automatic modeling of dREAL specifications, and a converter for translating queries expressed in SDL into dREAL. The automatic modeling tool plays an important role, since it can be successfully applied in the cases when the SPIN verification system is not applicable due to the large size of the SDL-specification models. The input language of software package SRDSVer3 includes the basic base language constructions of language SDL-2010 widely used in practice. The package SRDSVer3 allows the user to verify specifications of distributed systems with respect to their properties represented in the language SPLan, as well as to obtain the counterexamples in terms of SDL. The advantages of this approach are illustrated by automatic modeling and verification of a dynamic ATM network management system. An experiment was also conducted with an incorrect specification of this management system, where an error was introduced at the level of the SDL specification. If an error is detected, the package allows to trace the execution path in the original SDL specification.

Keywords

Authors

References