Monitoring and checking of real-time and probabilistic properties.

摘要

As real-time systems, such as cars, become an essential part of our lives, we must ensure that these real-time systems are safe and correct. The goal of this dissertation is to study a technique based on formal methods to guarantee safety and correctness for such real-time systems. In real-time systems, correct computation needs to be delivered in a timely manner. Correctness of real-time systems, therefore, depends on their computation as well as timeliness and dependability. One verification technique, called runtime verification, ensures program correctness by observing program executions at runtime and checking whether the executions satisfy given specifications. Existing runtime verification frameworks, however, do not provide intuitive specification languages for expressing real-time and probabilistic properties or adequate implementation for checking such properties. This dissertation aims to provide a complete runtime verification framework for real-time systems by extending a promising runtime verification framework, MaC (Monitoring and Checking). MaC verifies computational correctness by checking functional properties based on Linear Temporal Logic but provides neither adequate language nor efficient implementation for verifying timing and probabilistic properties, which are essential to real-time systems. This dissertation extends MaC with capabilities to verify timing and probabilistic properties by introducing time-bound temporal operators and probabilistic operators. Regular expressions are also included as a complement to the logic-based specification language. Time-bound temporal operators allow ones to specify a time bound in which a property must hold and thus are more appropriate for timing properties. Probabilistic operators allow ones to specify degrees of certainty in which probabilistic properties should hold. Probabilistic properties are checked using statistical analysis to mathematically support the results. As a case study, the extension is applied to check wireless sensor network applications. Wireless sensor network applications are real-time systems that can tolerate some degree of deadline misses and requires functional, timing, and probabilistic properties, which cannot be expressed by the existing MaC. The case study shows how the extended MaC can be used to verify such wireless sensor network applications. The results of this case study demonstrate usability of the extended MaC and provide basis for testing and debugging of wireless sensor network applications.