×

zbMATH — the first resource for mathematics

A formal proof of the deadline driven scheduler in PPTL axiomatic system. (English) Zbl 1360.68771
Summary: This paper presents an approach for verifying the correctness of the feasibility theorem on the deadline driven scheduler (DDS) with the axiom system of Propositional Projection Temporal Logic (PPTL). To do so, the deadline driven scheduling algorithm is modeled by an MSVL (Modeling, Simulation and Verification Language) program and the feasibility theorem is formulated by PPTL formulas with two parts: a necessary part and a sufficient part. Then, several lemmas are abstracted and proved by means of the axiom system of PPTL. With the help of the lemmas, two parts of the theorem are deduced respectively. This case study convinces us that some real-time properties of systems can be formally verified by theorem proving using the axiom system of PPTL.

MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B44 Temporal logic
68M20 Performance evaluation, queueing, and scheduling in the context of computer systems
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Software:
ACL2; CESAR; SPIN; PVS
PDF BibTeX Cite
Full Text: DOI
References:
[1] Clarke, E.; Emerson, E., Design and synthesis of synchronisation skeletons using branching time temporal logic, (Kozen, D., Proceedings of the Workshop on Logic of Programs, (1981), Springer-Verlag Heidelberg), 52-71
[2] Queille, J.; Sifakis, J., Specification and verification of concurrent systems in cesar, (Proceedings of the 5th Colloquium on International Symposium in Programming, (1982), Springer-Verlag London), 337-351 · Zbl 0482.68028
[3] Bledsoe, W. W.; Loveland, D. W., Interactive theorem proving and program development, Contemporary Mathematics Series, vol. 29, (1984), American Mathematical Society Providence · Zbl 0545.00023
[4] Holzmann, G., The model checker spin, IEEE Trans. Softw. Eng., 23, 5, 279-295, (1997)
[5] McMillan, K., Symbolic model checking: an approach to the state explosion problem, (1993), Kluwer Academic Dordrecht
[6] Manna, Z.; Pnueli, A., The temporal logic of reactive and concurrent system, (1992), Springer-Verlag New York
[7] Pnueli, A., The temporal logic of programs, (Proceedings of the 18th Annual Symposium on the Foundations of Computer Science, (1977), IEEE Computer Society Providence), 46-57
[8] Clarke, E.; Emerson, E.; Sistla, A., Automatic verification of finite state concurrent system using temporal logic specification, ACM Trans. Program. Lang. Syst., 8, 2, 244-263, (1986) · Zbl 0591.68027
[9] Owre, S.; Rushby, J.; Shankar, N., Pvs: a prototype verification system, (Kapur, D., Proceedings of the 11th International Conference on Automated Deduction, (1992), Springer-Verlag Heidelberg), 748-752
[10] Brock, B.; Kaufmann, M.; Moore, J., Acl2 theorems about commercial microprocessors, (Srivas, M.; Camilleri, A., Proceedings of the 1st International Conference on Formal Methods in Computer-Aided Design, (1996), Springer-Verlag London), 275-293
[11] Bertot, Y.; CastĂ©ran, P., Interactive theorem proving and program development, (2004), Springer-Verlag Berlin, Heidelberg · Zbl 1069.68095
[12] Coquand, T.; Huet, G., Constructions: a higher order proof system for mechanizing mathematics, (Buchberger, B., Proceedings of EUROCAL’85: European Conference on Computer Algebra, vol. 1: Invited Lectures, (1985), Springer-Verlag Heidelberg), 151-184 · Zbl 0581.03007
[13] Tian, C.; Duan, Z., Expressiveness of propositional projection temporal logic with star, Theor. Comput. Sci., 412, 18, 1729-1744, (2011) · Zbl 1221.03018
[14] Duan, Z.; Koutny, M.; Holt, C., Projection in temporal logic programming, (Pfenning, F., Proceedings of Logic Programming and Automated Reasoning, (1994), Springer-Verlag London), 333-344
[15] Duan, Z., Temporal logic and temporal logic programming, (2005), Science Press Beijing
[16] Duan, Z.; Yang, X.; Koutny, M., Frammed temporal logic programming, Sci. Comput. Program., 70, 1, 31-61, (2008) · Zbl 1131.68036
[17] Moszkowski, B., Executing temporal logic programs, (1986), Cambridge University Press Cambridge · Zbl 0658.68014
[18] Zhang, N.; Duan, Z.; Tian, C., A cylinder computation model for many-core parallel computing, Theor. Comput. Sci., 497, 68-83, (2013) · Zbl 1416.68074
[19] Duan, Z.; Zhang, N.; Koutny, M., A complete proof system for propositional projection temporal logic, Theor. Comput. Sci., 497, 84-107, (2013) · Zbl 1417.03146
[20] Duan, Z.; Tian, C., A unified model checking approach with projection temporal logic, (Liu, S.; Maibaum, T.; Araki, K., Proceedings of the 10th International Conference on Formal Methods and Software Engineering, (2008), Springer-Verlag Heidelberg), 167-186
[21] Wolper, P., On the relation of programs and computations to models of temporal logic, (Proceedings of Temporal Logic in Specification, (1987), Springer-Verlag London), 75-123
[22] Liu, C.; Layland, J., Scheduling algorithm for multiprogramming in a hard real-time environment, J. ACM, 20, 1, 46-61, (1973) · Zbl 0265.68013
[23] Zheng, Y.; Zhou, C., A formal proof of the deadline driven scheduler, (Proceedings of Formal Techniques in Real-Time and Fault-Tolerant Systems, (1994), Springer-Verlag Germany), 756-775
[24] Zhou, C.; Hoare, C.; Ravn, A., A calculus of durations, Inf. Process. Lett., 40, 5, 269-276, (1991) · Zbl 0743.68097
[25] Zhan, N., An intuitive formal proof for deadline driven scheduler, J. Comput. Sci. Technol., 16, 2, 146-158, (2001) · Zbl 0986.68009
[26] Xu, Q.; Zhan, N., Formalising scheduling theories in duration calculus, Nord. J. Comput., 14, 3, 173-201, (2008) · Zbl 1187.68102
[27] Tian, C.; Duan, Z., Complexity of propositional projection temporal logic with star, Math. Struct. Comput. Sci., 19, 1, 73-100, (2009) · Zbl 1161.03008
[28] Duan, Z.; Tian, C.; Zhang, L., A decision procedure for propositional projection temporal logic, Acta Inform., 45, 1, 43-78, (2008) · Zbl 1141.68039
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.