HyTech: A model checker for hybrid systems

被引：329

作者：

Henzinger T.A. ^{[1
]}

Ho P.-H. ^{[2
]}

Wong-Toi H. ^{[3
]}

机构：

[1] EECS Department, University of California, Berkeley

[2] Strategic CAD Labs, Intel Corp, Hillsboro, OR 97124

[3] Cadence Berkeley Labs, Berkeley, CA 94704, 2001 Addison Street, Third Fl.

来源：

International Journal on Software Tools for Technology Transfer | 1997年 / 1卷 / 1-2期

基金：

美国国家科学基金会;

关键词：

Hybrid automata; Hybrid systems; hytech; Symbolic model checking;

D O I：

10.1007/s100090050008

中图分类号：

学科分类号：

摘要：

A hybrid system is a dynamical system whose behavior exhibits both discrete and continuous change. A hybrid automaton is a mathematical model for hybrid systems, which combines, in a single formalism, automaton transitions for capturing discrete change with differential equations for capturing continuous change. HyTech is a symbolic model checker for linear hybrid automata, a subclass of hybrid automata that can be analyzed automatically by computing with polyhedral state sets. A key feature of HyTech is its ability to perform parametric analysis, i.e., to determine the values of design parameters for which a linear hybrid automaton satisfies a temporal-logic requirement. © 1997 Springer-Verlag.

引用

页码：110 / 122

页数：12

共 38 条

[1]

Alur R., Courcoubetis C., Dill D., Model checking in dense real time, Information and Computation, 104, 1, pp. 2-34, (1993)

[2]

Alur R., Courcoubetis C., Halbwachs N., Henzinger T., Ho P.-H., Nicollin X., Olivero A., Sifakis J., Yovine S., The algorithmic analysis of hybrid systems, Theoretical Computer Science, 138, pp. 3-34, (1995)

[3]

Alur R., Courcoubetis C., Henzinger T., Ho P.-H., Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems, Hybrid Systems I, pp. 209-229, (1993)

[4]

Alur R., Dill D., A theory of timed automata, Theoretical Computer Science, 126, pp. 183-235, (1994)

[5]

Alur R., Henzinger T., Ho P.-H., Automatic symbolic verification of embedded systems, IEEE Transactions on Software Engineering, 22, 3, pp. 181-201, (1996)

[6]

Alur R., Henzinger T., Real-time system-discrete system + clock variables, Software Tools for Technology Transfer, 1, 1-2, pp. 86-109, (1997)

[7]

Alur R., Kurshan R., Timing analysis in Cospan, Hybrid Systems III, 1066, pp. 220-231, (1996)

[8]

Balarin F., Sangiovanni-Vincentelli A., Iterative algorithms for formal verification of embedded real-time systems, Proceedings of the International Conference on Computer-aided Design (ICCAD), pp. 450-457, (1994)

[9]

Bengtsson J., Larsen K., Larsson F., Pettersson P., Yi W., Uppaal: A tool-suite for automatic verification of real-time systems, Hybrid Systems III, 1066, pp. 232-243, (1996)

[10]

Burch J., Clarke E., McMillan K., Dill D., Hwang L., Symbolic model checking: 10<sup>20</sup> states and beyond, Information and Computation, 98, 2, pp. 142-170, (1992)

← 1 2 3 4 →