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.
This work has been supported in part by NASA contract NAS1-00079.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Caspi, P., Curic, A., Maignan, A., Sofronis, C., Tripakis, S., Niebert, P.: From Simulink to SCADE/Lustre to TTA: a layered approach for distributed embedded applications. In: Proc. of the 2003 ACM SIGPLAN conference on Language, compiler, and tool for embedded systems, San Diego, USA (2003)
Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The Synchronous Data Flow Programming Language Lustre. Proceeding of the IEEE (September 1991)
Halbwachs, N., Lagnier, F., Raymond, P.: Synchronous observers and the verification of reactive systems. In: Third Int. Conf. on Algebraic Methodology and Software Technology, AMAST 1993, Workshop in Computing, Springer, Heidelberg (1993)
Sheeran, M., Stalmarck, G.: A tutorial on Stalmarck’s proof procedure for propositional logic, Prover Technology AB and Chalmers University of Technology, Sweden (1998)
Bjesse, P., Claessen, K.: SAT-based Verification without State Space Traversal. In: Formal Methods in Computer-Aided Design (2000)
Dajani-Brown, S., Cofer, D., Hartmann, G., Pratt, S.: Formal Modeling and Analysis of an Avionics Triplex Sensor Voter. In: Model Checking Software, 10th International SPIN Workshop, May 2003, Springer, Heidelberg (2003)
Berry, G., Bouali, A., Fornari, X., Ledinot, E., Nassor, E., de Simone, R.: ESTEREL: a formal method applied to avionic software development. Science of Computer Programming 36(1) (January 2000)
Osder, S.: Practical View of Redundancy Management Application and Theory. Journal of Guidance and Control 22(1) (January-February1999)
Collinson, R.P.G.: Introduction to Avionics. Chapman & Hall, London (1998)
McMillan, K.: Symbolic Model Checking. Kluwer Academic Publishers, Boston (1993)
Micheal, R.A.: Huth and Mark D Ryan, Logic in Computer Science Modelling and reasoning about systems. University Press, Cambridge (2000)
SMV web page, http://www-2.cs.cmu.edu/~modelcheck
Simulink weg page, http://www.mathworks.com/products/simulink
SCADE 4.1.1, Training Manual, Esterel Technologies, Montreal, Canada
SCADE 4.2, Design Verifier User Manual, Esterel Technologies, Montreal, Canada
Berry, G.: The effectiveness of Synchronous Languages for the Development of Safety-Critical Systems. white paper, Esterel Technologies (2003)
Ball, T., Levin, V., Xei, F.: Automatic Creation of Environment Models via Training. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 93–107. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dajani-Brown, S., Cofer, D., Bouali, A. (2004). Formal Verification of an Avionics Sensor Voter Using SCADE. In: Lakhnech, Y., Yovine, S. (eds) Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems. FTRTFT FORMATS 2004 2004. Lecture Notes in Computer Science, vol 3253. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30206-3_3
Download citation
DOI: https://doi.org/10.1007/978-3-540-30206-3_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23167-7
Online ISBN: 978-3-540-30206-3
eBook Packages: Springer Book Archive