analysis and comparison of different formal methods on the static behavior for fault-tolerant systems

Paper number

IAC-15,D1,IP,13,x30180

Author

Mr. Zheng WANG, Zhejiang University, China

Coauthor

Mr. Daniel Lüdtke, German Aerospace Center (DLR), Germany

Coauthor

Dr. Andreas Gerndt, German Aerospace Center (DLR), Simulation and Software Technology, Germany

Coauthor

Prof.Dr. HAI HUANG, Zhejiang University, China

Coauthor

Prof. Xiangxian Chen, Zhejiang University, China

Year

2015

Abstract

\begin{Abstract}
the computational demands for space systems are dramatically increasing. There are lots of projects, such as DLR’s project OBC-NG (On-board Computer Next Generation, that use COTS (Commercial Off-The-Shelf) components to improve the performance instead of space qualified components. But reliability and safety of the system will decrease, which affects fault-tolerant systems a lot. Actually OBC-NG can utilize all available computing resources to reconfigure itself between software and hardware for different missions and error mitigation. Reconfiguration achieves task migration, task morphing and supports redundancy. In this paper, we take a small prototype of OBC-NG as an example, which includes all significant features of OBC-NG.  We adopt different formal methods, for instance, SCPN (Stochastic Colored Petri Nets), ReCoNet , and a Mathematical analytical model, to analyze the static behavior of the prototype. The paper contains several formal models, architecture graph which models the available resources, i.e., nodes in the network, task distribution which models tasks running on different nodes, communication mapping which models the data dependencies between tasks, and attributes model which describes the role and workload of nodes. Through these models, we can analyze the probability of failures, reliability and safety of the system, and then determine when the system needs reconfiguration. In addition, we analyze the results of the static behavior, and give an outlook on modelling on reconfiguration at run-time, and optimization for it. Finally, the paper compares the advantages and disadvantages of different formal methods, and recommends employing SCPN as the future method to model OBC-NG and analyze dynamic attributes for fault-tolerant systems.
\end{Abstract}

Abstract document

IAC-15,D1,IP,13,x30180.brief.pdf

Manuscript document

(absent)