From Hybrid Data-Flow Languages to Hybrid Automata: A Complete Translation

被引:0
作者
Schrammel, Peter [1 ]
Jeannet, Bertrand [1 ]
机构
[1] INRIA Grenoble Rhone Alpes, F-38330 Montbonnot St Martin, France
来源
HSCC 12: PROCEEDINGS OF THE 15TH ACM INTERNATIONAL CONFERENCE ON HYBRID SYSTEMS: COMPUTATION AND CONTROL | 2012年
关键词
Data-Flow Languages; Hybrid Systems; Hybrid Automata; Verification;
D O I
暂无
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
Hybrid systems are used to model embedded computing systems interacting with their physical environment. There is a conceptual mismatch between high-level hybrid system languages like SIMULINK, which are used for simulation, and hybrid automata, the most suitable representation for safety verification. Indeed, in simulation languages the interaction between discrete and continuous execution steps is specified using the concept of zero-crossings, whereas hybrid automata exploit the notion of staying conditions. We describe a translation from a hybrid data-flow language to logico-numerical hybrid automata that points out this issue carefully. We expose various zero-crossing semantics, propose a sound translation, and discuss to which extent the original semantics is preserved.
引用
收藏
页码:167 / 176
页数:10
相关论文
共 32 条
[1]  
Acary V, 2008, LECT NOTES APPL COMP, V35, P1, DOI 10.1007/978-3-540-75392-6
[2]  
Agrawal A., 2004, ENTCS, V109
[3]  
Alur R., 2008, EMBEDDED SOFTWARE
[4]  
[Anonymous], THEO COMPUTER SCI
[5]   Not necessarily closed convex polyhedra and the double description method [J].
Bagnara, R ;
Hill, PM ;
Zaffanella, E .
FORMAL ASPECTS OF COMPUTING, 2005, 17 (02) :222-257
[6]  
Benveniste A., 2010, C DEC CONTR
[7]  
Benveniste A., 2011, LCTES
[8]  
Briand X., 2010, COMPUTER AIDED DESIG, V29
[9]  
Caspi P., 1987, POPL
[10]  
CHUTINAN A, 1999, LNCS, V1569