Accession Number : ADA314228

Title :   Concurrent Runtime Monitoring of Formally Specified Programs.

Descriptive Note : Technical rept.,

Corporate Author : STANFORD UNIV CA COMPUTER SYSTEMS LAB

Personal Author(s) : Mandal, Manas ; Sankar, Sriram

PDF Url : ADA314228

Report Date : APR 1990

Pagination or Media Count : 33

Abstract : This paper describes an application of formal specifications after an executable program has been constructed. We describe how high level specifications can be utilized to monitor critical aspects of the behavior of a program continuously while it is executing. This methodology provides a capability to distribute the monitoring of specifications on multiprocessor hardware platforms to meet practical time constraints. Typically, runtime checking of formal specifications involves a significant time penalty which makes it impractical during normal production operation of a program. In previous research, runtime checking has been applied during testing and debugging of software, but not on a permanent basis. Crucial to our current methodology is the use of multiprocessor machines hence runtime monitoring can be performed concurrently on different processors. We describe techniques for distributing checks onto different processors. To control the degree of concurrency, we introduce checkpoints a point in the program beyond which execution cannot proceed until the specified checks have been completed. Error reporting and recovery in a multi-processor environment is complicated and there are various techniques of handling this. We describe a few of these techniques in this paper. An implementation of this methodology for the Anna specification language for Ada programs is described. Results of experiments conducted on this implementation using a 12 processor Sequent Symmetry demonstrate that permanent concurrent monitoring of programs based on formal specifications is indeed feasible.

Descriptors :   *MONITORING, *SPECIFICATIONS, *COMPUTER PROGRAM VERIFICATION, TEST AND EVALUATION, METHODOLOGY, CONSISTENCY, TIME, SELF OPERATION, MULTIPROCESSORS, ADA PROGRAMMING LANGUAGE, DEBUGGING(COMPUTERS), CHECKOUT PROCEDURES, INDEX TERMS.

Subject Categories : Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE