Abstract
We present a theoretically sound and automated model-based design, analysis, and implementation framework for synthesizing correct-by-construction code. Special emphasis is put on multi-threaded software and multi-processor architectures. The framework consists in (1) a formal language which provides platform-independent constructs to specify the behavior of an application using an abstract execution model, and (2) a compilation chain for refining the application abstract model into its concrete implementation on a target platform. The prototype Jahuel is currently being used for developing experimental industrial applications.
Contact: Sergio.Yovine@imag.fr. Partially supported by MEDEA+ Project NEVA.
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
Assayad, I., Gerner, P., Yovine, S., Bertin, V.: Modelling, analysis and implementation of an on-line video encoder. In: DFMA 2005, IEEE Computer Society, Los Alamitos (2005)
Inf. tech - Coding of audio-visual objects - P. 2: Visual. Prentice Hall, ISO/IEC 14496-2:2001
Bertin, V., Daveau, J.M., Guillaume, P., Lepley, T., Pilat, D., Richard, C., Santana, M., Thery, T.: FlexCC2: An optimizing retargetable C compiler for DSP proc. In: Sangiovanni-Vincentelli, A.L., Sifakis, J. (eds.) EMSOFT 2002. LNCS, vol. 2491. Springer, Heidelberg (2002)
Binns, P., Vestal, S.: Formalizing software architectures for embedded systems. In: Henzinger, T.A., Kirsch, C.M. (eds.) EMSOFT 2001. LNCS, vol. 2211, p. 451. Springer, Heidelberg (2001)
Burns, A., Wellings, A.: Concurrency in Ada. Cambridge University Press, Cambridge (1998)
Caspi, P., Curic, A., Maignan, A., Sofronis, C., Tripakis, S., Niebert, P.: From Simulink to SCADE/Lustre to TTA: a layered approach for distrib. embedded applications. In: LCTES 2003 (2003)
Darte, A., Robert, Y., Vivien, F.: Scheduling and Automatic Parallelization. Birkhäuser, Boston (2000)
Goguen, J., Malcolm, G.: Algebraic Semantics of Imperative Programs. MIT Press, Cambridge (1996)
Goguen, J., Wang, G., Nam, Y.-K., Lin, K.: Abstract schema morphisms and schema matching generation. Tech. Rep. DCSE, UCSD (2004)
Groppa, W., Lusk, E., Skjellum, A.: Using MPI. Scientific and Engineering Computation, 2nd edn. MIT Press, Cambridge (1999)
Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous dataflow programming language Lustre. In: Proc. IEEE, vol. 79(9) (September 1991)
Hammond, L., Nayfeh, B.A., Olukotun, K.: A single-chip multiprocessor. Comp. 30(9) (1997)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Englewood Cliffs (1985)
Karsai, G., Sztipanovits, J., Ledeczi, A., Bapty, T.: Model-integrated development of embedded software. In: Proc. IEEE, vol. 91(1) (2003)
Kersten, M.: Comparison of the leading AOP tools. In: Aspect-Oriented Software Development, AOSD 2005 (2005) Industry track. Invited talk
Kloukinas, C., Nakhli, C., Yovine, S.: A Methodology and Tool Support for Generating Scheduled Native Code for Real-Time Java Applications. In: Alur, R., Lee, I. (eds.) EMSOFT 2003. LNCS, vol. 2855, pp. 274–289. Springer, Heidelberg (2003)
Kloukinas, C., Yovine, S.: Synthesis of Safe, QoS Extendible, Application Specific Schedulers for Heterogeneous Real-Time Systems. In: ECRTS 2003 (2003)
Sangiovanni-Vincentelli, A.: Defining platform-based design. EEDesign, February 5 (2002)
Schlett, M.: Trends in embedded-microprocessor design. IEEE Computer 31(8) (1998)
Sifakis, J.: Modeling real-time systems - challenges and work directions. In: Henzinger, T.A., Kirsch, C.M. (eds.) EMSOFT 2001. LNCS, vol. 2211, p. 373. Springer, Heidelberg (2001)
Sifakis, J., Tripakis, S., Yovine, S.: Building models of real-time systems from application software. Proceedings of the IEEE 91(1), 100–111 (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Assayad, I., Bertin, V., Defaut, F.X., Gerner, P., Quévreux, O., Yovine, S. (2005). Jahuel: A Formal Framework for Software Synthesis. In: Lau, KK., Banach, R. (eds) Formal Methods and Software Engineering. ICFEM 2005. Lecture Notes in Computer Science, vol 3785. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11576280_15
Download citation
DOI: https://doi.org/10.1007/11576280_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29797-0
Online ISBN: 978-3-540-32250-4
eBook Packages: Computer ScienceComputer Science (R0)