| | SLO | ENG | Cookies and privacy

Bigger font | Smaller font

Show document Help

Title:Applying automated model extraction for simulation and verification of real-life SDL specification with spin
Authors:ID Vlaovič, Boštjan (Author)
ID Vreže, Aleksander (Author)
ID Brezočnik, Zmago (Author)
ID Institute of Electrical and Electronics Engineers (Copyright holder)
Files:.pdf IEEE_Access_2017_Vlaovic,_Vreze,_Brezocnik_Applying_Automated_Model_Extraction_for_Simulation_and_Verification_of_Real-Life_SDL_Specific.pdf (13,46 MB)
MD5: B86FF0DF24248982A735162040EE9710
PID: 20.500.12556/dkum/0628cbd4-6a3d-434e-a743-ddd45547db9f
 
URL http://ieeexplore.ieee.org/document/7883829/
 
Language:English
Work type:Scientific work
Typology:1.01 - Original Scientific Article
Organization:FERI - Faculty of Electrical Engineering and Computer Science
Abstract: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.
Keywords:formal specifications, automated extraction, formal languages, simulation, formal verification, model cheking, SDL, Promela, SpinRCP, Sdl2pml
Publication status:Published
Publication version:Version of Record
Year of publishing:2017
Number of pages:str. 5046-5058
Numbering:Letn. 5
PID:20.500.12556/DKUM-67146 New window
ISSN:2169-3536
UDC:621.39
ISSN on article:2169-3536
COBISS.SI-ID:20580374 New window
DOI:10.1109/ACCESS.2017.2685238 New window
NUK URN:URN:SI:UM:DK:CTAAN65V
Publication date in DKUM:03.08.2017
Views:1402
Downloads:429
Metadata:XML DC-XML DC-RDF
Categories:Misc.
:
VLAOVIČ, Boštjan, VREŽE, Aleksander and BREZOČNIK, Zmago, 2017, Applying automated model extraction for simulation and verification of real-life SDL specification with spin. IEEE access [online]. 2017. Vol. 5, p. 5046–5058. [Accessed 21 January 2025]. DOI 10.1109/ACCESS.2017.2685238. Retrieved from: https://dk.um.si/IzpisGradiva.php?lang=eng&id=67146
Copy citation
  
Average score:
0.5
1
1.5
2
2.5
3
3.5
4
4.5
5
(0 votes)
Your score:Voting is allowed only for logged in users.
Share:Bookmark and Share


Searching for similar works...Please wait....
Hover the mouse pointer over a document title to show the abstract or click on the title to get all document metadata.

Record is a part of a journal

Title:IEEE access
Publisher:Institute of Electrical and Electronics Engineers
ISSN:2169-3536
COBISS.SI-ID:519839513 New window

Secondary language

Language:Slovenian
Keywords:formalna specifikacija, avtomatska ekstrakcija, simulacija, formalni jeziki


Comments

Leave comment

You must log in to leave a comment.

Comments (0)
0 - 0 / 0
 
There are no comments!

Back
Logos of partners University of Maribor University of Ljubljana University of Primorska University of Nova Gorica