Concurrent runtime monitoring of formally specified programs

Author

Sankar, Sriram ; Mandal, Manas

Author_Institution

Stanford Univ., CA, USA

Volume

26

Issue

3

fYear

1993

fDate

3/1/1993 12:00:00 AM

Firstpage

32

Lastpage

41

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

formal specification; parallel programming; specification languages; system monitoring; Anna; annotated Ada; checking code; diagnostic information; formal specification constructs; formal specification language; program execution; specification consistency; subtype annotations; underlying program; Computer languages; Condition monitoring; Formal specifications; Hardware; Information security; Operating systems; Program processors; Programming; Runtime; Safety;

fLanguage

English

Journal_Title

Computer

Publisher

ieee

ISSN

0018-9162

Type

jour

DOI

10.1109/2.204684

Filename

204684