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.
Chapter PDF
Similar content being viewed by others
Keywords
References
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)
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)
Benveniste, A., Guernic, P.L.: Hybrid dynamical systems theory and the signal language. IEEE Transactions on Automatic Control 35(5), 535–546 (1990)
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)
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)
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)
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)
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)
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
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)
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)
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)
Pnueli, A., Siegel, M., Singerman, E.: Translation validation. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 151–166. Springer, Heidelberg (1998)
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)
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)
Weise, D., Crew, R., Ernst, M., Steensgaard, B.: Value dependence graphs: Representation without taxation. In: 21st Principles of Programming Languages, pp. 297–310 (1994)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 IFIP International Federation for Information Processing
About this paper
Cite this paper
Chan Ngo, V., Talpin, JP., Gautier, T. (2015). Translation Validation for Synchronous Data-Flow Specification in the SIGNAL Compiler. In: Graf, S., Viswanathan, M. (eds) Formal Techniques for Distributed Objects, Components, and Systems. FORTE 2015. Lecture Notes in Computer Science(), vol 9039. Springer, Cham. https://doi.org/10.1007/978-3-319-19195-9_5
Download citation
DOI: https://doi.org/10.1007/978-3-319-19195-9_5
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-19194-2
Online ISBN: 978-3-319-19195-9
eBook Packages: Computer ScienceComputer Science (R0)