Temporal logic framework for performance analysis of architectures of systems

Abstract

This paper presents a formal mathematical framework for performance analysis (in terms of success of given tasks) of complex systems, ATLAS. This method interestingly combines temporal aspects (for the description of the complex system) and probabilities (to represent performance). The system’s task to be evaluated is described using a temporal language, the ATLAS language: the architecture of the task is decomposed into elementary functionalities and temporal operators specify their arrangement. Starting with the success probabilities of the elementary functionalities, it is then possible to compute the overall success probability of the task using mathematical formulae which are proven in this paper. The method is illustrated with a deorbitation task for a retired satellite called ENVISAT.