扩展线性时段不变式是时段演算中的一类重要公式.时段演算是周巢尘院士于20世纪90年代提出的一种用于嵌入式实时软件设计的演算系统,它开创性地将积分概念引入计算机实时软件的分析中,从而能够描述处理连续时间区间性质,是国际上公认的描述和分析实时系统的主流方法之一.由于时段演算内容丰富并且相关的综述和专著已出版,文章旨在对扩展线性时段不变式这一时段演算子集的模型检验问题的研究情况进行论述:①介绍时段演算、线性不变式及其扩展;②分别论述线性时段不变式以及扩展线性时段不变式的模型检验研究情况,其中重点介绍扩展的线性时段不变式,在离散时间语义和连续时间语义下的近期验证成果.
Abstract
Extended Linear Duration Invariants (ELDIs) is an important subset of Duration Calculus(DC), proposed by academician Chaochen Zhou in 1990s. It introduces the notion of duration, the integral of state expression over the reference interval, and has become one of the main methods to specify and analyze real-time systems. Due to the rich content of DC and the publication of related reviews and monographs, we hereby focus on the research process of model checking of ELDIs. In this paper, we first introduce DC, LDIs and their extensions, and then discuss the research on model checking of LDIs and ELDIs, with emphasis on recent achievements in model checking of ELDIs in discrete time and continuous time semantics.
关键词
时段演算 /
扩展线性时段不变式 /
模型检验 /
实时系统
{{custom_keyword}} /
Key words
Duration Calculus /
Extended Linear Duration Invariants /
model checking /
realtime systems
{{custom_keyword}} /
{{custom_sec.title}}
{{custom_sec.title}}
{{custom_sec.content}}
参考文献
[1] Zhou C, Hoare C A R, Ravn A P. A calculus of durations[J]. Information Processing Letters, 1991, 40(5):269-276.
[2] Halpern J Y, Manna Z, Moszkowski B C. A hardware semantics based on temporal intervals[C]∥Proceedings of the International Colloquium on Automata, Languages and Programming (ICALP), 1983: 278-291.
[3] Zhou C, Ravn A P, Hansen M R. An extended duration calculus for hybrid real-time systems[C]∥Proceedings of the Workshop on Hybrid Systems, 1992: 36-59.
[4] Zhou C, Li X. A mean-value duration calculus[C]∥Proceedings of a Classical Mind, Essays in Honour of C.A. R. Hoare, 1994: 431-451.
[5] Liu Z, Ravn A P, Sorensen E V, et al. Towards a calculus of systems dependability[J]. Journal of High Integrity Systems, 1994, 1(1): 49-65.
[6] Zhan N. A higher-order duration calculus and its completeness[J]. Science in China, 2000, 43(6):625-640.
[7] Meyer R, Faber J, Hoenicke J, et al. Model checking duration calculus: A practical approach[J]. Formal Aspects of Computing, 2008, 20(4):481-505.
[8] Zhou C, Hansen M R. Duration Calculus: A formal approach to real-time systems[M]. Berlin:Springer, 2004.
[9] 李晓山, 周巢尘. 时段演算综述[J]. 计算机学报, 1994, 11:842-851.
[10]Zhou C, Hansen M R, Sestoft P. Decidability and undecidability results for Duration Calculus[C]∥Proceedings of the Symposium on Theoretical Aspects of Computer Science (STACS), 1993: 58-68.
[11]Fr nzle M. Model-checking dense-time Duration Calculus[J]. Formal Aspects of Computing, 2004, 16(2):121-139.
[12]Fr nzle M, Hansen M R. Deciding an interval logic with accumulated durations[C]∥Proceedings of the 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), 2007: 201-215.
[13]Hansen M R. Model-checking discrete Duration Calculus[J]. Formal Aspects of Computing, 1994, 6(1):826-845.
[14]Pandya P K. Finding extremal models of discrete Duration Calculus formulae using symbolic search[J]. Electronic Notes in Theoretical Computer Science, 2005, 128(6):247-262.
[15]Sharma B, Pandya P K, Chakraborty S. Bounded validity checking of interval duration logic[C]∥Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2005: 301-316.
[16]Zhou C, Zhang J, Yang L, et al. Linear duration invariants[C]∥Proceedings of the 3rd International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT), 1994: 86-109.
[17]Clarke E M, Emerson E A, Sistla A P. Automatic verification of finite-state concurrent systems using temporal logic specifications[J]. ACM Transactions on Programming Languages and Systems, 1986, 8(2):244-263.
[18]Queille J P, Sifakis J. Specification and verification of concurrent systems in CESAR[C]∥Proceedings of the 5th International Symposium on Programming, 1982: 337-351.
[19]Clarke E M, Grumberg O, Peled D A. Model checking[M]. Boston:MIT Press, 1999.
[20]Dima C. Real-time automata[J]. Journal of Automata, Languages and Combinatorics, 2001, 6(1): 3-24.
[21]Alur R, Dill DL. A theory of timed automata[J]. Theoretical Computer Science, 1994,126(2):183-235.
[22]Braberman V A, Huang D V. On checking timed automata for linear duration invariants[C]∥Proceedings of the 19th IEEE Real-Time Systems Symposium (RTSS), 1998: 264-273.
[23]Li X D, Huang D V. Checking linear duration invariants by linear programming[C]∥Proceedings of Concurrency and Parallelism, Programming, Networking, and Security: 2nd Asian Computing Science Conference (ASIAN), 1996: 321-332.
[24]Li X D, Huang D V, Zheng T. Checking hybrid automata for linear duration invariants[C]∥Proceedings of Advances in Computing Science: 3rd Asian Computing Science Conference (ASIAN), 1997: 166-180.
[25]Henzinger T A. The theory of hybrid automata[C]∥Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science (LICS), 1996: 278-292.
[26]Thai P, Hung D V. Verifying linear duration constraints of timed automata[C]∥Proceedings of the 1st International Colloquium on Theoretical Aspects of Computing (ICTAC), 2004: 295-209.
[27]Zhang M, Hung D V, Liu Z. Verification of linear duration invariants by model checking CTL properties[C]∥Proceedings of the 5th International Colloquium on Theoretical Aspects of Computing (ICTAC), 2008: 395-409.
[28]Zhang M, Liu Z, Zhan N. Model checking linear duration invariants of networks of automata[C]∥Proceedings of the 3rd International IPM Conference on Fundamentals of Software Engineering (FSEN), 2009: 244-259.
[29]Fr nzle M, Hansen M R. Efficient model checking for Duration Calculus based on branching-time approximations[C]∥Proceedings of the 6th IEEE International Conference on Software Engineering and Formal Methods (SEFM), 2008: 63-72.
[30]Fr nzle M, Hansen M R. Efficient model checking for Duration Calculus?[J]. International Journal of Software and Informatics, 2009, 3(2/3):171-196.
[31]Zu Q, Zhang M, Zhu J, et al. Bounded model-checking of discrete Duration Calculus[C]∥Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control (HSCC), 2013:213-222.
[32]Clarke E M, Emerson E A. Design and synthesis of synchronization skeletons using branching time temporal logic[J]. Lecture Notes on Computer Science, 1981, 131:52-71.
[33]Larsen K G, Pettersson P, Wang Y. Uppaal in a nutshell[J]. International Journal on Software Tools for Technology Transfer, 1997, 1(1):134-152.
[34]An J, Zhan N, Li X, et al. Model checking bounded continuous-time extended linear duration invariants[C]∥Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (HSCC), 2018: 81-90.
[35]Bengtsson J, Wang Y. Timed automata: Semantics, algorithms and tools[C]∥Lectures on Concurrency and Petri Nets, 2003: 87-124.
[36]Tarski A. A decision method for elementary algebra and geometry[M]. Berkeley: University of California Press, 1951.
[37]安杰,张苗苗.基于实时自动机的连续时段演算的验证[J]. 软件学报, 2019, 30(7): 1953-1965.
{{custom_fnGroup.title_cn}}
脚注
{{custom_fn.content}}
基金
国家自然科学基金资助项目(61472279)
{{custom_fund}}
PDF(1251 KB)
