| | SLO | ENG | Piškotki in zasebnost

Večja pisava | Manjša pisava

Izpis gradiva

Naslov:Applying automated model extraction for simulation and verification of real-life SDL specification with spin
Avtorji:Vlaovič, Boštjan (Avtor)
Vreže, Aleksander (Avtor)
Brezočnik, Zmago (Avtor)
Institute of Electrical and Electronics Engineers (Lastnik avtorskih pravic)
Datoteke:.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
 
URL http://ieeexplore.ieee.org/document/7883829/
 
Jezik:Angleški jezik
Vrsta gradiva:Znanstveno delo (r2)
Tipologija:1.01 - Izvirni znanstveni članek
Organizacija:FERI - Fakulteta za elektrotehniko, računalništvo in informatiko
Opis: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.
Ključne besede:formal specifications, automated extraction, formal languages, simulation, formal verification, model cheking, SDL, Promela, SpinRCP, Sdl2pml
Leto izida:2017
Št. strani:str. 5046-5058
Številčenje:Letn. 5
ISSN:2169-3536
UDK:621.39
COBISS_ID:20580374 Novo okno
DOI:10.1109/ACCESS.2017.2685238 Novo okno
ISSN pri članku:2169-3536
NUK URN:URN:SI:UM:DK:CTAAN65V
Število ogledov:713
Število prenosov:316
Metapodatki:XML RDF-CHPDL DC-XML DC-RDF
Področja:Ostalo
:
  
Skupna ocena:(0 glasov)
Vaša ocena:Ocenjevanje je dovoljeno samo prijavljenim uporabnikom.
Objavi na:AddThis
AddThis uporablja piškotke, za katere potrebujemo vaše privoljenje.
Uredi privoljenje...

Postavite miškin kazalec na naslov za izpis povzetka. Klik na naslov izpiše podrobnosti ali sproži prenos.

Gradivo je del revije

Naslov:IEEE Access
Založnik:Institute of Electrical and Electronics Engineers
ISSN:2169-3536
COBISS.SI-ID:519839513 Novo okno

Sekundarni jezik

Jezik:Slovenski jezik
Ključne besede:formalna specifikacija, avtomatska ekstrakcija, simulacija, formalni jeziki


Komentarji

Dodaj komentar

Za komentiranje se morate prijaviti.

Komentarji (0)
0 - 0 / 0
 
Ni komentarjev!

Nazaj
Logotipi partnerjev Univerza v Mariboru Univerza v Ljubljani Univerza na Primorskem Univerza v Novi Gorici