Formal Model and Code Verification in Model-Based Design

被引：0

作者：

Popovici, Katalin ^{[1
]}

Lalo, Marc ^{[1
]}

机构：

[1] MathWorks, F-38330 Montbonnot St Martin, France

来源：

2009 JOINT IEEE NORTH-EAST WORKSHOP ON CIRCUITS AND SYSTEMS AND TAISA CONFERENCE | 2009年

关键词：

D O I：

暂无

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

The increasing complexity of embedded software makes its verification a key challenge in designing embedded systems. This paper gives an overview of Model-Based Design used for large and complex embedded systems, with emphasis on: the early verification of the design. Two tools for verification through formal analysis are described: Simulink (R) Design Verifier (TM) to check the properties of a model, and PolySpace (R) to prove the absence of certain run-time errors in the embedded software.

引用

页码：392 / 395

页数：4

共 15 条

[1] Static analysis by abstract interpretation: application to the detection of heap overflows [J].

Allamigeon, Xavier ;

Hymans, Charles .

JOURNAL OF COMPUTER VIROLOGY AND HACKING TECHNIQUES, 2008, 4 (01) :5-23

[2]

[Anonymous], SIM DES VER

[3]

BEHBOODIAN A, 2005, DSP MAGAZINE

[4]

Cousot P, 2004, INT FED INFO PROC, V156, P359

[5]

Cousot P., 1977, C RECORD 1977 ACM S, P238

[6]

DABNEY J, 2004, RETURN INVESTMENT IN

[7]

DAVEY C, 2007, INT C SOFTW ENG MINN

[8]

El-Far I.K., 2001, ENCY SOFTWARE ENG

[9]

HODGE G, 2004010269 SAE

[10]

International Technology Roadmap for Semiconductors, 2005, INT TECHN ROADM SEM

← 1 2 →