Deductive Schedulability Verification Methodology of Real-Time Software using both Refinement Verification and Hybrid Automata

• Yamane, Satoshi

Abstract

Real-time software runs over real-time operating systems, and guaranteeing Qualities is difficult. As timing constraints and resource allocations are strict, it is necessary to verify schedulability, safety and liveness properties. In this paper, we formally specify real-time software using hybrid automata and verify its schedulability using both deductive refinement theory and scheduling theory. In this case, the above real-time software consists of periodic processes and a fixed-priority preemptive scheduling policy on one CPU. Using our proposed methods, we can uniformally and easily specify real-time software and verify its schedulability based on hybrid automata. Moreover, we can verify its schedulability at design stage.

Journal

• Proceedings - IEEE Computer Society's International Computer Software and Applications Conference

  Proceedings - IEEE Computer Society's International Computer Software and Applications Conference 527-533, 2003-01-01

  Institute of Electrical and Electronics Engineers (IEEE)

Details

• CRID: 1050574047082305408
• NII Article ID: 120006655572
• ISSN: 07306512
• Web Site: http://hdl.handle.net/2297/6708
• Text Lang: en
• Article Type: conference paper
• Data Source:
  • IRDB
  • CiNii Articles