20.500.12556/DKUM-67146 Applying automated model extraction for simulation and verification of real-life SDL specification with spin 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. formal specifications automated extraction formal languages simulation formal verification model cheking SDL Promela SpinRCP Sdl2pml formalna specifikacija avtomatska ekstrakcija simulacija formalni jeziki true true true Angleški jezik Slovenski jezik Znanstveno delo 2017-08-03 12:58:55 2017-08-03 12:59:35 2022-08-01 13:36:15 2019-07-11 16:10:34 2017 0 0 str. 5046-5058 Letn. 5 21 March 2017 0000-00-00 Zaloznikova Objavljeno NiDoloceno 0000-00-00 0000-00-00 0000-00-00 2169-3536 621.39 519839513 20580374 10.1109/ACCESS.2017.2685238 2169-3536 URN:SI:UM:DK:CTAAN65V IEEE_Access_2017_Vlaovic,_Vreze,_Brezocnik_Applying_Automated_Model_Extraction_for_Simulation_and_Verification_of_Real-Life_SDL_Specific.pdf IEEE_Access_2017_Vlaovic,_Vreze,_Brezocnik_Applying_Automated_Model_Extraction_for_Simulation_and_Verification_of_Real-Life_SDL_Specific.pdf 1 B86FF0DF24248982A735162040EE9710 bcafbdfe11109ebc3153456967aa1b7538864b2c3d995639b02350cf3c1d0827 797e7a80-7c0e-11eb-bb7a-00155d0001ca 20.500.12556/dkum/0628cbd4-6a3d-434e-a743-ddd45547db9f https://dk.um.si/Dokument.php?lang=slv&id=114808 http://ieeexplore.ieee.org/document/7883829/ 1 https://dk.um.si/Dokument.php?lang=slv&id=114807 Fakulteta za elektrotehniko, računalništvo in informatiko 0 0 0