Applying Automated Model Extraction for Simulation and Verification of Real-Life SDL Specification With Spin | Zendy

Bostjan Vlaovic | Zendy; Aleksander Vreze | Zendy; Zmago Brezocnik | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Applying Automated Model Extraction for Simulation and Verification of Real-Life SDL Specification With Spin

Author(s) -

Bostjan Vlaovic,

Aleksander Vreze,

Zmago Brezocnik

Publication year - 2017

Publication title -

ieee access

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.587

H-Index - 127

ISSN - 2169-3536

DOI - 10.1109/access.2017.2685238

Subject(s) - aerospace , bioengineering , communication, networking and broadcast technologies , components, circuits, devices and systems , computing and processing , engineered materials, dielectrics and plasmas , engineering profession , fields, waves and electromagnetics , general topics for engineers , geoscience , nuclear engineering , photonics and electrooptics , power, energy and industry applications , robotics and control systems , signal processing and analysis , transportation

Formally defined Specification and Description Language (SDL) is used for the design and specification of complex safety-critical systems. Each change in the specification of the product should be immediately checked formally against the requirements' specification. This paper presents semi-automated system abstraction, automated model extraction, simulation, and formal verification of real-life complex SDL specification. Sound algorithms implemented in our sdl2pml automated model extraction tool preserve all properties of the SDL system. Sdl2pml includes our model of discrete time, abstraction, and support for all relevant SDL functionality and constructs such as dynamic process creation, rational data types, and communication with more than one process instance. To the best of our knowledge, most of them are not supported by any other known approach. We use our SpinRCP tool for simulation and formal verification of the extracted model with the Spin model checker. We demonstrate the applicability of our approach on ISDN User adaptation protocol from SI3000 Softswitch. The extracted Promela model is the largest one ever processed by Spin. We have shown that Spin simulation and model checking can be applied successfully to such huge models.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research