Abstract
\(\mu \)C/OS-III is the third generation of real-time operating systems based on multi-task scheduling for embedded systems. The multi-task system which refers to tasks with the same priority, tasks synchronization and communication, is scheduled by the operating system kernel. It is critical to ensure the timeliness and correctness of related applications using \(\mu \)C/OS-III. This paper proposes a model checking approach to verify a multi-task embedded system running under \(\mu \)C/OS-III. To do so, the multi-task system and its properties are modelled in TMSVL. A model checker built in the toolkit MSV is used to verify the schedulabilty of the \(\mu \)C/OS-III multi-task system. Experiments show that our approach is effective and efficient in verifying embedded systems.
This research is supported by the NSFC Grant Nos. 61133001, 61272117, 61322202, 61420106004, and 91418201.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Abdeddaım, Y., Asarin, E., Maler, O.: Scheduling with timed automata. Theoret. Comput. Sci. 354(4), 272–300 (2006)
Mokadem, H.B., Berard, B., Gourcuff, V., De Smet, O., Roussel, J.-M.: Verification of a timed multitask system with uppaal. IEEE Trans. Autom. Sci. Eng. 7(4), 921–932 (2010)
Bini, E., Buttazzo, G.C.: Schedulability analysis of periodic fixed priority systems. IEEE Trans. Comput. 53(11), 1462–1473 (2004)
Bini, E., Buttazzo, G.C., Buttazzo, G.M.: Rate monotonic analysis: the hyperbolic bound. IEEE Trans. Comput. 52(7), 933–942 (2003)
Bucci, G., Fedeli, A., Sassoli, L., Vicario, E.: Timed state space analysis of real-time preemptive systems. IEEE Trans. Softw. Eng. 30(2), 97–111 (2004)
Duan, Z., Tian, C.: A unified model checking approach with projection temporal logic. In: Liu, S., Araki, K. (eds.) ICFEM 2008. LNCS, vol. 5256, pp. 167–186. Springer, Heidelberg (2008)
Duan, Z., Yang, X., Koutny, M.: Framed temporal logic programming. Sci. Comput. Program. 70(1), 31–61 (2008)
Han, M., Duan, Z., Wang, X.: Time constraints with temporal logic programming. In: Aoki, T., Taguchi, K. (eds.) ICFEM 2012. LNCS, vol. 7635, pp. 266–282. Springer, Heidelberg (2012)
Huang, Y., Ferreira, J.F., He, G., Qin, S., He, J.: Deadline analysis of AUTOSAR OS periodic tasks in the presence of interrupts. In: Groves, L., Sun, J. (eds.) ICFEM 2013. LNCS, vol. 8144, pp. 165–181. Springer, Heidelberg (2013)
Labrosse, J.J.: uC/OS-III: The Real-Time Kernel. Micrium Press, Weston (2009)
Liu, C.L., Layland, J.W.: Scheduling algorithms for multiprogramming in a hard-real-time environment. J. ACM (JACM) 20(1), 46–61 (1973)
Madl, G., Dutt, N., Abdelwahed, S.: A conservative approximation method for the verification of preemptive scheduling using timed automata. In: 2009 15th IEEE Real-Time and Embedded Technology and Applications Symposium, RTAS 2009, pp. 255–264 (2009)
Miku00ionis, M., Larsen, K.G., Rasmussen, J.I., Nielsen, B., Skou, A., Palm, S.U., Pedersen, J.S., Hougaard, P.: Schedulability analysis using uppaal: Herschel-planck case study. In: Proceedings of the 4th International Conference on Leveraging Applications of Formal Methods, Verification, and Validation - Volume Part II (2010)
Pang, T., Duan, Z., Tian, C.: Symbolic model checking for propositional projection temporal logic. In: 2012 Sixth International Symposium on Theoretical Aspects of Software Engineering (TASE), pp. 9–16. IEEE (2012)
Rasmus, R.V., Trick, M.A.: Round robin scheduling-a survey. Eur. J. Oper. Res. 188(3), 617–636 (2008)
Tian, C., Duan, Z.: Propositional Projection Temporal Logic, B\({\ddot{u}}\)chi Automata and \(\omega \)-Regular Expressions. In: Agrawal, M., Du, D.-Z., Duan, Z., Li, A. (eds.) TAMC 2008. LNCS, vol. 4978, pp. 47–58. Springer, Heidelberg (2008)
Wasziwoski, L., Hanzalek, Z.: Model checking of multitasking real-time applications based on the timed automata model using one clock. Behavioral Modeling for Embedded Systems and Technologies: Applications for Design and Implementation: Applications for Design and Implementation, p. 194 (2009)
Waszniowski, L., Krákora, J., Hanzálek, Z.: Case study on distributed and fault tolerant system modeling based on timed automata. J. Syst. Softw. 82(10), 1678–1694 (2009)
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Cui, J., Duan, Z., Tian, C., Zhang, N., Zhou, C. (2015). Model Checking \(\mu \)C/OS-III Multi-task System with TMSVL. In: Butler, M., Conchon, S., Zaïdi, F. (eds) Formal Methods and Software Engineering. ICFEM 2015. Lecture Notes in Computer Science(), vol 9407. Springer, Cham. https://doi.org/10.1007/978-3-319-25423-4_12
Download citation
DOI: https://doi.org/10.1007/978-3-319-25423-4_12
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-25422-7
Online ISBN: 978-3-319-25423-4
eBook Packages: Computer ScienceComputer Science (R0)