Schedulability Analysis Model for Multiprocessor Real-Time Systems Using UPPAAL
Author:
Affiliation:

Clc Number:

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    Abstract:

    As multiprocessor real-time systems are increasingly applied in safety critical systems, it's important to ensure the correctness of such systems. One key attribute of the correctness of real-time system is the schedulability that guarantees to satisfy the timing requirements. The traditional methods for determining the schedulability are either pessimistic or unsafe. To tackle the drawbacks of those methods, this paper proposes a scheme to achieve the schedulability analysis using model checking. It provides a schedulability analysis framework for multiprocessor real-time system. All the components involved in the schedulability of the system, including the tasks, the execution infrastructure and the dispatching management unit, are modeled as timed automata and implemented in UPPAAL. Further, UPPAAL is employed to verify whether the schedulability property is always satisfied. Symbolic model checking is applied to determine schedulability. However, because of the over-approximation for stopwatches, symbolic model checking cannot be used to disprove schedulability. As a supplement, statistical model checking is used to estimate the probability of non-schedulability and generate concrete counterexamples going along with non-schedulability. Statistical model checking is also used to obtain some performance information when system is schedulable.

    Reference
    Related
    Cited by
Get Citation

代声馨,洪玫,郭兵,杨秋辉,黄蔚,徐保平.多处理器实时系统可调度性分析的UPPAAL模型.软件学报,2015,26(2):279-296

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:July 01,2014
  • Revised:October 31,2014
  • Adopted:
  • Online: February 06,2015
  • Published:
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063