| Naslov: | Discrete time model for process meta language with fictitious-clock |
|---|
| Avtorji: | ID Vlaovič, Boštjan (Avtor)
ID Vreže, Aleksander (Avtor) |
|---|
| Datoteke: |  applsci-12-02990-v3.pdf (660,17 KB)
MD5: CBDCEE6DBB0A40EB88CBB0F5D7D70076
 https://www.mdpi.com/2076-3417/12/6/2990
|
|---|
| Jezik: | Angleški jezik |
|---|
| Vrsta gradiva: | Članek v reviji |
|---|
| Tipologija: | 1.01 - Izvirni znanstveni članek |
|---|
| Organizacija: | FERI - Fakulteta za elektrotehniko, računalništvo in informatiko
|
|---|
| 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 |
|---|
| Status publikacije: | Objavljeno |
|---|
| Verzija publikacije: | Objavljena publikacija |
|---|
| Poslano v recenzijo: | 20.01.2022 |
|---|
| Datum sprejetja članka: | 10.03.2022 |
|---|
| Datum objave: | 15.03.2022 |
|---|
| Založnik: | MDPI AG |
|---|
| Leto izida: | 2022 |
|---|
| Št. strani: | 21 str. |
|---|
| Številčenje: | Vol. 12, iss. 6 |
|---|
| PID: | 20.500.12556/DKUM-92289  |
|---|
| UDK: | 621.39 |
|---|
| COBISS.SI-ID: | 102449923 |
|---|
| DOI: | 10.3390/app12062990 |
|---|
| ISSN pri članku: | 2076-3417 |
|---|
| Avtorske pravice: | © 2022 by the authors |
|---|
| Datum objave v DKUM: | 27.03.2025 |
|---|
| Število ogledov: | 132 |
|---|
| Število prenosov: | 11 |
|---|
| Metapodatki: |    |
|---|
| Področja: | Ostalo
|
|---|
|
:
|
Kopiraj citat |
|---|
| | | | Skupna ocena: | (0 glasov) |
|---|
| Vaša ocena: | Ocenjevanje je dovoljeno samo prijavljenim uporabnikom. |
|---|
| Objavi na: |  |
|---|
Postavite miškin kazalec na naslov za izpis povzetka. Klik na naslov izpiše
podrobnosti ali sproži prenos. |
