Generating test cases for real-time systems from logic specifications

1 November 1995

journal article
Published by Association for Computing Machinery (ACM) in ACM Transactions on Computer Systems

Vol. 13 (4) , 365-398
https://doi.org/10.1145/210223.210226

Abstract

We address the problem of automated derivation of functional test cases for real-time systems, by introducing techniques for generating test cases from formal specifications written in TRIO, a language that extends classical temporal logic to deal explicitly with time measures. We describe an interactive tool that has been built to implement these techniques, based on interpretation algorithms of the TRIO language. Several heuristic criteria are suggested to reduce drastically the size of the test cases that are generated. Experience in the use of the tool on real-life cases is reported.

Keywords

This publication has 16 references indexed in Scilit:

Validating real-time systems by history-checking TRIO specifications
ACM Transactions on Software Engineering and Methodology, 1994
Proving properties of real-time systems through logical specifications and Petri net models
IEEE Transactions on Software Engineering, 1994
An investigation of the Therac-25 accidents
Computer, 1993
Test selection based on finite state models
IEEE Transactions on Software Engineering, 1991
TRIO: A logic language for executable specifications of real-time systems
Journal of Systems and Software, 1990
Mockingbird: A logical methodology for testing
The Journal of Logic Programming, 1990
Test generation for sequential circuits
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1988
Test sets generation from algebraic specifications using logic programming
Journal of Systems and Software, 1986
Timing Constraints of Real-Time Systems: Constructs for Expressing Them, Methods of Validating Them
IEEE Transactions on Software Engineering, 1985
Testing Formal Specifications to Detect Design Errors
IEEE Transactions on Software Engineering, 1985