Abstract

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.

Meeting Name

First IEEE International Conference on Engineering of Complex Computer Systems, 1995. Held jointly with 5th CSESAW, 3rd IEEE RTAW and 20th IFAC/IFIP WRTP

Department(s)

Mathematics and Statistics

Second Department

Computer Science

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

Document Type

Article - Conference proceedings

Document Version

Final Version

File Type

text

Language(s)

English

Rights

© 1995 Institute of Electrical and Electronics Engineers (IEEE), All rights reserved.

Publication Date

01 Jan 1995

Download

Full Text Link

Share

 
COinS