Search

A run-time monitor shares computational resources, such as memory and CPU time, with the target program. Furthermore, heavy computation performed by a monitor for checking target program's execution with respect to requirement properties can be a bottleneck to the target program's execution. Therefore, computational characteristics of run-time monitoring cause a significant impact on the target program's execution.We investigate computational issues on run-time monitoring. The first issue is the power of run-time monitoring. In other words, we study the class of properties run-time monitoring can evaluate. The second issue is computational complexity of evaluating properties written in process algebraic language. Third, we discuss sound abstraction of the target program's execution, which does not change the result of property evaluation. This abstraction can be used as a technique to reduce monitoring overhead. Theoretical understanding obtained from these issues affects the implementation of Java-MaC, a toolset for the run-time monitoring and checking of Java programs. Finally, we demonstrate the abstraction-based overhead reduction technique implemented in Java-MaC through a case study.

ForewordThis volume contains the proceedings of the Third International Workshop on Run-time Verification (RV '03). RV '03 was held on July 13, 2003, as a satellite workshop of the International Conference of Computer-Aided Verification (CAV '03). The first two workshops in this series were also held as satellite workshops of CAV; RV '01 was held in Paris in July 2001, and RV '02 was held in Copenhagen in July 2002.The purpose of this series of workshops has been to bring together researchers and practitioners, interested in various aspects related to the dynamic analysis of software and systems, with respect to formally specified correctness requirements. Run-time verification aims to provide a “lightweight” complement to traditional verification methods like model checking and theorem proving, by analysing an actual implementation with respect to the reduced correctness obligations of certifying the correctness of a single execution. Despite the weaker guarantees, run-time verification improves upon other more ad-hoc approaches in monitoring, by providing formal proofs.The papers selected for this year's workshop cover a wide range of topics related to runtime verification, including designing efficient and optimal verification algorithms, techniques for instrumenting programs at the source or object code/byte code level to observe program execution, developing specification languages for monitors, dynamic program analysis, and formally proving the correctness of monitoring systems. This volume includes these papers and the abstract of the Invited Presentation by the Invited Presentation by Aloysius K. Mok (University of Texas at Austin). The volume will be published in the Electronic Notes in Theoretical Computer Science (ENTCS). This series is published electronically through the facilities of Elsevier Science B.V. and its auspices. The volumes in the ENTCS series can be accessed at the URL http://www.elsevier.nl/locate/entcs.We would like to thank the Program Committee members and their reviewers, who did an excellent job evaluating the submissions and shaping the program of the workshop. We are grateful to the Steering Committee for helpful guidance and support. Special thanks go to Al Mok for agreeing to be the Invited Speaker. Thanks to the CAV '03 co-Chairs: Warren A. Hunt, Jr. (University of Texas at Austin) and Fabio Somenzi (University of Colorado at Boulder) for the opportunity to continue the tradition of having the RV workshops as CAV satellites. July 1, 2003Oleg SokolskyMahesh ViswanathanProgram Committee Saddek BensalemVERIMAG LaboratoryRance CleavelandState University of New York at Stony BrookAnn GatesUniversity of Texas, El PasoPatrice GodefroidBell LaboratoriesGerard HolzmannNASA/JPL Laboratory for Reliable SoftwareSusan HorwitzUniversity of Wisconsin, MadisonMichael MoellerUniversity of OldenburgAloysius K. MokUniversity of Texas, AustinHenny SipmaStanford UniversityOleg SokolskyUniversity of PennsylvaniaScott StollerState University of New York at Stony BrookMahesh ViswanathanUniversity of Illinois at Urbana-ChampaignSergio YovineVERIMAG LaboratoryLenore ZuckNew York UniversitySteering Committee Klaus HavelundNASA Ames Research Center - Kestrel TechnologyInsup LeeUniversity of PennsylvaniaGrigore RosuUniversity of Illinois at Urbana-Champaign