Discrete Time Model for Process Meta Language with Fictitious-Clock
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 describin...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
MDPI AG
2022-03-01
|
| Series: | Applied Sciences |
| Subjects: | |
| Online Access: | https://www.mdpi.com/2076-3417/12/6/2990 |
| _version_ | 1797447212147408896 |
|---|---|
| author | Boštjan Vlaovič Aleksander Vreže |
| author_facet | Boštjan Vlaovič Aleksander Vreže |
| author_sort | Boštjan Vlaovič |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-03-09T13:51:38Z |
| format | Article |
| id | doaj.art-f1f46dfc96d34644a3783421c7ed1e09 |
| institution | Directory Open Access Journal |
| issn | 2076-3417 |
| language | English |
| last_indexed | 2024-03-09T13:51:38Z |
| publishDate | 2022-03-01 |
| publisher | MDPI AG |
| record_format | Article |
| series | Applied Sciences |
| spelling | doaj.art-f1f46dfc96d34644a3783421c7ed1e092023-11-30T20:49:45ZengMDPI AGApplied Sciences2076-34172022-03-01126299010.3390/app12062990Discrete Time Model for Process Meta Language with Fictitious-ClockBoštjan Vlaovič0Aleksander Vreže1Faculty of Electrical Engineering and Computer Science, University of Maribor, Koroška Cesta 46, 2000 Maribor, SloveniaFaculty of Electrical Engineering and Computer Science, University of Maribor, Koroška Cesta 46, 2000 Maribor, SloveniaIndustries 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.https://www.mdpi.com/2076-3417/12/6/2990formal specificationsformal languagesdiscrete timemodel checkingautomated extractionSDL |
| spellingShingle | Boštjan Vlaovič Aleksander Vreže Discrete Time Model for Process Meta Language with Fictitious-Clock Applied Sciences formal specifications formal languages discrete time model checking automated extraction SDL |
| title | Discrete Time Model for Process Meta Language with Fictitious-Clock |
| title_full | Discrete Time Model for Process Meta Language with Fictitious-Clock |
| title_fullStr | Discrete Time Model for Process Meta Language with Fictitious-Clock |
| title_full_unstemmed | Discrete Time Model for Process Meta Language with Fictitious-Clock |
| title_short | Discrete Time Model for Process Meta Language with Fictitious-Clock |
| title_sort | discrete time model for process meta language with fictitious clock |
| topic | formal specifications formal languages discrete time model checking automated extraction SDL |
| url | https://www.mdpi.com/2076-3417/12/6/2990 |
| work_keys_str_mv | AT bostjanvlaovic discretetimemodelforprocessmetalanguagewithfictitiousclock AT aleksandervreze discretetimemodelforprocessmetalanguagewithfictitiousclock |