Redundancy management is widely utilized in mission critical digital flight control systems. This study focuses on the use of SCADE and its formal verification component, the Design Verifier, to assess the design correctness of a sensor voter algorithm used for management of three redundant sensors. The sensor voter algorithm is representative of embedded software used in many aircraft today. The algorithm is captured as a Simulink diagram; it takes input from three sensors and computes an output signal and a hardware flag indicating correctness of the output. This study is part of an overall effort to compare several model checking tools to the same problem. SCADE is used to analyze the voter's correctness in this part of the study. Since synthesis of a correct environment for analysis of the voter's normal and off-normal behavior is a key factor when applying formal verification tools, this paper is focused on 1) the different approaches used for modeling the voter's environment and 2) the strengths and shortcomings of such approaches when applied to the problem under investigation.