SYSTEMATIC TESTING AND FORMAL VERIFICATION TO VALIDATE REACTIVE PROGRAMS

被引：7
|
作者：
MULLERBURG, M [1 ]
HOLENDERSKI, L [1 ]
MAFFEIS, O [1 ]
MERCERON, A [1 ]
MORLEY, M [1 ]
机构：
[1] SCHLOSS BIRLINGHOVEN,D-53757 ST AUGUSTIN,GERMANY
来源：
SOFTWARE QUALITY JOURNAL | 1995年 / 4卷 / 04期
关键词：
VALIDATION; SYSTEMATIC TESTING; FORMAL VERIFICATION; REACTIVE SYSTEMS; SYNCHRONOUS PROGRAMMING;
D O I：
10.1007/BF00402649
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
The use of systematic testing and formal verification in the validation of reactive systems implemented in synchronous languages is illustrated. Systematic testing and formal verification are two techniques for checking the consistency between a program and its specification. The approach to validation is through specification: two system views are developed in addition to the program, a behavioural specification for systematic testing and a logical specification for formal verification. Pursuing both activities, reactive programs can be validated both more efficiently (in terms of costs) and more effectively (in terms of confidence in correctness). This principle is demonstrated here using the well known lift example.
引用
收藏
页码：287 / 307
页数：21
相关论文
共 50 条
  • [41] Using Krakatoa for Teaching Formal Verification of Java Programs
    Divasón, Jose
    Romero, Ana
    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2019, 11758 LNCS : 37 - 51
  • [42] Randomized differential testing as a prelude to formal verification
    Groce, Alex
    Holzmann, Gerard
    Joshi, Rajeev
    ICSE 2007: 29TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, PROCEEDINGS, 2007, : 621 - +
  • [43] Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra
    Foster, Simon
    Ye, Kangfeng
    Cavalcanti, Ana
    Woodcock, Jim
    RELATIONAL AND ALGEBRAIC METHODS IN COMPUTER SCIENCE, 2018, 11194 : 205 - 224
  • [44] Formal Verification and Testing Based on P Systems
    Gheorghe, Marian
    Ipate, Florentin
    Dragomir, Ciprian
    MEMBRANE COMPUTING, 2010, 5957 : 54 - +
  • [45] TESTING AND FORMAL VERIFICATION OF SERVICE ORIENTED ARCHITECTURES
    Sloan, John C.
    Khoshgoftaar, Taghi M.
    INTERNATIONAL JOURNAL OF RELIABILITY QUALITY AND SAFETY ENGINEERING, 2009, 16 (02) : 137 - 162
  • [46] Testing and Formal Verification of Logarithmic Function Design
    Agarwal, Sanjeev
    Bhuria, Indu
    INTERNATIONAL CONFERENCE ON METHODS AND MODELS IN SCIENCE AND TECHNOLOGY (ICM2ST-10), 2010, 1324 : 57 - +
  • [47] Verification criterion directed testing for formal specifications
    Zeng, XM
    Tsai, JJP
    Weigert, TJ
    SEKE '96: THE 8TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND KNOWLEDGE ENGINEERING, PROCEEDINGS, 1996, : 393 - 399
  • [48] Automated verification of reactive and concurrent programs by calculation
    Foster, Simon
    Ye, Kangfeng
    Cavalcanti, Ana
    Woodcock, Jim
    JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 2021, 121
  • [49] On Modularity in Reactive Control Architectures, with an Application to Formal Verification
    Biggar, Oliver
    Zamani, Mohammad
    Shames, Iman
    ACM TRANSACTIONS ON CYBER-PHYSICAL SYSTEMS, 2022, 6 (02)
  • [50] Formal Verification of Numerical Programs: From C Annotated Programs to Mechanical Proofs
    Boldo, Sylvie
    Marche, Claude
    MATHEMATICS IN COMPUTER SCIENCE, 2011, 5 (04) : 377 - 393
12345