Abstract
In this paper, adopting the translation validation approach, we present a formal verification process to prove the correctness of compiler transformations on systems of polychronous equations. We encode the source programs and the transformations with polynomial dynamical systems and prove that the transformations preserve the abstract clocks and clock relations of the source programs. In order to carry out the correctness proof, an appropriate relation called refinement and an automated proof method are presented. Each individual transformation or optimization step of the compiler is followed by our validation process which proves the correctness of this running. The compiler will continue its work if and only if the correctness is proved positively. In this paper, the highly optimizing, industrial compiler from the synchronous language SIGNAL to C is addressed.
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.
Similar content being viewed by others
References
Bryant, R.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers C-35(8), 677–691 (1986)
Le Borgne, M., Benveniste, A., Le Guernic, P.: Dynamical systems over Galois fields and control problems. In: Proceedings of 33th IEEE on Decision and Control, vol. 3, pp. 1505–1509 (1991)
Besnard, L., Gautier, T., Le Guernic, P., Talpin, J.-P.: Compilation of polychronous data flow equations. In: Synthesis of Embedded Software. Springer (2010)
Besnard, L., Gautier, T., Moy, M., Talpin, J.-P., Johnson, K., Maraninchi, F.: Automatic translation of C/C++ parallel code into synchronous formalism using an SSA intermediate form. In: Proceedings of the 9th Workshop on Automated Verification of Critical Systems, AVOCS (2009)
Dutertre, B., Le Borgne, M., Marchand, H.: SIGALI: un système de calcul formel pour la vérification de programmes SIGNAL. Manuel d’utilisation. Note technique, non publiée (December 1998)
Park, D.: Concurrency and Automata on Infinite Sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981)
Gamatie, A.: Designing embedded systems with the SIGNAL programming: Synchronous, Reactive Specification. Springer, New York (2009) ISBN 978-1-4419-0940-4
Le Guernic, P., Talpin, J.-P., Le Lann, J.-C.: Polychrony for system design. Journal for Circuits, Systems and Computers 12(3), 261–304 (2003)
Halbwachs, N.: A synchronous language at work: the story of LUSTRE. In: 3th ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2005) (July 2005)
Kouchnarenko, O., Pinchinat, S.: Intensional approaches for symbolic methods. Electronic Notes in Theoretical Computer Science (August 1998)
Marchand, H., Rutten, H., Le Borgne, E., Samaan, M.: Formal verification of SIGNAL programs: Application to a power transformer station controller. Science of Computer Programming 41(1), 85–104 (2001)
Polychrony Toolset, http://www.irisa.fr/espresso/Polychrony/
Peralta, J.C., Gautier, T., Besnard, L., Le Guernic, P.: LTSs for translation validation of (multi-clocked) SIGNAL specifications. In: 8th IEEE/ACM International Conference on Formal Method and Models for Codesign, MEMOCODE (2010)
Pinchinat, S., Marchand, H., Le Borgne, M.: Symbolic abstractions of automata and their application to the supervisory control problem. In: INRIA Technical Reports No 1279, pp. 1–29 (November 1999)
Pnueli, A., Shtrichman, O., Siegel, M.D.: 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)
Milner, R.: Operational and algebraic semantics of concurrent processes. Research Report ECS-LFCS-88-46, Lab. for Foundations of Computer Science, Edinburgh (February 1988)
Van Glabbeek, R.J.: The Linear Time-Branching Time Spectrum II: The Semantics of Sequential Systems with Silent Moves (Extended Abstract). In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 66–81. Springer, Heidelberg (1993)
VeriSync Project, http://www.irit.fr/Verisync/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ngo, V.C., Talpin, JP., Gautier, T., Le Guernic, P., Besnard, L. (2012). Formal Verification of Compiler Transformations on Polychronous Equations. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds) Integrated Formal Methods. IFM 2012. Lecture Notes in Computer Science, vol 7321. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-30729-4_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-30729-4_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-30728-7
Online ISBN: 978-3-642-30729-4
eBook Packages: Computer ScienceComputer Science (R0)