: Avionics systems play a critical role in the operation of aircrafts. The demand for more safety and higher performance has increased the complexity of these systems. The design of these software-intensive networked systems should be dependable and verifiable according to the airworthiness regulations. Thus, detailed analysis and verification of complex and safety critical avionics systems is required, especially at the initial stages of the design. Formal methods provide a good framework for the specification and verification of complex systems from the initial high level design to the final detailed design phase. Here a system was designed for the flight control of a light commercial aircraft. The aim was to satisfy the many functional, operational and safety requirements that are necessary for the aircraft flight control based on the aviation standards. The designed flight control system (FCS) was formally specified and verified using the Architecture Analysis Design Language (AADL, SAE 5506 Standard). All formal analysis, supported by the AADL toolbox, was carried out on the formal model of the FCS. Fault tree analysis, fault hazard analysis, system safety assessment, flow latency, connection binding consistency, resource allocation analysis and fault impact analysis are among the performed analysis. The initial design and specification was further improved based on the results of formal verifications. The AADL was also employed to describe and verify the behavioral characteristics of the FCS. The results showed that the designed FCS, after required modifications and enhacements, successfully satisfies the requirements and can be the basis for advanced design stages. Keywords: AADL, Flight Control, Formal method, avionics, Error model, SSA. Isfahan
