Abstract
As safety critical systems increase in size and complexity, the need for efficient tools to verify their reliability grows. In this paper we present a tool that helps engineers design safe and reliable systems. Systems are reliable if they keep operating safely when components fail. Our tool is at the core of the Scade Design Verifier integrated within Scade, a product developed by Esterel Technologies. Scade includes a graphical interface to build formal models in the synchronous data-flow language Lustre. Our tool automatically extends Lustre models by injecting faults, using libraries of typical failures. It allows to perform Failure Mode and Effect Analysis, which consists of verifying whether systems remain safe when selected components fail. The tool can also compute minimal combinations of failures breaking systems’ safety, which is similar to Fault Tree Analysis. The paper includes successful verifications of examples from the aeronautics industry.
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
Andersson, G., Bjesse, P., Cook, B., Hanna, Z.: A proof engine approach to solving combinational design automation problems. In: Proceedings of the 39th conference on Design automation, pp. 725–730. ACM Press, New York (2002)
Audemard, G., Bertoli, P., Cimatti, A., Kornilowicz, A., Sebastiani, R.: A SAT based approach for solving formulas over boolean and linear mathematical propositions. In: Voronkov, A. (ed.) CADE 2002. LNCS, vol. 2392, pp. 195–210. Springer, Heidelberg (2002)
Ben-Ari, M., Pnueli, A., Manna, Z.: The temporal logic of branching time. Acta Informatica 20, 207–226 (1983)
Bieber, P., Castel, C., Seguin, C.: Combination of fault tree analysis and model-checking for safety assessment of complex system. In: Bondavalli, A., Thévenod-Fosse, P. (eds.) EDCC 2002. LNCS, vol. 2485, pp. 19–31. Springer, Heidelberg (2002)
Bozzano, M., Villafiorita, A.: Improving system reliability via model checking: The FSAP/NuSMV-SA safety analysis platform. In: Anderson, S., Felici, M., Littlewood, B. (eds.) SAFECOMP 2003. LNCS, vol. 2788, pp. 49–62. Springer, Heidelberg (2003)
Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. on Computers C-35(8), 677–691 (1986)
Caspi, P., Pilaud, D., Halbwachs, N., Plaice, J.: Lustre: a declarative language for programming synchronous systems. In: 14th ACM Symposium on Principles of Programming Languages, Munchen (January 1987)
Cimatti, A., et al.: NuSMV2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)
Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods in System Design 19(1), 7–34 (2001)
Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specification. ACM Trans. on Programming Languages and Systems 8(2), 244–263 (1986)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5(7), 394–397 (1962)
Dutuit, Y., Rauzy, A.: Exact and truncated computations of prime implicants of coherent and non-coherent fault trees within Aralia. Reliability Engineering and System Safety (1997)
Griffault, A., Lajeunesse, S., Point, G., Rauzy, A., Signoret, J.P., Thomas, P.: The AltaRica language. In: Proceedings of the International Conference on Safety and Reliability, ESREL 1998, June 20-24. Balkema Publishers (1998)
Holzmann, G.J.: The model checker SPIN. IEEE Trans. on Software Engineering SE-23(5), 279–295 (1997)
McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)
Papadopoulos, Y., Maruhn, M.: Model-based synthesis of fault trees from Matlab-Simulink models. In: Proc. International Conference on Dependable Systems and Networks, pp. 77–82 (2001)
Pnueli, A.: The temporal logic of programs. In: Proc.18th Annual Symp. Foundations of Computer Science, pp. 46–57. IEEE, Los Alamitos (1977)
Ravi, K., Somenzi, F.: Minimal assignments for bounded model checking. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 31–45. Springer, Heidelberg (2004)
Sheeran, M., Singh, S., Stålmarck, G.: Checking Safety Properties Using Induction and a SAT-Solver. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 108–125. Springer, Heidelberg (2000)
Sheeran, M., Stålmarck, G.: A Tutorial on Stålmarck’s Proof Procedure for Propositional Logic. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522, pp. 82–99. Springer, Heidelberg (1998)
Esterel Technologies. Scade suite do-178b qualified code generator, http://www.esterel-technologies.com/products/scade-suite/do-178b-code-generation.html
Vesely, W.E., Goldberg, F.F., Roberts, N.H., Haasl, D.F.: Fault Tree Handbook. U. S. Nuclear Regulatory Commission, NUREG-0492, Washington DC (1981)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Abdulla, P.A., Deneux, J., Stålmarck, G., Ågren, H., Åkerlund, O. (2006). Designing Safe, Reliable Systems Using Scade. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods. ISoLA 2004. Lecture Notes in Computer Science, vol 4313. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11925040_8
Download citation
DOI: https://doi.org/10.1007/11925040_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-48928-3
Online ISBN: 978-3-540-48929-0
eBook Packages: Computer ScienceComputer Science (R0)