Towards validated real-time software

被引：9

作者：

Bertin, V ^{[1
]}

Poize, M ^{[1
]}

Pulou, J ^{[1
]}

Sifakis, J ^{[1
]}

机构：

[1] France Telecom, Ctr Natl Etud Telecommun, F-38243 Meylan, France

来源：

EUROMICRO RTS 2000: 12TH EUROMICRO CONFERENCE ON REAL-TIME SYSTEMS, PROCEEDINGS | 2000年

关键词：

real-time computing; embedded applications; real-time constraints; compiling; synchronous languages; validation; timed automata; model-checking; external environment modelling;

D O I：

10.1109/EMRTS.2000.854003

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

We present a tool for the design and validation of embedded real-time applications. The tool integrates two approaches, the use of the synchronous programming language ESTEREL far design and the application of model-checking techniques for validation of real-time properties. Validation is carried out on a global formal model (timed automata) Inking into account the effective implementation of the application on the target hardware architecture as well as its external environment behavior.

引用

页码：157 / 164

页数：4

共 10 条

[1]

ALUR R, 1990, LECT NOTES COMPUT SC, V443, P322, DOI 10.1007/BFb0032042

[2]

BAUER JC, 1997, P 8 INT C SIGN PROC, P1032

[3] THE SYNCHRONOUS APPROACH TO REACTIVE AND REAL-TIME SYSTEMS [J].

BENVENISTE, A ;

BERRY, G .

PROCEEDINGS OF THE IEEE, 1991, 79 (09) :1270-1282

[4] THE ESTEREL SYNCHRONOUS PROGRAMMING LANGUAGE - DESIGN, SEMANTICS, IMPLEMENTATION [J].

BERRY, G ;

GONTHIER, G .

SCIENCE OF COMPUTER PROGRAMMING, 1992, 19 (02) :87-152

[5]

BERTIN V, 1999, P GRAISYHM AAA LILL

[6]

HENZINGER TA, 1997, SOFTWARE TOOLS TECHN, V1, P110

[7]

Larsen K.G., 1997, J SOFTWARE TOOLS TEC, V1, P134

[8] SCHEDULING ALGORITHMS FOR MULTIPROGRAMMING IN A HARD-REAL-TIME ENVIRONMENT [J].

LIU, CL ;

LAYLAND, JW .

JOURNAL OF THE ACM, 1973, 20 (01) :46-61

[9]

Mouly M., 1992, GSM SYSTEM MOBILE CO

[10]

YOVINE S, 1998, LECT NOTES COMPUTER

← 1 →