О корректности моделирования модульных вычислительных систем реального времени с помощью сетей временных автоматов

Рассматривается задача проверки допустимости конфигураций модульных вычислительных систем реального времени (МВС РВ). Конфигурация считается допустимой, если все работы успевают выполниться на МВС РВ в рамках своих директивных интервалов. Предложена обобщенная модель функционирования МВС РВ и метод построения на её основе модели для конкретной конфигурации. Модель представляет собой сеть временных автоматов с остановкой таймеров. По вычислению сети автоматов предлагается строить временную диаграмму (ВД) функционирования МВС РВ, необходимую для проверки допустимости. В работе обосновывается корректность предложенного подхода. Из спецификаций на МВС РВ был выделен ряд требований, применимых к моделям МВС РВ и их компонентов на выбранном уровне абстракции. Модели считаются корректными, если удовлетворяют этим требованиям. Доказано, что если все модели компонентов системы удовлетворяют соответствующим требованиям, то модель МВС РВ, построенная согласно предложенному подходу, удовлетворяет требованиям к модели системы в целом (то есть корректна), а также является детерминированной. Под детерминированностью понимается однозначность построения ВД сети автоматов, соответствующей заданной конфигурации. Это позволяет использовать для проверки допустимости конфигурации любое вычисление соответствующей сети автоматов, что крайне важно для эффективности предложенного подхода, так как число возможных вычислений сети автоматов растет экспоненциально с числом работ в системе. Выполнение требований корректности к моделям компонентов системы может быть проверено автоматически с использованием верификатора и подхода автоматов-наблюдателей. Все разработанные нами модели компонентов системы удовлетворяют соответствующим требованиям, что было доказано с помощью верификатора UPPAAL. Если пользовательские модели компонентов системы удовлетворяют требованиям корректности, то они могут быть включены в модель МВС РВ, которая при этом останется корректной и детерминированной.

1. Watkins C.B., Walter R., “Transitioning from Federated Avionics Architectures to

2. Integrated Modular Avionics”, Proceedings of the 26th IEEE/AIAA Digital Avionics Systems Conference, 2007, 2.A.1-1–2.A.1-10.

3. 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.

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

5. Avionics Application Software Standard Interface. Arinc Specification 653, Aeronautical Radio, 1997.

6. 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.

7. Mallachiev K.M., Pakulin N.V., Khoroshilov A.V., “Design and Architecture of RealTime Operating System”, Proceedings of ISP RAS, 28:2 (2016), 181–192.

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

9. 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.

10. Третьяков А., “Автоматизация построения расписаний для периодических систем реального времени”, ТрудыИнститутасистемногопрограммированияРАН, 22 (2012), 375–400.

11. 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.

12. 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.

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

14. “UPPAAL Home”, http://www.uppaal.org/.

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

16. 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.

17. 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.

18. 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.

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