微信服务号

微信订阅号

2025-5-2- 5
Home > Archive>Volume 22, Issue 6, 2011 >1236-1251. DOI:10.3724/SP.J.1001.2011.04015
PDF HTML XML Export Cite reminder
Schedulability Analysis Tool for Distributed Real-Time Systems Based on Automata Theory
Author:
Affiliation:

  • Article
    • | |
  • Metrics
    • |
  • Reference [32]
    • |
  • Related [20]
    • |
  • Cited by [1]
    • | |
  • Comments
    Abstract:

    Distributed systems are complicated real-time systems, which have been used in many safety-critical domains. In order to ensure the real-time constraints over the tasks running on these systems, the traditional schedulability analysis techniques, based on worst-case response time analysis, usually consider the worst case which could never occur in real world applications, and therefore the obtained results are pessimistic. The model checking technique based on automata theory could exhaustively search the whole system state space and return precise results. By using formal methods to analyze the schedulability of tasks on distributed systems, this paper presents the formal task model on distributed systems. It uses action automata and environment automata to model the task execution semantics and the external event arrival patterns respectively. It also translates the schedulability analysis to the reachability analysis of the locations in automata network, and proves the decidability of schedulability under certain scheduling policies with attached conditions and scope. Based on these conclusions, the formal check model implements a schedulability check tool, SCT (schedulability checking tool), and compares it with other techniques and tools on accurateness and performance. The comparisons show that SCT always provides the most accurate results but with the longest execution time.

    Reference
    [1] Liu CL, Layland JW. Scheduling algorithms for multiprogramming in a hard real-time environment. Journal of the ACM, 1973,20(1):46?61. [doi: 10.1145/321738.321743]
    [2] Audsley N, Burns A, Richardson M, Tindell K, Wellings AJ. Applying new scheduling theory to static priority preemptive scheduling. Software Engineering Journal, 1993,8(5):284?292. [doi: 10.1049/sej.1993.0034]
    [3] Lehoczky JP. Fixed priority scheduling of periodic task sets with arbitrary deadlines. In: Proc. of the 11th RTSS. IEEE Press, 1990. 201?209. [doi: 10.1109/REAL.1990.128748]
    [4] Clarke EM, Grumberg O, Peled DA. Model Checking. Cambridge: MIT Press, 1999.
    [5] Alur R, Dill DL. A theory of timed automata. Theoretical Computer Science, 1994,126(2):183?235. [doi: 10.1016/0304-3975(94)90010-8]
    [6] Fehnker A. Scheduling a steel plant with timed automata. In: Proc. of the 6th RTCSA. Los Alamitos: IEEE Press, 1999. 280?286. [doi: 10.1109/RTCSA.1999.811256]
    [7] Cassez F, Laroussinie F. Model checking for hybrid systems by quotienting and constraints solving. In: Emerson EA, Sistla AP, eds. Proc. of the 12th CAV. LNCS 1855, Heidelberg: Springer-Verlag, 2000. 373?388. [doi: 10.1007/10722167_29]
    [8] Alur R, Courcoubetis C, Halbwachs N, Henzinger TA, Ho PH, Nicollin X, Olivero A, Sifakis J, Yovine S. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 1995,138(1):3?34. [doi: 10.1016/0304-3975(94)00202-T]
    [9] Behrmann G, David A, Larsen KG. A tutorial on UPPAAL. In: Proc. of the 4th Int’l School on Formal Methods for the Design of Computer, Communication, and Software Systems. LNCS 3185, Heidelberg: Springer-Verlag, 2004. 200?236.
    [10] Hendriks M, Verhoef M. Timed automata based analysis of embedded system architectures. In: Proc. of the 20th IPDPS. IEEE Press, 2006. 268?275. [doi: 10.1109/IPDPS.2006.1639422]
    [11] Cassez F, Larsen KG. The impressive power of stopwatches. In: Palamidessi C, ed. Proc. of the 11th CONCUR. LNCS 1877, Heidelberg: Springer-Verlag, 2000. 138?152.
    [12] Fersman E, Krcal P, Pettersson P, Wang Y. Task automata: Schedulability, decidability and undecidability. Information and Computation, 2007,205(8):1149?1172. [doi: 10.1016/j.ic.2007.01.009]
    [13] Amnell T, Fersman E, Mokrushin L, Pettersson P, Wang Y. TIMES: A tool for schedulability analysis and code generation of realtime systems. In: Larsen KG, Niebert P, eds. Proc. of the 1st FORMATS. LNCS 2791, Heidelberg: Springer-Verlag, 2004. 60?72. [doi: 10.1007/978-3-540-40903-8_6]
    [14] Krcal P, Stigge M, Wang Y. Multi-Processor schedulability analysis of preemptive real-time tasks with variable execution times. In: Raskin J, Thiagarajan PS, eds. Proc. of the 5th FORMATS. LNCS 4763, Heidelberg: Springer-Verlag, 2007. 274?289. [doi: 10.1007/978-3-540-75454-1_20]
    [15] Fersman E, Mokrushin L, Pettersson P, Wang Y. Schedulability analysis of fixed-priority systems using timed automata. Theoretical Computer Science, 2006,354(2):301?317. [doi: 10.1016/j.tcs.2005.11.019]
    [16] Hamann A, Henia R, Racu R, Jersak M, Richter K, Ernst R. SymTA/S-Symbolic timing analysis for systems. In: WIP Proc. of the 16th ECRTS. Catania: IEEE Press, 2004. 17?20.
    [17] Tindell K, Clark J. Holistic schedulability analysis for distributed hard real-time systems. Microprocessing and Microprogramming, 1994,40(2-3):117?134. [doi: 10.1016/0165-6074(94)90080-9]
    [18] Richter K, Ernst R. Event model interfaces for heterogeneous system analysis. In: Proc. of the DATE. IEEE Press, 2002. 506?513. [doi: 10.1109/DATE.2002.998348]
    [19] Thiele L, Chakraborty S, Naedele M. Real-Time calculus for scheduling hard real-time systems. In: Proc. of the IEEE Int’l Symp. on Circuits and Systems. Washington: IEEE Press, 2000. 101?104. [doi: 10.1109/ISCAS.2000.858698]
    [20] Le Boudec JL. Application of network calculus to guaranteed service networks. IEEE Trans. on Information Theory, 1998,44(3): 1087?1096. [doi: 10.1109/18.669170]
    [21] Perathoner S, Wandeler E, Thiele L, Hamann A, Schliecker S, Henia R, Racu R, Ernst R, Harbour MG. Influence of different system abstraction on the performance analysis of distributed real-time systems. In: Proc. of the 7th EMSOFT. New York: ACM Press, 2007. 193?202. [doi: 10.1145/1289927.1289959]
    [22] Henzinger TA, Nicollin X, Sifakis J, Yovine S. Symbolic model checking for real-time systems. Information and Computation, 1994, 111(2):193?244. [doi: 10.1006/inco.1994.1045]
    [23] Tripakis S, Yovine S. Analysis of timed systems using time-abstracting bisimulations. Formal Methods in System Design, 2001, 18(1):25?68. [doi: 10.1023/A:1008734703554]
    [24] Larsen KG, Larsen F, Pettersson P, Wang Y. Compact data structures and state-space reduction for model-checking real-time systems. Int’l Journal of Time-Critical Computing Systems, 2003,25(2):255?275. [doi: 10.1023/A:1025132427497]
    [25] Behrmann G, Larsen KG, Pearson J, Weise C, Wang Y. Efficient timed reachability analysis using clock difference diagrams. In: Halbwachs N, Peled D, eds. Proc. of the 11th CAV. LNCS 1633, Heidelberg: Springer-Verlag, 1999. 341?353. [doi: 10.1007/3-540-48683-6_30]
    [26] Sha L, Rajkumar R, Lehoczky JP. Priority inheritance protocols: An approach to real-time synchronization. IEEE Trans. on Computers, 1990,39(9):1175?1185. [doi: 10.1109/12.57058]
    [27] Larsen KG, Pettersson P, Wang Y. Compositional and symbolic model-checking of real-time systems. In: Proc. of the 16th RTSS. Pisa: IEEE Press, 1995. 76?89. [doi: 10.1109/REAL.1995.495198]
    [28] McManis J, Varaiya P. Suspension automata: A decidable class of hybrid automata. In: Dill DL, ed. Proc. of the 6th CAV. LNCS 818, Heidelberg: Springer-Verlag, 1994. 105?117. [doi: 10.1007/3-540-58179-0_47]
    [29] Henzinger TA, Kopke PW, Puri A, Varaiya P. What’s decidable about hybrid automata? In: Proc. of the 27th ACM Symp. on Theory of Computing. New York: ACM Press, 1995. 373?382. [doi: 10.1145/225058.225162]
    [30] Henzinger TA. Hybrid automata with finite bisimulations. In: Fül?p Z, Gécseg F, eds. Proc. of the 22nd ICALP. LNCS 944, Heidelberg: Springer-Verlag, 1995. 324?335. [doi: 10.1007/3-540-60084-1_85]
    [31] Dill DL. Timing assumptions and verification of finite-state concurrent systems. In: Sifakis J, ed. Proc. of the Int’l Workshop on Automatic Verification Methods for Finite State Systems. LNCS 407, Heidelberg: Springer-Verlag, 1989. 197?212. [doi: 10.1007/3-540-52148-8_17]
    [32] Alur R. Timed automata. In: Halbwachs N, Peled D, eds. Proc. of the 11th Int’l Conf. on Computer Aided Verification. LNCS 1633, Heidelberg: Springer-Verlag, 1999. 8?22. [doi: 10.1007/3-540-52148-8_17]
    Comments
    Comments
    分享到微博
    Submit
Get Citation

桂盛霖,罗蕾,李允,于淼,徐建华.基于自动机理论的分布式实时调度分析工具.软件学报,2011,22(6):1236-1251

Copy
Share
Article Metrics
  • Abstract:8830
  • PDF: 8780
  • HTML: 0
  • Cited by: 0
History
  • Received:July 09,2010
  • Revised:March 29,2011
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2041554Visitors
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