Specifying real-time properties in autonomic systems |
| |
Authors: | Ji Zhang Zhinan Zhou Betty H. C. Cheng Philip K. McKinley |
| |
Affiliation: | (1) Software Engineering and Network Systems Laboratory, Department of Computer Science and Engineering, Michigan State University, 3115 Engineering Building, East Lansing, MI 48824, USA;(2) Present address: San Jose Mobile Communications Lab, Samsung Telecommunications America, 85 W. Tasman Dr., San Jose, CA 95134, USA |
| |
Abstract: | Increasingly, computer software must adapt dynamically to changing conditions. The correctness of adaptation cannot be rigorously addressed without precisely specifying the requirements for adaptation. In many situations, these requirements involve absolute time, in addition to a logical ordering of events. This paper introduces an approach to formally specifying such timing requirements for adaptive software. We introduce TA-LTL, a timed adaptation-based extension to linear temporal logic, and use this logic to specify three timing properties associated with the adaptation process: safety, liveness, and stability. A dynamic adaptation scenario involving interactive audio streaming software is used to illustrate the timed temporal logic. A number of related papers and technical reports of the Software Engineering and Network Systems Laboratory can be found at the following URL: http://www.cse.msu.edu/sens. |
| |
Keywords: | Autonomic systems Adaptation Timing properties Temporal logic Model checking |
本文献已被 SpringerLink 等数据库收录! |
|