Abstract
Scade is an industrial strength synchronous language and tool suite for the development of the software of safety-critical systems. It supports formal verification using the so-called Design Verifier. Here we start developing a freely available alternative to the Design Verifier intended to support the academic study of verification techniques tailored for SCADE programs. Inspired by work of Hagen and Tinelli on the SMT-based verification of LUSTRE programs, we develop an SMT-based verification method for Scade programs. We introduce Lama as an intermediate language into which Scade programs can be translated and which easily can be transformed into SMT solver instances. We also present first experimental results of our approach using the SMT solver Z3.
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
Abdulla, P.A., Deneux, J., Stålmarck, G., Ågren, H., Åkerlund, O.: Designing safe, reliable systems using scade. In: Margaria, T., Steffen, B. (eds.) ISoLA 2004. LNCS, vol. 4313, pp. 115–129. Springer, Heidelberg (2006)
André, C.: Semantics of S.S.M (Safe State Machine). Tech. Rep. UMR 6070, I3S Laboratory, University of Nice-Sophia Antipolis (2003), http://rw4.cs.uni-saarland.de/teaching/esd07/papers/SSMsemantics.pdf
Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, ch. 26, pp. 825–885. IOS Press (2009)
Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0. In: Proc. 8th Intern. Workshop on Satisfiability Modulo Theories, Edinburgh, UK (2010)
Basold, H.: Transformationen von Scade-Modellen zur SMT-basierten Verifikation. Master’s thesis, TU Braunschweig (2012), http://arxiv.org/abs/1403.2752
Bjesse, P., Claessen, K.: SAT-based verification without state space traversal. In: Hunt Jr., W.A., Johnson, S.D. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 372–389. Springer, Heidelberg (2000)
Cardelli, L.: Type systems. In: Tucker, A.B. (ed.) CRC Handbook of Computer Science and Engineering, ch. 97. Chapman and Hall (2004)
CENELEC: EN 50128 – Railway Applications – Software for Railway Control and Protection Systems. European Standard (2012)
Champion, A., Delmas, R., Dierkes, M.: Generating property-directed potential invariants by backward analysis. In: Proc. FTSCS. EPTCS, vol. 105, pp. 22–38 (2012)
Colaço, J.L., Pagano, B., Pouzet, M.: A conservative extension of synchronous data-flow with state machines. In: EMSOFT, pp. 173–182. ACM Press (2005)
DO-178B: Software considerations in airborne systems and equipment certification (December 2011)
Dutertre, B., de Moura, L.: The YICES SMT solver. Tech. rep., SRI Int. (2006)
Esterel: Scade language reference manual (2011)
Franzén, A.: Using satisfiability modulo theories for inductive verification of Lustre programs. Electr. Notes Theor. Comput. Sci. 144(1), 19–33 (2006)
Hagen, G.: Verifying safety properties of Lustre programs: an SMT-based approach. Ph.D. thesis, Department of Computer Science. The University of Iowa (2008)
Hagen, G., Tinelli, C.: Scaling up the formal verification of Lustre programs with SMT-based techniques. In: Proc. FMCAD, pp. 1–9 (2008)
Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous dataflow programming language lustre. Proceedings of the IEEE 79(9), 1305–1320 (1991)
Halbwachs, N., Lagnier, F., Raymond, P.: Synchronous observers and the verification of reactive systems. In: Proc. of AMAST 1993. Workshops in Computing, pp. 83–96. Springer, London (1994)
Halbwachs, N., Raymond, P.: A turotial of Lustre (2002), http://www-verimag.imag.fr/~halbwach/lustre-tutorial.html (last accessed: March 13, 2014)
Huhn, M., Milius, S.: Observations on formal safety analysis in practice. Science of Computer Programming 80, Part A, 150–168 (2014)
Jeannet, B.: The NBAC verification/slicing tool, http://pop-art.inrialpes.fr/people/bjeannet/nbac/index.html (last accessed: February 17, 2014)
Kahsai, T., Tinelli, C.: PKind: A parallel k-induction based model checker. In: Barnat, J., Heljanko, K. (eds.) PDMC. EPTCS, vol. 72, pp. 55–62 (2011)
Ljung, M.: Formal modelling and automatic verification of Lustre programs using NP-Tools. Master’s thesis, Prover Technology AB and Department of Teleinformatics, KTH, Stockholm (1999)
Maraninchi, F., Rémond, Y.: Mode-automata: About modes and states for reactive systems. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, pp. 185–199. Springer, Heidelberg (1998)
de Moura, L., Owre, S., Shankar, N.: The SAL language manual. Tech. rep., SRI International (2003), http://sal.csl.sri.com/doc/language-report.pdf (last accessed: March 12, 2014)
de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Pace, G., Halbwachs, N., Raymond, P.: Counter-example generation in symbolic abstract model-checking. Int. J. Software Tools and Technology Transfer 5(2), 158–164 (2004)
Sheeran, M., Singh, S., Stålmarck, G.: Checking safety properties using induction and a SAT-solver. In: Hunt Jr., W.A., Johnson, S.D. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 108–125. Springer, Heidelberg (2000)
Whalen, M., Cofer, D., Miller, S., Krogh, B.H., Storm, W.: Integration of formal analysis into a model-based software development process. In: Leue, S., Merino, P. (eds.) FMICS 2007. LNCS, vol. 4916, pp. 68–84. Springer, Heidelberg (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Basold, H., Günther, H., Huhn, M., Milius, S. (2014). An Open Alternative for SMT-Based Verification of Scade Models. In: Lang, F., Flammini, F. (eds) Formal Methods for Industrial Critical Systems. FMICS 2014. Lecture Notes in Computer Science, vol 8718. Springer, Cham. https://doi.org/10.1007/978-3-319-10702-8_9
Download citation
DOI: https://doi.org/10.1007/978-3-319-10702-8_9
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10701-1
Online ISBN: 978-3-319-10702-8
eBook Packages: Computer ScienceComputer Science (R0)