A responsive computing system is a hybrid of real-time, distributed and fault-tolerant systems. In such a system, severe consequences can occur if the run-time behavior does not conform to the expected behavior or specifications. In this paper, we present a formal approach to ensure satisfaction of the specifications in the operational environment as follows. First we specify behavior of the systems using Interval Temporal Logic (ITL). Next we give algorithms for trace checking of programs in such systems. Finally, we present a fully distributed run-time evaluation system which causally orders the events of the system during its execution and checks this run-time behavior against its ITL specification. The approach is illustrated using a train-set example.
G. Tsai et al., "Ensuring the Satisfaction of a Temporal Specification at Run-Time," Proceedings of the First IEEE International Conference on Engineering of Complex Computer Systems, 1995. Held jointly with 5th CSESAW, 3rd IEEE RTAW and 20th IFAC/IFIP WRTP, Institute of Electrical and Electronics Engineers (IEEE), Jan 1995.
The definitive version is available at http://dx.doi.org/10.1109/ICECCS.1995.479365
First IEEE International Conference on Engineering of Complex Computer Systems, 1995. Held jointly with 5th CSESAW, 3rd IEEE RTAW and 20th IFAC/IFIP WRTP
Mathematics and Statistics
Keywords and Phrases
Distributed Processing; Distributed System; Fault-Tolerant Systems; Formal Specification; Fully Distributed Run-Time Evaluation System; Interval Temporal Logic; Operational Environment; Real-Time System; Real-Time Systems; Responsive Computing System; Run-Time Behavior; Run-Time Temporal Specification Satisfaction; Software Fault Tolerance; Temporal Logic; Trace Checking; Train-Set Example
Article - Conference proceedings
© 1995 Institute of Electrical and Electronics Engineers (IEEE), All rights reserved.