Verifying a scheduling protocol of safety-critical systems. (English) Zbl 1423.90101

Summary: It is of great importance to ensure safety and reliability of the scheduling protocol of safety-critical systems since the failure will cause serious damage. This paper analyzes a real-time scheduling protocol of a safety-critical system and models it using a modeling, simulation and verification language program. Further, the schedulability and other desired properties are specified using propositional projection temporal logic formulas. As a result, these properties are proved with theorem proving and further verified using the runtime verification approach at code level.


90B35 Deterministic scheduling theory in operations research
68M20 Performance evaluation, queueing, and scheduling in the context of computer systems
Full Text: DOI


[1] Ahmed W, Hasan O, Tahar S (2015) Formal reliability analysis of wireless sensor network data transport protocols using HOL. In: IEEE international conference on wireless and mobile computing, networking and communications, pp 217-224
[2] Angeletti, D.; Giunchiglia, E.; Narizzano, M.; Puddu, A.; Sabina, S., Using bounded model checking for coverage analysis of safety-critical software in an industrial setting, J Autom Reason, 45, 397-414, (2010)
[3] Armando A, Mantovani J, Platania L (2006) Bounded model checking of software using SMT solvers instead of SAT solvers. In: Valmari A (ed) Model checking software. SPIN 2006. Lecture notes in computer science, vol 3925. Springer, Berlin, Heidelberg, pp 146-162 · Zbl 1178.68148
[4] Bernardeschi, C.; Domenici, A., Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system, Inf Process Lett, 116, 409-415, (2016) · Zbl 1356.68177
[5] Bertot Y, Castéran P (2004) Interactive theorem proving and program development. Springer, New York · Zbl 1069.68095
[6] Beyer D, Keremoglu ME (2011) CPAchecker: a tool for configurable software verification. In: Gopalakrishnan G, Qadeer S (eds) Computer aided verification. CAV 2011. Lecture notes in computer science, vol 6806. Springer, Berlin, Heidelberg, pp 184-190
[7] Blech, JO; Ould Biha, S.; Barthe, G. (ed.); Pardo, A. (ed.); Schneider, G. (ed.), Verification of PLC properties based on formal semantics in Coq, 58-73, (2011), Berlin
[8] Brockschmidt M, Cook B, Ishtiaq S, Khlaaf H, Piterman N (2016) T2: temporal property verification. In: International conference on tools and algorithms for the construction and analysis of systems, Springer, pp 387-393
[9] Chen, L.; Jiao, J.; Wei, Q.; Zhao, T., An improved formal failure analysis approach for safety-critical system based on MBSA, Eng Fail Anal, 82, 713-725, (2017)
[10] Cimatti, A.; Clarke, E.; Giunchiglia, F.; Roveri, M., NuSMV: a new symbolic model checker, Int J Softw Tools Technol Transf, 2, 410-425, (2000) · Zbl 1059.68582
[11] Clarke E, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: International conference on computer aided verification, Springer, pp 154-169 · Zbl 0974.68517
[12] Clarke, EM; Emerson, EA; Sistla, AP, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Trans Program Lang Syst (TOPLAS), 8, 244-263, (1986) · Zbl 0591.68027
[13] Clarke EM, Grumberg O, Peled D (1999) Model checking. MIT press, Cambridge
[14] Dietsch D, Heizmann M, Langenfeld V, Podelski A (2015) Fairness modulo theory: a new approach to LTL software model checking. In: Computer aided verification · Zbl 1381.68157
[15] Duan Z (1996) An extended interval temporal logic and a framing technique for temporal logic programming. PhD thesis, University of Newcastle upon Tyne
[16] Duan Z (2005) Temporal logic and temporal logic programming. Science Press, Henderson
[17] Duan, Z.; Koutny, M., A framed temporal logic programming language, J Comput Sci Technol, 19, 341-351, (2004)
[18] Duan, Z.; Tian, C., A practical decision procedure for propositional projection temporal logic with infinite models, Theor Comput Sci, 554, 169-190, (2014) · Zbl 1358.68188
[19] Duan, Z.; Yang, X.; Koutny, M., Framed temporal logic programming, Sci Comput Program, 70, 31-61, (2008) · Zbl 1131.68036
[20] 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
[21] Duan Z, Tian C, Zhang N (2016) A canonical form based decision procedure and model checking approach for propositional projection temporal logic. Elsevier, New York · Zbl 1370.68200
[22] Gordon, MJC; Melham, TF, Introduction to HOL: a theorem proving environment for higher order logic, IEEE Trans Reliab, 89, 317-320, (1993) · Zbl 0779.68007
[23] Holzmann, GJ, The model checker SPIN, IEEE Trans Software Eng, 23, 279-295, (1997)
[24] Kaufmann, M.; Moore, JS; Mohamed, OA (ed.); Muñoz, C. (ed.); Tahar, S. (ed.), An ACL2 tutorial, 17-21, (2008), Berlin · Zbl 1165.68461
[25] Kroening D, Tautschnig M (2014) CBMC-C bounded model checker. In: Tools and algorithms for construction and analysis of systems
[26] Melham T (1993) Higher order logic and hardware verification. Cambridge University Press, Cambridge · Zbl 0819.68015
[27] Owre S, Rushby JM, Shankar N (1992) PVS: a prototype verification system. In: International conference on automated deduction, Springer, pp 748-752
[28] Paulson LC (1994) Isabelle-a generic theorem prover. Of LNCS. Springer, New York · Zbl 0825.68059
[29] Pnueli A (1977) The temporal logic of programs. In: 18th annual symposium on foundations of computer science, 1977, IEEE, pp 46-57
[30] Richards RJ (2010) Modeling and security analysis of a commercial real-time operating system kernel. Springer, Boston, pp 301-322
[31] Spichkova M, Blech JO, Herrmann P, Schmidt H (2014) Modeling spatial aspects of safety-critical systems with focus-st. In: The workshop on model driven engineering, pp 49-58
[32] Sun J, Liu Y, Dong JS (2008) Model checking CSP revisited: introducing a process analysis toolkit. In: international symposium on leveraging applications of formal methods, verification and validation, Springer, pp 307-322
[33] Tuan LA, Man CZ, Quan TT (2010) Modeling and verification of safety critical systems: a case study on pacemaker. In: Fourth international conference on secure software integration and reliability improvement, pp 23-32
[34] Vardi, MY, Verification of concurrent programs: the automata-theoretic framework, Ann Pure Appl Logic, 51, 79-98, (1991) · Zbl 0725.03013
[35] Wang M, Tian C, Duan Z (2017) Full regular temporal property verification as dynamic program execution. In: Proceedings of the 39th international conference on software engineering, ICSE 2017, Buenos Aires, Argentina, May 20-28, 2017—companion volume, pp 226-228
[36] Wang, X.; Tian, C.; Duan, Z.; Zhao, L., MSVL: a typed language for temporal logic programming, Front Comput Sci, 11, 762-785, (2017)
[37] Yang K, Duan Z, Tian C, Zhang N (2017) A compiler for MSVL and its applications. Theor Comput Sci. https://doi.org/10.1016/j.tcs.2017.07.032 · Zbl 1407.68096
[38] Yang, X.; Duan, Z., Operational semantics of framed temporal logic programs, Logic Program Proceed, 3668, 356-370, (2007) · Zbl 1131.68407
[39] Yasmeen A, Feigh KM, Gelman G, Gunter EL (2012) Formal analysis of safety-critical system simulations. In: International conference on application and theory of automation in command and control systems, ATACCS ’12, London, UK, May 29-31, 2012, pp 71-81
[40] Zhang, N.; Yang, M.; Gu, B.; Duan, Z.; Tian, C., Verifying safety critical task scheduling systems in PPTL axiom system, J Comb Optim, 31, 1-27, (2014) · Zbl 1333.90055
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.