Paper Info
Title
Formal Verification of an Avionics Sensor Voter Using SCADE
Abstract
Redundancy management is widely utilized in mission critical digital flight control systems. This study focuses on the use of SCADE (Safety Critical Application Development Environment) 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, captured as a Simulink diagram, 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.
Year
DOI
Venue
2004
10.1007/978-3-540-30206-3_3
LECTURE NOTES IN COMPUTER SCIENCE
Keywords
Field
DocType
model checking,application development,formal verification
Model checking,Embedded software,Computer science,Correctness,Avionics,Redundancy (engineering),Mission critical,Formal methods,Computer engineering,Embedded system,Distributed computing,Formal verification
Conference
Volume
ISSN
Citations 
3253
0302-9743
11
PageRank 
References 
Authors
0.73
11
3
Name
Order
Citations
PageRank
Samar Dajani-brown1423.50
Darren D. Cofer221420.08
Amar Bouali315412.50