1. Discrete time model for process meta language with fictitious-clockBoštjan Vlaovič, Aleksander Vreže, 2022, izvirni znanstveni članek Opis: Industries like telecommunications, medical, automotive, military, avionics, and aerospace
use complex real-time systems. Specification and Description Language (SDL) is one of the leading
domain specific languages that is formally defined by international standards and well established in
describing such systems. To check system properties abstracted model of the system is prepared in
selected modeling language. We use Spin (Simple Promela Interpreter) model checker that is one of
the leading tools for verification of complex concurrent and reactive systems. This paper focuses on
modeling the SDL timer construct. It is one of the SDL constructs that is not easily modeled with
Promela, but is present in many SDL systems. After an overview of the related work we propose
a new Discrete Time Model for Promela (DTMP) that is seamlessly integrated in our framework
for modeling SDL systems and can be used with the mainstream version of the Spin tool. To the
best of our knowledge, this is not possible with the existing solutions. We describe how DTMP can
be used to model SDL systems that use timers. Experimental results demonstrate its applicability
to non-SDL systems with Fischer’s mutual exclusion protocol and the Parallel Acknowledgment
with Retransmission that were used in prior studies. We compare state-space requirements with
one of the existing solutions DT Promela and DT Spin. With that, virtues and shortcomings of this
high-level solution are exposed. We have shown that DTMP is effective when an extensive range of
timer expiration values are used, which is usually the case in real-life SDL systems.
Ključne besede: formal specifications, formal languages, discrete time, model checking, automated extraction, SDL, Promela, SpinRCP, Sdl2pml
Objavljeno v DKUM: 27.03.2025; Ogledov: 0; Prenosov: 6
 Celotno besedilo (660,17 KB)
Gradivo ima več datotek! Več... |
2. Applying automated model extraction for simulation and verification of real-life SDL specification with spinBoštjan Vlaovič, Aleksander Vreže, Zmago Brezočnik, 2017, izvirni znanstveni članek 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
Objavljeno v DKUM: 03.08.2017; Ogledov: 1402; Prenosov: 474
Celotno besedilo (13,46 MB)
Gradivo ima več datotek! Več... |
3. SNEMANJE POGOVOROV ZA OMOGOČANJE LEGALNEGA NADZORA V TELEKOMUNIKACIJSKIH OMREŽJIHDavid Brezovšek, 2009, diplomsko delo Opis: Diplomska naloga opisuje storitev za snemanje pogovorov lokalnega naročnika telefonske centrale pri podjetju Iskratel, d. o. o.
Storitev za snemanje pogovorov lokalnega naročnika telefonske centrale naj bi bila sposobna narediti telefonski klic na poljubno snemalno napravo, administracija storitve pa naj bi potekala izključno preko upravljalnega vozlišča telefonske centrale — storitev spada med dopolnilne storitve lokalnega naročnika telefonske centrale. Razvoj storitve za snemanje pogovorov lokalnega naročnika telefonske centrale je pomenil implementacijo dodatne funkcionalnosti v obstoječi produkt SI2000 iCS proizvajalca Iskratel. Delo je vključevalo vse faze razvoja storitve za snemanje pogovorov lokalnega naročnika telefonske centrale, tj. od ideje do končne izvedbe. Storitev za snemanje pogovorov lokalnega naročnika telefonske centrale sem razvijal v programskem jeziku SDL. Posebna pozornost je bila namenjena preverjanju delovanja celotnega produkta SI2000 iCS oziroma potrjevanju, da implementacija nove funkcionalnosti za snemanje pogovorov lokalnega naročnika nima negativnih stranskih učinkov na delovanje ostalih funkcionalnosti produkta SI2000 iCS. Rezultat naloge je delujoča rešitev, ki omogoča snemanje klicev lokalnega naročnika na poljubno snemalno napravo, ki je zmožna sprejeti telefonski klic po eni izmed signalizacij, podprtih v telefonski centrali (npr. analogni, H.323, ISDN, SIP ...). Pogovori nadzorovanega lokalnega naročnika se snemajo stalno ali na zahtevo lokalnega naročnika telefonske centrale. Nadzor lokalnega naročnika aktivira administrativno osebje telefonske centrale, v primeru snemanja na zahtevo pa lokalni naročnik telefonske centrale med zvezo.
Ključne besede: snemanje pogovorov, legalni nadzor, SI2000, SDL
Objavljeno v DKUM: 19.01.2010; Ogledov: 2719; Prenosov: 178
Celotno besedilo (2,06 MB) |
4. PRIMERJAVA IZBRANIH RAZVOJNIH ORODIJ S PODPORO JEZIKU SDLKlara Podbreznik, 2009, diplomsko delo Opis: V diplomskem delu so predstavljena izbrana razvojna orodja s podporo jeziku SDL (Specification and Description Language) – Telelogic SDL Suite, ObjectGEODE, Cinderella in Safire Professional. Orodja smo preverjali z uporabo poenostavljenega protokola V.76, ki je namenjen vzpostavitvi podatkovne povezave in prenosu podatkov med dvema uporabnikoma. V večini orodij smo uvozili obstoječ opis sistema, le v orodju Cinderella smo sistem zgradili tudi sami. V orodju Safire Professional sistema ni bilo mogoče uvoziti, zaradi prevelikega odstopanja od standarda Z.100, tudi lastna izgradnja sistema ni bila uspešna. Delovanje sistema smo praviloma preverili s simulacijo štirih testnih scenarijev. Ob tem smo predstavili uporabniško izkušnjo ter prednosti in slabosti posameznega orodja s poudarkom na preverjanju skladnosti s standardom Z.100.
Ključne besede: SDL, Telelogic SDL Suite, ObjectGEODE, Cinderella, Safire Professional, razvojno orodje, telekomunikacijski sistem, specifikacija
Objavljeno v DKUM: 10.04.2009; Ogledov: 2436; Prenosov: 218
Celotno besedilo (2,67 MB) |
5. |
6. |
7. Odkrivanje interakcij med telefonskimi storitvami z orodjem ObjectGEODE : diplomsko delo univerzitetnega študijaTatjana Kuhar Avdičaušević, 1999, diplomsko delo Ključne besede: telekomunikacijski sistemi, osnovne telefonske storitve, dopolnilne storitve, interakcije med storitvami, formalne metode, SDL, MSC, GOAL, ObjectGEODE
Objavljeno v DKUM: 26.07.2007; Ogledov: 2539; Prenosov: 0 |
8. |
