Concurrent runtime monitoring of formally specified programs

1 March 1993

journal article
Published by Institute of Electrical and Electronics Engineers (IEEE) in Computer

Vol. 26 (3) , 32-41
https://doi.org/10.1109/2.204684

Abstract

A methodology for continuously monitoring a program for specification consistency during program execution is described. Prior development of the formal specification and program is assumed. The program is annotated with constructs from a formal specification language, and the formal specification constructs are transformed into checking code, which is then inserted into the underlying program. Calls to this checking code are inserted into underlying program wherever it can potentially become inconsistent with its specification. If an inconsistency does in fact occur, diagnostic information is provided. The implementation of such a system for Anna (annotated Ada) subtype annotations is presented.

Keywords

This publication has 4 references indexed in Scilit:

A note on the detection of an Ada compiler bug while debugging an Anna program
ACM SIGPLAN Notices, 1989
Formal program construction by transformations-computer-aided, intuition-guided programming
IEEE Transactions on Software Engineering, 1989
Concurrent runtime checking of annotated Ada programs
Published by Springer Nature ,1986
Watchdog Processors and Structural Integrity Checking
IEEE Transactions on Computers, 1982