Performability analysis of an avionics-interface

This paper reports on a case study in the quantitative analysis of safety-critical systems. Although formal methods are becoming more and more accepted in the development of such systems, usually they are used in the verification of qualitative properties. However, in many cases system safety also depends on the fact that certain quantitative requirements are met. Therefore we are interested in statements about quantitative properties, which can be achieved by a rigorous formal method. Our approach is to create a generalized stochastic Petri net (GSPN) model of the system and use it for the analysis of the system. The object of this case study is a fault-tolerant computer (FTC) constructed by Daimler Benz Aerospace (DASA) for the International Space Station (ISS). One part of the FTC is the Avionics Interface (AVI) which connects the FTC with a bus-system. We want to determine the data throughput that can be reached by the AVI and obtain informations about bus-usage-profiles which can cause the rejection of messages. Although such rejections are allowed according to the specification, they can cause a significant deterioration in the overall bus performance. In this article we describe a GSPN model of the AVI software and its environment. This model is used to make predictions about the AVI performability. Since a complete analytical solution of the model is not possible due to its complexity and the infinite state space, a simulation is used to analyse the crucial AVI behavior for several bus-usage-profiles.