Abstract Avionics Application Standard Software Interface (ARINC 653) is a software specification for space and time partitioning in safety-critical avionics real-time operating systems. Correctly designed task schedulers are crucial for ARINC 653 running systems. This paper proposes a model-checking-based method for analyzing and verifying ARINC 653 scheduling model. Based on priced timed automata theory, an ARINC 653 scheduling system was modelled as a priced timed automata network. The schedulability of the system was described as a set of temporal logic expressions, and was analyzed and verified by a model checker. Our research shows that it is feasible to use model checking to analyze task schedulability in an ARINC 653 hierarchical scheduling system. The method discussed modelled preemptive scheduling by using the stop/watch features of priced timed automata. Unlike traditional scheduling analysis techniques, the proposed approach uses an exhaustive method to automate analysis of the schedulability of a system, resulting in a more precise analysis.

References

[1] Alur R., Courcoubetis C., Halbwachs N., Henzinger T., Ho P., Nicollin N., Olivero A., Sifakis J., and Yovine S., “The Algorithmic Analysis of Hybrid Systems,” Theoretical Computer Science, vol. 138, no. 1, pp. 3-34, 1995.

[2] Alur R. and Dill D., “A Theory of Timed Automata,” Theoretical Computer Science, vol. 126, no. 2, pp. 183-235, 1994.

[3] Amnell T., Fersman E., Mokrushin L., Petterssou P., and Yi W., “TIMES B-A Tool for Modelling and Implementation of Embedded Systems,” in Proceedings of Tools and Algorithms for the Construction and Analysis of Systems, Grenoble, pp. 460-464, 2002.

[4] Asberg M., Pettersson P., and Nolte T., “Modelling, Verification and Synthesis of Two- Tier Hierarchical Fixed-Priority Preemptive Scheduling,” in Proceedings of 23rd Euromicro Conference on Real-Time Systems, Porto, pp. 172-181, 2011.

[5] Aziz M. and Shah S., “Evolutionary Testing for Timing Analysis of Parallel Embedded Software,” The International Arab Journal of Information Technology, vol. 16, no. 3, pp. 415-423, 2019.

[6] Behrmann G., David A., and Larsen K., A Tutorial on Uppaal, Springer, 2004.

[7] Burns A., Advances in Real-Time Systems, Upper Prentice-Hall, 1994.

[8] Committee A., “Avionics Application Software Standard Interface Part 1-Required Services,” ARINC Specification 653P1-2, Technical Standard, Aeronautical Radio Inc., Annapolis, Maryland, 2006.

[9] Daum M., Dörrenbächer J., and Wolff B., “Proving Fairness and Implementation Correctness of A Microkernel Scheduler,” Journal of Automated Reasoning, vol. 42, no. 2- 4, pp. 349-388, 2009.

[10] Davis R. and Burns A., “Hierarchical Fixed Priority Pre-Emptive Scheduling,” in Proceedings of 26th IEEE International Symposium on Real-Time Systems, Miami, pp. 388-398, 2005.

[11] Glaubius R., Tidwell T., Smart W., and Gill C., “Scheduling Design and Verification for Open Soft Real-Time Systems,” in Proceedings of IEEE International Symposium on Real-Time Systems, Barcelona, pp. 505-514, 2008.

[12] Liu Q., Gui S., Luo L., and Li Y., “Schedulability Verification of AADL Model Based on UPPAAL,” Journal of Computer Applications Computer Applications, vol. 29, no. 7, pp. 1820-1824, 2009.

[13] Mikučionis M., Larsen K., Rasmussen J., and Nielsen B., Schedulability Analysis Using Uppaal: Herschel-Planck Case Study, Springer, 2010.

[14] Nasri M., Nelissen G., and Brandenburg B., “Response-Time Analysis of Limited- Preemptive Parallel DAG Tasks under Global Scheduling,” in Proceedings of Euromicro Conference on Real-Time Systems, Dagstuhl, pp. 1-23, 2019.

[15] Regehr J., Reid A., Webb K., Parker M., and Lepreau J., “Evolving Real-Time Systems Using Hierarchical Scheduling and Concurrency Analysis,” in Proceedings of 24th IEEE International Symposium on Real-Time Systems, Cancun, pp. 25-36, 2003. 106 The International Arab Journal of Information Technology, Vol. 17, No. 1, January 2020

[16] Serrano M., Melani A., Bertogna M., and Quinones E., “Response-Time Analysis of DAG Tasks under Fixed Priority Scheduling with Limited Preemptions,” in Proceedings of Design, Automation and Test in Europe Conference and Exhibition, Dresden, pp. 1066-1071, 2016.

[17] Sokolsky O. and Chernoguzov A., “Analysis of AADL Models Using Real-Time Calculus with Applications to Wireless Architectures,” Technical Report No.MS-CIS-08-25, University of Pennsylvania, 2008.

[18] Wang T. and Qingfan G., “Research on Distributed Integrated Modular Avionics System Architecture Design and Implementation,” in Proceedings of 32nd IEEE/AIAA International Conference on Digital Avionics Systems, East Syracuse, pp. 1-53, 2013.

[19] Waszniowski L. and Hanzálek Z., “Formal Verification of Multitasking Applications Based on Timed Automata Model,” Real-Time Systems, vol. 38, no. 1, pp. 39-65, 2008.

[20] Yalcinkaya B., Nasri M., and Brandenburg B., “An Exact Schedulability Test for Non- Preemptive Self-Suspending Real-Time Tasks,” in Proceedings of the Design, Automation and Test in Europe Conference and Exhibition, Florence, pp. 1-8, 2019. Ning Fu is an assistant research fellow at the School of Computer, Northwestern Polytechnical University, Xi'an. He received his Ph.D. (2010) degree in computer science and technology from Northwestern Polytechnical University. His main research interests focus on modelling and verification embedded system by formal methods. Lijun Shan is a lecturer at the School of Computer, Northwestern Polytechnical University, Xi'an. She received her Ph.D. degree in computer science and technology from National University of Defense Technology. Her main research interests include Model-Driven Development Method and Formal Method. Chenglie Du is a professor, Ph.D. supervisor at the School of Computer, Northwestern Polytechnical University. His main research interests include Cyber- Physical system modelling & analysis and trustworthy software architecture. Zhiqiang Liu is an associate professor at the School of Software and Microelectronics, Northwestern Polytechnical University, Xi’an. His current research interests focus on modelling and verification embedded system by formal methods. Han Peng is a PhD candidate at the School of Computer, Northwestern Polytechnical University, Xi'an. His current research interests focus on modelling and verification Cyber- Physical system by formal methods.