Advertisement

Translation Validation for Synchronous Data-Flow Specification in the SIGNAL Compiler

  • Van Chan NgoEmail author
  • Jean-Pierre Talpin
  • Thierry Gautier
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9039)

Abstract

We present a method to construct a validator based on translation validation approach to prove the value-equivalence of variables in the compilation of the Signal compiler. The computation of output signals in a Signal program and their counterparts in the generated C code is represented by a Synchronous Data-flow Value-Graph (Sdvg). Our validator proves that every output signal and its counterpart variable have the same values by transforming the Sdvg graph.

Keywords

Value-Graph Graph transformation Formal verification Translation validation Certified compiler Synchronous programs 

References

  1. 1.
    Aubry, P., Guernic, P.L., Machard, S.: Synchronous distribution of signal programs. In: Proceedings of the 29th Hawaii International Conference on System Sciences, vol. 1, pp. 656–665. IEEE Computer Society Press (1996)Google Scholar
  2. 2.
    Ballance, R., Maccabe, A., Ottenstei, K.: The program dependence web: A representation supporting control, data, and demand driven interpretation of imperative languages. In: Proc. of the SIGPLAN 1990 Conference on Programming Language Design and Implementation, pp. 257–271 (1990)Google Scholar
  3. 3.
    Benveniste, A., Guernic, P.L.: Hybrid dynamical systems theory and the signal language. IEEE Transactions on Automatic Control 35(5), 535–546 (1990)CrossRefzbMATHGoogle Scholar
  4. 4.
    Besnard, L., Gautier, T., Guernic, P.L., Talpin, J.-P.: Compilation of polychronous data-flow equations. In: Synthesis of Embedded Software, pp. 01–40. Springer (2010)Google Scholar
  5. 5.
    Blazy, S.: Which c semantics to embed in the front-end of a formally verified compiler? In: Tools and Techniques for Verification of System Infrastructure, TTVSI (2008)Google Scholar
  6. 6.
    Gautier, T., Guernic, P.L.: Code generation in the sacres project. In: Towards System Safety, Proceedings of the Safety-critical Systems Symposium, pp. 127–149 (1999)Google Scholar
  7. 7.
    Gautier, T., Guernic, P.L., Besnard, L.: SIGNAL: A declarative language for synchronous programming of real-time systems. In: Kahn, G. (ed.) FPCA 1987. LNCS, vol. 274, pp. 257–277. Springer, Heidelberg (1987)CrossRefGoogle Scholar
  8. 8.
    Maffeis, O., Guernic, P.L.: Distributed implementation of SIGNAL: Scheduling & graph clustering. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994 and ProCoS 1994. LNCS, vol. 863, pp. 547–566. Springer, Heidelberg (1994)CrossRefGoogle Scholar
  9. 9.
    Ngo, V.C.: Formal verification of a synchronous data-flow compiler: from signal to c. Ph.D Thesis (2014), http://tel.archives-ouvertes.fr/tel-01058041
  10. 10.
    Ngo, V.C., Talpin, J.-P., Gautier, T., Guernic, P.L., Besnard, L.: Formal verification of compiler transformations on polychronous equations. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds.) IFM 2012. LNCS, vol. 7321, pp. 113–127. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  11. 11.
    Ngo, V.C., Talpin, J.-P., Gautier, T., Guernic, P.L., Besnard, L.: Formal verification of synchronous data-flow program transformations toward certified compilers. Frontiers of Computer Science, Special Issue on Synchronous Programming 7(5), 598–616 (2013)MathSciNetGoogle Scholar
  12. 12.
    Pnueli, A., Shtrichman, O., Siegel, M.: Translation validation: From SIGNAL to C. In: Olderog, E.-R., Steffen, B. (eds.) Correct System Design. LNCS, vol. 1710, pp. 231–255. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  13. 13.
    Pnueli, A., Siegel, M., Singerman, E.: Translation validation. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 151–166. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  14. 14.
    Tate, R., Stepp, M., Tatlock, Z., Lerner, S.: Equility saturation: A new approach to optimization. In: 36th Principles of Programming Languages, pp. 264–276 (2009)Google Scholar
  15. 15.
    Tristan, J.-B., Govereau, P., Morrisett, G.: Evaluating value-graph translation validation for llvm. In: ACM SIGPLAN Conference on Programming and Language Design Implementation (2011)Google Scholar
  16. 16.
    Weise, D., Crew, R., Ernst, M., Steensgaard, B.: Value dependence graphs: Representation without taxation. In: 21st Principles of Programming Languages, pp. 297–310 (1994)Google Scholar

Copyright information

© IFIP International Federation for Information Processing 2015

Authors and Affiliations

  • Van Chan Ngo
    • 1
    Email author
  • Jean-Pierre Talpin
    • 1
  • Thierry Gautier
    • 1
  1. 1.INRIARennesFrance

Personalised recommendations