Open AccessEXPERIENCE WITH FORMAL VERIFICATION OF SDL PROTOCOLS
Author(s) -
Marius Minea,
Cornel Izbaşa,
Călin Jebelean
Publication year - 2014
Publication title -
computing
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.184
H-Index - 11
eISSN - 2312-5381
pISSN - 1727-6209
DOI - 10.47839/ijc.2.3.231
Subject(s) - computer science , formal verification , software engineering , process (computing) , formal methods , component (thermodynamics) , communications protocol , programming language , block (permutation group theory) , software , embedded system , operating system , physics , geometry , mathematics , thermodynamics
This paper presents a case study in the application of formal methods to the verification of communication protocols. We analyze one component block of telephone switching software developed in the SDL language at Alcatel Network Systems Romania. We use the IF toolset from VERIMAG Grenoble to build a state-transition model of the system and verify selected properties. We present the steps performed for translation and verification and discuss the potential for automating the process and using it on a larger scale.