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
12