Checkers, Self-Testers, and Self-Correctors for Reactive Systems.

摘要

This report discusses the development of formal methods for monitoring safety-critical real-time and reactive systems. This project centers on building on expertise in the area of process-algebra-based specification and analysis of real-time systems as well as the paradigm of program checking which allows one to make rigorous statements about the correctness of program behavior rather than of the program itself. To integrate these ideas a prototype system (JavaMAC) for monitoring and checking Java programs has been implemented. MAC takes a monitoring script provided by the user, the program, and a requirement specification and produces (a) an instrumentation of the program to send variable update information to the monitoring and checking unit (b) a script for transforming low level program variable values to abstract events and (c) a script for checking whether a sequence of events is consistent with the desired property. These scripts written in new languages are defined (PEDL and MEDL respectively) and are then used to produce other components that extract low- level information from the program, convert it to events and check that the sequence of events represents correct behavior. The prototype has been successfully tested on two applications --- micro air vehicles attaining a desired formation, and convergence of a network routing protocol. Performance measurements have been done on JavaMAC in an attempt to breakdown the overhead introduced by JavaMAC into its various components. Subsequently several optimizations in JavaMAC have been introduced to improve the performance. Other research funded by this grant includes papers on probabilistic bisimulation and on low-overhead checking of the correctness of the output produced by programs for sorting and other mathematically well-defined tasks.