On the Correctness of Real-Time Modular Computer Systems Modeling with Stopwatch Automata Networks
In this paper, we consider a schedulability analysis problem for real-time modular computer systems (RT MCS). A system configuration is called schedulable if all the jobs finish within their deadlines. The authors propose a stopwatch automata-based general model of RT MCS operation. A model instance...
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Yaroslavl State University
2018-04-01
|
| Series: | Моделирование и анализ информационных систем |
| Subjects: | |
| Online Access: | https://www.mais-journal.ru/jour/article/view/678 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1849338889289859072 |
|---|---|
| author | Alevtina B. Glonina Vasily V. Balashov |
| author_facet | Alevtina B. Glonina Vasily V. Balashov |
| author_sort | Alevtina B. Glonina |
| collection | DOAJ |
| description | In this paper, we consider a schedulability analysis problem for real-time modular computer systems (RT MCS). A system configuration is called schedulable if all the jobs finish within their deadlines. The authors propose a stopwatch automata-based general model of RT MCS operation. A model instance for a given RT MCS configuration is a network of stopwatch automata (NSA) and it can be built automatically using the general model. A system operation trace, which is necessary for checking the schedulability criterion, can be obtained from the corresponding NSA trace. The paper substantiates the correctness of the proposed approach. A set of correctness requirements to models of system components and to the whole system model were derived from RT MCS specifications. The authors proved that if all models of system components satisfy the corresponding requirements, the whole system model built according to the proposed approach satisfies its correctness requirements and is deterministic (i.e. for a given configuration a trace generated by the corresponding model run is uniquely determined). The model determinism implies that any model run can be used for schedulability analysis. This fact is crucial for the approach efficiency, as the number of possible model runs grows exponentially with the number of jobs in a system. Correctness requirements to models of system components models can be checked automatically by a verifier using observer automata approach. The authors proved by using UPPAAL verifier that all the developed models of system components satisfy the corresponding requirements. User-defined models of system components can be also used for system modeling if they satisfy the requirements. |
| format | Article |
| id | doaj-art-0745cddfd8804a27b7c54bfb14f11521 |
| institution | Kabale University |
| issn | 1818-1015 2313-5417 |
| language | English |
| publishDate | 2018-04-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj-art-0745cddfd8804a27b7c54bfb14f115212025-08-20T03:44:17ZengYaroslavl State UniversityМоделирование и анализ информационных систем1818-10152313-54172018-04-0125217419210.18255/1818-1015-2018-2-174-192498On the Correctness of Real-Time Modular Computer Systems Modeling with Stopwatch Automata NetworksAlevtina B. Glonina0Vasily V. Balashov1Lomonosov Moscow State UniversityLomonosov Moscow State UniversityIn this paper, we consider a schedulability analysis problem for real-time modular computer systems (RT MCS). A system configuration is called schedulable if all the jobs finish within their deadlines. The authors propose a stopwatch automata-based general model of RT MCS operation. A model instance for a given RT MCS configuration is a network of stopwatch automata (NSA) and it can be built automatically using the general model. A system operation trace, which is necessary for checking the schedulability criterion, can be obtained from the corresponding NSA trace. The paper substantiates the correctness of the proposed approach. A set of correctness requirements to models of system components and to the whole system model were derived from RT MCS specifications. The authors proved that if all models of system components satisfy the corresponding requirements, the whole system model built according to the proposed approach satisfies its correctness requirements and is deterministic (i.e. for a given configuration a trace generated by the corresponding model run is uniquely determined). The model determinism implies that any model run can be used for schedulability analysis. This fact is crucial for the approach efficiency, as the number of possible model runs grows exponentially with the number of jobs in a system. Correctness requirements to models of system components models can be checked automatically by a verifier using observer automata approach. The authors proved by using UPPAAL verifier that all the developed models of system components satisfy the corresponding requirements. User-defined models of system components can be also used for system modeling if they satisfy the requirements.https://www.mais-journal.ru/jour/article/view/678modelingmodel checkingintegrated modular avionicsscheduling |
| spellingShingle | Alevtina B. Glonina Vasily V. Balashov On the Correctness of Real-Time Modular Computer Systems Modeling with Stopwatch Automata Networks Моделирование и анализ информационных систем modeling model checking integrated modular avionics scheduling |
| title | On the Correctness of Real-Time Modular Computer Systems Modeling with Stopwatch Automata Networks |
| title_full | On the Correctness of Real-Time Modular Computer Systems Modeling with Stopwatch Automata Networks |
| title_fullStr | On the Correctness of Real-Time Modular Computer Systems Modeling with Stopwatch Automata Networks |
| title_full_unstemmed | On the Correctness of Real-Time Modular Computer Systems Modeling with Stopwatch Automata Networks |
| title_short | On the Correctness of Real-Time Modular Computer Systems Modeling with Stopwatch Automata Networks |
| title_sort | on the correctness of real time modular computer systems modeling with stopwatch automata networks |
| topic | modeling model checking integrated modular avionics scheduling |
| url | https://www.mais-journal.ru/jour/article/view/678 |
| work_keys_str_mv | AT alevtinabglonina onthecorrectnessofrealtimemodularcomputersystemsmodelingwithstopwatchautomatanetworks AT vasilyvbalashov onthecorrectnessofrealtimemodularcomputersystemsmodelingwithstopwatchautomatanetworks |