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 条
  • [31] A dynamic logic for the formal verification of java card programs
    Universität Karlsruhe, Institut für Logik, Komplexität und Deduktionssysteme, Karlsruhe
    D-76128, Germany
    Lect. Notes Comput. Sci., 1600, (6-24):
  • [32] Formal verification of protocol properties of sequential java programs
    College of Computer Science and Technology, Jilin University, 2699 Qianjin Street, Changchun, 130012, China
    Proc Int Comput Software Appl Conf, (475-482):
  • [33] Formal verification of concurrent programs using the Larch prover
    Chetali, B
    IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1998, 24 (01) : 46 - 62
  • [34] Formal Verification of Spacecraft Control Programs (Experience Report)
    Mokhov, Andrey
    Lukyanov, Georgy
    Lechner, Jakob
    PROCEEDINGS OF THE 12TH ACM SIGPLAN INTERNATIONAL SYMPOSIUM ON HASKELL (HASKELL '19), 2019, : 139 - 145
  • [35] Towards Formal Verification of State Continuity for Enclave Programs
    Jangid, Mohit Kumar
    Chen, Guoxing
    Zhang, Yinqian
    Lin, Zhiqiang
    PROCEEDINGS OF THE 30TH USENIX SECURITY SYMPOSIUM, 2021, : 573 - 590
  • [36] Formal Verification of the Race Condition Vulnerability in Ladder Programs
    Mesli-Kesraoui, Soraya
    Goubali, Olga
    Kesraoui, Djamal
    Eloumami, Ibtihal
    Oquendo, Flavio
    2020 IEEE CONFERENCE ON CONTROL TECHNOLOGY AND APPLICATIONS (CCTA), 2020, : 892 - 897
  • [37] Methods and Tools for Formal Verification of Cloud Sisal Programs
    Kasyanov, Victor N.
    Kasyanova, Elena, V
    2ND INTERNATIONAL CONFERENCE ON MATHEMATICS AND COMPUTERS IN SCIENCE AND ENGINEERING (MACISE 2020), 2020, : 219 - 222
  • [38] Formal Verification of Ladder Logic programs using NuSMV
    Kottler, Sam
    Khayamy, Mehdy
    Hasan, Syed Rafay
    Elkeelany, Omar
    SOUTHEASTCON 2017, 2017,
  • [39] Formal Verification of Higher-Order Probabilistic Programs
    Sato, Tetsuya
    Aguirre, Alejandro
    Barthe, Gilles
    Gaboardi, Marco
    Garg, Deepak
    Hsu, Justin
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2019, 3 (POPL):
  • [40] Three Early Formal Approaches to the Verification of Concurrent Programs
    Cliff B. Jones
    Minds and Machines, 2024, 34 : 73 - 92
12345