Contract-Based Verification of Simulink Models

被引：0

作者：

Bostrom, Pontus ^{[1
]}

机构：

[1] Abo Akad Univ, Dept Informat Technol, FIN-20520 Turku, Finland

来源：

FORMAL METHODS AND SOFTWARE ENGINEERING | 2011年 / 6991卷

关键词：

REFINEMENT CALCULUS;

D O I：

暂无

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

This paper presents an approach to compositional contract-based verification of Simulink models. The verification approach uses Synchronous Data Flow (SDF) graphs as a formalism to obtain sequential program statements that can then be analysed using traditional refinement-based verification techniques. Automatic generation of the proof obligations needed for verification of correctness with respect to contracts, as well as automatic proofs are also discussed.

引用

页码：291 / 306

页数：16

共 19 条

[1]

[Anonymous], 1997, Object-oriented software construction

[2]

Back R.-J., 2000, Formal Aspects of Computing, V12, P313, DOI 10.1007/s001650070008

[3]

Back R.-J., 1998, Refinement Calculus: A Systematic Introduction

[4]

BACK RJR, 1990, LECT NOTES COMPUT SC, V430, P42

[5]

Back RJR, 1994, LECT NOTES COMPUT SC, V836, P367

[6]

Barnett M., 2011, COMMUNICATIONS ACM, V54

[7]

Barnett M, 2006, LECT NOTES COMPUT SC, V4111, P364

[8]

Bostrom P., 2008, THESIS ABO AKAD U

[9]

Bostrom P., 2007, 10 SCAND INT C FLUID, V1, P227

[10]

Bostrom P., 2010, 985 TUCS

← 1 2 →