원문정보
초록
영어
Runtime verification aims to check whether an application executes its behaviour as specified. Thereby the active execution trace of an application is checked in terms of the actual execution context; diagnosis and, possibly, recovery actions are taken when the specification is violated. In today’s practices, software is increasingly distributed over multiple processes, potentially running at different locations. This is supported by middleware that, to some extent, allows implementing applications in a distribution-transparent way. To enable effective runtime verification in distributed software we focus in this paper on three requirements: (1) distribution-transparent specification of software behaviour, as software is also implemented in such a way, (2) end-to-end verification of behaviour, and (3) automatic generation of verification modules for arbitrary process and distribution structures. We present a novel runtime verification approach satisfying these requirements and present its implementation in the EventChaser system. Furthermore we present an approach that at least minimizes the distribution-awareness of specifications to an acceptable level for software not using supported middleware for inter-process communication.
목차
I. INTRODUCTION
II. BACKGROUND: RUNTIME VERIFICATION
III. PROBLEM STATEMENT
A. An Illustrative Example: Document-Editing Application
B. Requirements for the Runtime Verification of Distributed Messages
C. Shortcomings of the Existing Runtime Verification Systems
IV. THE EVENTCHASER VERIFICATION SYSTEM
A. Code Analyser
B. Causal Thread Manager
C. Code Generator
V. A SAMPLE SPECIFICATION
VI. THE ASPECT-ORIENTED REALIZATION OF EVENTCHASER
VII. DESCRIPTION OF EVENTCHASER'S SEMANTICS FOR DISTRIBUTED CASE
VIII. EVALUATION
IX. DISTRIBUTION-SENSITIVITY IN EVENTCHASER
X. CONCLUSION AND FUTURE WORK
References