Runtime Assertion Checking of Temporal Specifications in a Mobile Environment - AHS


A mobile concurrent system can be checked for correctness at run-time by placing assertions in the code in a method called assertion checking. We propose using this method on a model problem, the Automated Highway System (AHS), to ensure that temporal specifications of the system are fulfilled at run-time. The process of assertion checking used involves collection of event histories and using assertions to scan through these histories to evaluate them for correctness. Implementation results using Java Aglets (Mobile Agents) on a network of workstations are used to measure the effectiveness of the error detection through fault coverage and error detection latency for various induced failures.

Meeting Name

20th Symposium on Reliable Distributed Systems (2001: Oct. 28-31, New Orleands, LA)


Computer Science

Keywords and Phrases

Error Checking; Mobile Computing; Monitoring; Software Correctness; Temporal Logic

Document Type

Article - Conference proceedings

Document Version


File Type




Publication Date

31 Oct 2001

This document is currently not available here.