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 条
  • [21] Formal Verification of Masking Countermeasures for Arithmetic Programs
    Gao, Pengfei
    2020 35TH IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE 2020), 2020, : 1385 - 1387
  • [22] FORMAL VERIFICATION OF A CLASS OF CONCURRENT PROGRAMS.
    Mori, Masaaki
    Taniguchi, Kenichi
    Kasami, Tadao
    Fujii, Mamoru
    Systems, computers, controls, 1981, 10 (04): : 11 - 20
  • [23] A formal framework for synthesis and verification of logic programs
    Avellone, A
    Ferrari, M
    Fiorentini, C
    LOGIC BASED PROGRAM SYNTHESIS AND TRANSFORMATION, 2001, 2042 : 1 - 17
  • [24] EXTRACTION AND VERIFICATION OF PROGRAMS BY ANALYSIS OF FORMAL PROOFS
    ALEXI, W
    THEORETICAL COMPUTER SCIENCE, 1988, 61 (2-3) : 225 - 258
  • [25] Games for formal design and verification of reactive systems
    Alur, Rajeev
    Fourth ACM & IEEE International Conference on Formal Methods and Models for Co-Design, Proceedings, 2006, : 3 - 3
  • [26] A Formal Approach to Testing Programs in Practice
    Liu, Shaoying
    Shen, Wuwei
    Nakajima, Shin
    COMPUTER SCIENCE AND INFORMATION SYSTEMS, 2012, 9 (04) : 1469 - 1491
  • [27] Three Early Formal Approaches to the Verification of Concurrent Programs
    Jones, Cliff B.
    MINDS AND MACHINES, 2024, 34 (SUPPL 1) : 73 - 92
  • [28] Formal verification of secure programs in the presence of side effects
    Black, PE
    Windley, PJ
    PROCEEDINGS OF THE THIRTY-FIRST HAWAII INTERNATIONAL CONFERENCE ON SYSTEM SCIENCES, VOL III: EMERGING TECHNOLOGIES TRACK, 1998, : 327 - 334
  • [29] Formal Verification of Quantum Programs: Theory, Tools, and Challenges
    Lewis, Marco
    Soudjani, Sadegh
    Zuliani, Paolo
    ACM TRANSACTIONS ON QUANTUM COMPUTING, 2024, 5 (01):
  • [30] Formal Specification-Based Inspection for Verification of Programs
    Liu, Shaoying
    Chen, Yuting
    Nagoya, Fumiko
    McDermid, John A.
    IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2012, 38 (05) : 1100 - 1122
12345