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 条
  • [1] Integrating formal verification and conformance testing for reactive systems
    Constant, Camille
    Jeron, Thierry
    Marchand, Herve
    Rusu, Vlad
    IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2007, 33 (08) : 558 - 574
  • [2] Automated formal verification and testing of c programs for embedded systems
    Kandl, Susanne
    Kirner, Raimund
    Puschner, Peter
    10TH IEEE INTERNATIONAL SYMPOSIUM ON OBJECT AND COMPONENT-ORIENTED REAL-TIME DISTRIBUTED COMPUTING, PROCEEDINGS, 2007, : 373 - +
  • [3] Combining formal verification and conformance testing for validating reactive systems
    Rusu, V
    SOFTWARE TESTING VERIFICATION & RELIABILITY, 2003, 13 (03): : 157 - 180
  • [4] Formal verification of PLC programs
    Rausch, M
    Krogh, BH
    PROCEEDINGS OF THE 1998 AMERICAN CONTROL CONFERENCE, VOLS 1-6, 1998, : 234 - 238
  • [5] FORMAL VERIFICATION OF PARALLEL PROGRAMS
    KELLER, RM
    COMMUNICATIONS OF THE ACM, 1976, 19 (07) : 371 - 384
  • [6] FORMAL VERIFICATION OF ADA PROGRAMS
    GUASPARI, D
    MARCEAU, C
    POLAK, W
    IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1990, 16 (09) : 1058 - 1075
  • [7] CIVL: Formal Verification of Parallel Programs
    Zheng, Manchun
    Rogers, Michael S.
    Luo, Ziqing
    Dwyer, Matthew B.
    Siegel, Stephen F.
    2015 30TH IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE), 2015, : 830 - 835
  • [8] Formal Verification of Practical MPI Programs
    Vo, Anh
    Vakkalanka, Sarvani
    DeLisi, Michael
    Gopalakrishnan, Ganesh
    Kirby, Robert M.
    Thakur, Rajeev
    ACM SIGPLAN NOTICES, 2009, 44 (04) : 261 - 269
  • [9] Formal Verification of Spacecraft Control Programs
    Lukyanov, Georgy
    Mokhov, Andrey
    Lechner, Jakob
    ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS, 2020, 19 (05)
  • [10] A Logic for Formal Verification of Quantum Programs
    Kakutani, Yoshihiko
    ADVANCES IN COMPUTER SCIENCE - ASIAN 2009: INFORMATION SECURITY AND PRIVACY, PROCEEDINGS, 2009, 5913 : 79 - 93
12345