Formal reliability analysis of redundant architectures