Formal Refinement Checking in a System-level Design Methodology

• Autorzy: Talpin J.-P. , Le Guernic P. , Shukla S.K. , Doucet F. , Gupta R.
• Konferencja: Third International Conference on Application of Concurrency to System Design (ACSD'03) (18-20 June, 2003, Guimaraes, Portugal)
• Języki publikacji: EN

Abstrakty

EN

Rising complexity, increasing performance requirements, and shortening time-to-market demands necessitate newer design paradigms for embedded system design. Such newer design methodologies require raising the level of abstraction for design entry, reuse of intellectual property blocks as virtual components, refinement based design, and formal verification to prove correctness of refinement steps. The problem of combining various components from different designers and companies, designed at different levels of abstraction, and embodying heterogeneous models of computation is a difficult challenge for the designer community today. Moreover, one of the gating factors for widespread adoption of the system-level design paradigm is the lack of formal models, method and tools to support refinement. In the absence of provably correct and adequate behavioral synthesis techniques, the refinement of a system-level description towards its implementation is primarily a manual process. Furthermore, proving that the implementation preserves the properties of the higher system-level design-abstraction is an outstanding problem. In this paper, we address these issues and define a formal refinement-checking methodology for system-level design. Our methodology is based on a polychronous model of computation of the multi-clocked synchronous formalism Signal. This formalism is implemented in the Polychrony workbench. We demonstrate the effectiveness of our approach by the experimental case study of a SpecC modeling example. First, we define a technique to systematically model SpecC programs in the Signal formalism. Second, we define a methodology to compare system-level models of SpecC programs and to validate behavioral equivalence relations between these models at different levels of abstraction. Although we use SpecC modeling examples to illustrate our technique, our methodology is generic and language-independent and the model that supports it conceptually minimal by offering a scalable notion and a flexible degree of abstraction.

Słowa kluczowe

EN

embedded computer systems; abstract thought; intellectual property

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2004
• Tom: Vol. 62, nr 2
• Strony: 243--273
• Opis fizyczny: Bibliogr. 37 poz., wykr.

Twórcy

autor

Talpin J.-P.

• Inria-Irisa, Campus de Beaulieu, 35042 Rennes, France

autor

Le Guernic P.

• Inria-Irisa, Campus de Beaulieu, 35042 Rennes, France

autor

Shukla S.K.

• Virginia Tech, Electrical and Computer Engineering, Blacksburg, VA24061, USA

autor

Doucet F.

• University of California at San Diego, Department of Computer Science and Engineering, AP&M3111 9500 Gilman Drive, La Jolla, CA 92093-0114, USA

autor

Gupta R.

• University of California at San Diego, Department of Computer Science and Engineering, AP&M3111 9500 Gilman Drive, La Jolla, CA 92093-0114, USA

Bibliografia

• [1] Abramsky, S., Gay. S. J., Nagarajan, R. Interaction categories and the foundations of typed concurrent programming. In Deductive Program Design: Proceedings of the 1994 Marktoberdorf International Summer School. Nato Asi Series F, Springer-Verlag, 1996.
• [2j Abrial, J.-R. The B Book - Assigning Programs to Meanings. Cambridge University Press, August 1996.
• [3] Amagbegnon, T. P., Besnard, L., Le Guemic, P. "Implementation of the data-flow synchronous language Signal". In Conference on Programming Language Design and Implementation. ACM Press, 1995.
• [4] Benveniste, A., Caspi, P., Carloni, L. P., Sangiovanni-Vincentelli, A. L. "Heterogeneous Reactive Systems Modeling and Correct-by-Construction Deployment". In Embedded Software Conference. Springer Verlag, October 2003.
• [5] Benveniste, A., Caspi, P., Edwards, S., Halbwachs, N.., Le Guernic, P., De Simone. R. "The synchronous languages twelve years later". In Proceedings of the IEEE, special issue on embedded systems. IEEE Press, January 2003.
• [6] Benveniste, A., Caspi, P., Le Guernic, P., Marchand. H., Talpin. J.-P., Tripakis, S. "A protocol for loosely time-triggered architectures". In Embedded Software Conference. Springer Verlag, October 2002.
• [7] Benveniste, A., Le Guemic, P., Jacquemot, C. "Synchronous programming with events and relations: the SIGNAL language and its semantics". In Science of Computer Programming, v. 16. Elsevier. 1991.
• [8] Berry, G., Gonthier, G. "The Esterel synchronous programming language: design, semantics, implementation". In Science of Computer Programming, v. 19, 1992.
• [9] Buck, J., Ha, S., Lee, A., and Messerschmitt, D. Ptolemy: A Framework for Simulating and Prototyping Heterogeneous Systems. In International Journal of Computer Simulation, special issue on "Simulation Software Development", v. 4. Ablex, April 1994.
• [10] Carloni, L. P., McMillan, K. L., Sangiovanni-Vincentelli, A. L. "Latency-Insensitive Protocols". In International Conference on Computer-Aided Verification. Lecture notes in computer science v. 1633. Springer Verlag. July 1999.
• [11] Chandy K.M., Misra J. Parallel Program Design: A Foundation. Addison Wesley, 1999.
• [12] De Micheli. G., Ernst, E., and Wolf, W. "Readings in Hardware/Software Co-Design". Morgan Kaufmann, 2001.
• [13] F. Doucet. F., Otsuka, M., Shukla, S., Gupta, R. An environment for dynamic component composition for efficient co-design. In Design Automation and Test in Europe. Ieee Press, 2002.
• [14] Gamatie. A., Gautier, T. "Synchronous modeling of avionics applications using the SIGNAL language". In Real-time embedded technology and applications symposium. Ieee Press, 2002.
• [15] Gajski, D., Zhu, J., Dbmer. R., Gerstlauer, A., Zhao, S. SPECC: Specification Language and Methodology. Kluwer Academic Publishers, March 2000.
• [16] Groetker, T. Liao. S., Martin. G., Swan, S. System Design with SYSTEMC. Kluwer Academic Publishers, May 2002.
• [17] Hoare, C. Communicating sequential processes. Prentice Hall. 1985.
• [18] Kahn, G. The semantics of a simple language for parallel programming. In 1fip Congress. North Holland. 1974.
• [19] Kerboeuf. M., Nowak, D., Talpin, J.-P. "The steam-boiler problem in SIGNAL-COQ". International Conference on Theorem Proving in Higher-Order Logics (TPHOLS). Springer Verlag Lectures Notes in Computer Science, Aout 2000.
• [20] Kerboeuf, M., Nowak, D., Talpin, J.-P. "Formal proof of a polychronous protocol for loosely time-triggered architectures'". International conference on formal engineering methods. Springer Verlag Lectures Notes in Computer Science, Novembre 2003.
• [21] Lee, E., Sangiovanni-Vincentelli, A. "A framework for comparing models of computation". In IEEE transactions on computer-aided design, V. 17, n. 12. IEEE Press, December 1998.
• [22] Le Guemic. P., Talpin, J.-P., Le Lann, J.-L. Polychrony for system design. In Journal of Circuits, Systems and Computers. Special Issue on Application Specific Hardware Design. World Scientific, 2002.
• [23] Marchand, H., Bournai. P., Le Borgne, M., Le Guernic, P. Synthesis of Discrete-Event Controllers based on the Signal Environment. In Discrete Event Dynamic System: Theory and Applications, v. 10{4), pp. 325-346, 2000.
• [24] H. Marchand, E. Rutten, M. Le Borgne, M. Samaan. Formal Verification of SIGNAL programs: Application to a Power Transformer Station Controller. Science of Computer Programming, v. 41(1), pp. 85-104, 2001.
• [25] Nowak, D., Beauvais, J.-R., Talpin, J.-P. "Co-inductive axiomatization of a synchronous language". In International Conference on Theorem Proving in Higher-Order Logics. Springer Verlag, October 1998.
• [26] Nowak, D., Talpin. J.-P. Gautier, T, Le Guernic, P. "An ML-like module system for the synchronous language Signal", Proceedings of European Conference on Parallel Processing (EuroPAR). Springer Verlag Lectures Notes in Computer Science, Aout 1997.
• [27] Nowak, D., Talpin, J. P., Le Guernic, P. "Synchronous structures". In International Conference on Concurrency Theory. Springer Verlag, August 1999.
• [28] The Polychrony workbench, available from http://www. irisa.fr/espresso/Polychrony.
• [29] Roscoe, A. W. The Theory and Practice of Concurrency. Prentice-Hall, 1997.
• [30] The SPECC website, http: //www. ics.uci.edu/~specc.
• [31] The SYSTEMC website, http://www.systemc.org.
• [32] The System Verilog website, http://www.systemverilog.org.
• [33] The Gnu Compiler Collection (GCC). http://http://gcc.gnu.org, 2004.
• [34] The GCC Tree-SSA Branch, http://gcc.gnu.org/projects/tree-ssa, 2004.
• [35] Talpin, J.-P., Gamatie, A., Le Dez, B., Bemer, D., Le Guernic, P. Hard real-time implementation of embedded software in JAVA. In International workshop on scientific engineering of distributed JAVA applications. Lectures Notes in Computer Science, Springer Verlag, November 2003.
• [36] Talpin, J.-P, Le Guernic, P., Shukia, S., Gupta, R., Doucet, F. "Polychrony for formal refinement-checking in a system-level design methodology". Application of Concurrency to System Design. IEEE Press, June 2003.
• [37] Talpin, J.-P., Bemer, D., Shukia, S. K., Le Guernic, P., Gupta, R. "A behavioral type inference system for compositional system design". Application of Concurrency to System Design. IEEE Press, 2004.