Verifying safety critical task scheduling systems in PPTL axiom system

详细信息    查看全文

• 作者：Nan Zhang ; Mengfei Yang ; Bin Gu ; Zhenhua Duan…
• 关键词：Theorem proving ; Scheduler ; Real ; time ; Safety critical system
• 刊名：Journal of Combinatorial Optimization
• 出版年：2016
• 出版时间：February 2016
• 年：2016
• 卷：31
• 期：2
• 页码：577-603
• 全文大小：618 KB
• 参考文献：Bertot Y, Castéran P (2004) Interactive theorem proving and program development. Springer-Verlag, Berlin, Heidelberg
  Brock B, Kaufmann M, Moore J (1996) Acl2 theorems about commercial microprocessors. In: Srivas M, Camilleri A (eds) Proceedings of the 1st international conference on formal methods in computer-aided design. Springer-Verlag, London, pp 275–293
  Duan Z (2005) Temporal logic and temporal logic programming. Science Press, Beijing
  Duan Z, Zhang N, Koutny M (2013) A complete proof system for propositional projection temporal logic. Theoret Comput Sci 497:84–107MathSciNet CrossRef MATH
  Gordon M, Melham T (1993) Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, Cambridge
  Holzmann G (1997) The model checker spin. IEEE Trans Softw Eng 23(5):279–295MathSciNet CrossRef
  McMillan K (1993) Symbolic model checking: an approach to the state explosion problem. Kluwer Academic, DordrechtCrossRef
  Owre S, Rushby J (1992) Pvs: a prototype verification system. In: Kapur D (ed) Proceedings of the 11th international conference on automated deduction. Springer-Verlag, Heidelberg, pp 748–752
  Paulson L (1994) Isabelle—a generic theorem prover. Springer, BerlinMATH
  Sistla A (1983) Theoretical issues in the design and verification of distributed systems. PhD thesis, Harvard University
  Tian C, Duan Z (2009) Complexity of propositional projection temporal logic with star. Math Str Comput Sci 19(1):73–100MathSciNet CrossRef MATH
  Vardi M (1988) A temporal fixpoint calculus. In: POPL ’88 Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM, New York, pp 250–259
  Wolper P (1983) Temporal logic can be more expressive. Info Control 56:72–99MathSciNet CrossRef MATH
  
• 作者单位：Nan Zhang (1)
  Mengfei Yang (2)
  Bin Gu (2)
  Zhenhua Duan (1)
  Cong Tian (1)
  
  1. Institute of Computing Theory and Technology and ISN Lab, Xidian University, Xi’an, 710071, China
  2. China Academy of Space Technology, Beijing, 100094, China
  
• 刊物类别：Mathematics and Statistics
• 刊物主题：Mathematics
  Combinatorics
  Convex and Discrete Geometry
  Mathematical Modeling and IndustrialMathematics
  Theory of Computation
  Optimization
  Operation Research and Decision Theory
  
• 出版者：Springer Netherlands
• ISSN：1573-2886

文摘

This paper presents a case study of formal verification of safety critical task scheduling systems. First, a scheduling algorithm described in a temporal logic programming language is presented; then a sufficient and necessary condition for the schedulability of task set is formalized. Further, the correctness of the condition is proved by means of theorem proving in the axiom system of Propositional Projection Temporal Logic. Keywords Theorem proving Scheduler Real-time Safety critical system