On the correctness of real-time modular computer systems modeling with stopwatch automata networks

A. B. Glonina ; V. V. Balashov

Modelirovanie i analiz informacionnyh sistem, Tome 25 (2018) no. 2, pp. 174-192.

Résumé

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.

Détail

Keywords: modeling, model checking, integrated modular avionics, scheduling.

Bibliographie

[1] Watkins C. B., Walter R., “Transitioning from Federated Avionics Architectures to Integrated Modular Avionics”, Proceedings of the 26th IEEE/AIAA Digital Avionics Systems Conference, 2007, 2.A.1-1–2.A.1-10

[2] Glonina A. B., Bahmurov A. G., “Stopwatch Automata-Based Model for Efficient Schedulability Analysis of Modular Computer Systems”, Parallel Computing Technologies, LNCS, 10421, Springer, 2017, 289–300

[3] Cassez F., Larsen K, “The Impressive Power of Stopwatches”, CONCUR 2000 — Concurrency Theory, LNCS, 1877, Springer, 2000, 138–152 | MR

[4] Avionics Application Software Standard Interface, Arinc Specification 653, Aeronautical Radio, 1997

[5] Marouf M., Sorel Y., “Scheduling Non-Preemptive Hard Real-Time Tasks with Strict Periods”, Proceedings of the 16th IEEE Conference on Emerging Technologies Factory Automation (ETFA), 2011, 1–8

[6] Mallachiev K. M., Pakulin N. V., Khoroshilov A. V., “Design and Architecture of Real-Time Operating System”, Proceedings of ISP RAS, 28:2 (2016), 181–192 | DOI

[7] RTCA: DO-297: Integrated Modular Avionics (IMA) Development Guidance and Certification Considerations, Radio Technical Commission for Aeronautics, 2005

[8] Balashov V. V., Balakhanov V. A., Kostenko V. A., “Scheduling of Computational Tasks in Switched Network-Based IMA Systems”, Proceedings of International Conference on Engineering and Applied Sciences Optimization, 2014, 1001–1014

[9] Tretyakov A., “Automation of Scheduling for Periodic Real-Time Systems”, Proceedings of ISP RAS, 22 (2012), 375–400 (in Russian)

[10] Wang D., Han J., Ma D., Zhao X., “Studying on ARINC653 Partition Run-time Scheduling and Simulation”, Proceedings of World Academy of Science, Engineering and Technology, 2012, 1583–1587

[11] Lee Y. H., Kim D., Younis M., Zhou J., “Scheduling Tool and Algorithm for Integrated Modular Avionics Systems”, Proceedings of the 19th IEEE Digital Avionics Systems Conference, 2000, 1C2/1–1C2/8

[12] Aircraft Data Network Part 7. Avionics Full Duplex Switched Ethernet (AFDX) Network, Aeronautical Radio, 2005

[13] UPPAAL Home, http://www.uppaal.org/

[14] Andre E., “Observer Patterns for Real-Time Systems”, Proceedings of the 18th International Conference on Engineering of Complex Computer Systems, 2013, 125–134

[15] Abdeddaim Y., Maler O., “Preemptive Job-Shop Scheduling using Stopwatch Automata”, Tools and Algorithms for the Construction and Analysis of Systems, LNCS, 2280, Springer, 2002, 113–126 | MR

[16] Krcal P., Yi W., “Decidable and Undecidable Problems in Schedulability Analysis Using Timed Automata”, Tools and Algorithms for the Construction and Analysis of Systems, LNCS, 2988, Springer, 2004, 236–250

[17] David A., Illum J., Larsen K., Skou A., “Model-based Framework for Schedulability Analysis Using Uppaal 4.1”, Model-Based Design for Embedded Systems, 2009, 93–119 | DOI

[18] Apt K. R., Kozen D. C., “Limits for Automatic Verification of Finite-State Concurrent Systems”, Information Processing Letters, 22:6 (1986), 307–309 | DOI | MR