Abdoulaye Gamatie
ABSTRACT
In this paper, we propose a sound abstraction for an efficient static analysis of synchronous programs describing multi-clock embedded systems in Signal. This abstraction combines the Boolean theory and numeric interval approximation to adequately address clock relations defined as combinations of logical and numerical expressions. Through a few examples, we show how the proposed solution is used to determine absence of reaction captured by empty clocks; mutual exclusion captured by two or more clocks whose associated signals never occur at the same time; or hierarchical control of component activations via clock inclusion. We also show this analysis improves the quality of the code generated automatically by the Signal compiler, e.g., a code with smaller footprint, or a code executed more efficiently thanks to optimizations enabled by the new abstraction.
- G. Alefeld and J. Hertzberger. Introduction to Interval Computation. Academic Press, NY, 1983.Google Scholar
- T. Amagbegnon, L. Besnard, and P. Le Guernic. Arborescent canonical form of Boolean expressions. Technical Report 2290, INRIA, June 1994. URL www.inria.fr/rrrt/rr-2290.html.Google Scholar
- C. Barrett, S. Ranise, A. Stump, and C. Tinelli. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org, 2008.Google Scholar
- A. Benveniste, P. Caspi, S. Edwards, N. Halbwachs, P. Le Guernic, and R. de Simone. The synchronous languages twelve years later. In Special issue on Embedded Systems, IEEE, 2003.Google Scholar
- G. Berry. The foundations of ESTEREL. In Proof, Language and Interaction: Essays in Honour of Robin Milner. MIT Press, 2000. Google ScholarDigital Library
- F. Besson, T. Jensen, and J.-P. Talpin. Polyhedral analysis for synchronous languages. In Proceedings of the 6th International Symposium on Static Analysis, volume 1694 of Lecture Notes in Computer Science, pages 51--68. Springer-Verlag, September 1999. Google ScholarDigital Library
- A. Biere, A. Biere, M. Heule, H. van Maaren, and T. Walsh. Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications. IOS Press, Amsterdam, The Netherlands, 2009. Google ScholarDigital Library
- R. Bryant. Graph-based algorithms for boolean function manipulation. IEEE transactions on computers, C-35(8):677--691, August 1986. Google ScholarDigital Library
- D. Chapiro. Globally Asynchronous Locally Synchronous Systems. PhD thesis, Stanford University, 1984. Google ScholarDigital Library
- P. Cousot and R. Cousot. Static determination of dynamic properties of programs. In Proceedings of the Second International Symposium on Programming, pages 106--130. Dunod, Paris, France, 1976.Google Scholar
- R. Cytron, J. Ferrante, B. K. Rosen, M. N.Wegman, and F. K. Zadeck. Efficiently computing static single assignment form and the control dependence graph. ACM Trans. Program. Lang. Syst., 13:451--490, October 1991. ISSN 0164-0925. Google ScholarDigital Library
- L. de Moura and N. Bjorner. Satisfiability Modulo Theories: An Appetizer. In Brazilian Symposium on Formal Methods (SBMF'2009), Gramado, Brazil, August 2009. Google ScholarDigital Library
- B. Dutertre and L. de Moura. Yices sat-solver. http://yices.csl.sri.com/, 2009.Google Scholar
- J. Ferrante, K. J. Ottenstein, and J. D. Warren. The program dependence graph and its use in optimization. ACM Trans. Program. Lang. Syst., 9:319--349, July 1987. ISSN 0164-0925. Google ScholarDigital Library
- A. Gamatié. Designing Embedded Systems with the SIGNAL Programming Language: Synchronous, Reactive Specification. Springer, New York, 2009. ISBN 978-1-4419-0940-4. Google ScholarDigital Library
- A. Gamatié, T. Gautier, and P. Le Guernic. Towards static analysis of SIGNAL programs using interval techniques. In Synchronous Languages, Applications, and Programming (SLAP'06), March 2006.Google Scholar
- A. Gamatié, T. Gautier, and L. Besnard. An Interval-Based Solution for Static Analysis in the SIGNAL Language. In 15th IEEE Conference andWorkshop on Engineering of Computer Based Systems (ECBS'2008), Belfast, Northern Ireland, pages 182--190, April 2008. Google ScholarDigital Library
- L. Gonnord and N. Halbwachs. Abstract acceleration to improve precision of linear relation analysis. Research report, Verimag, 03 2010. URL http://laure.gonnord.org/pro/papers/rr-verimag10.pdf.Google Scholar
- G. Hagen and C. Tinelli. Scaling up the formal verification of LUSTRE programs with smt-based techniques. In FMCAD '08: Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design, pages 1--9, Piscataway, NJ, USA, 2008. IEEE Press. ISBN 978-1-4244-2735-2. Google ScholarDigital Library
- N. Halbwachs. A synchronous language at work: the story of LUSTRE. In 3th ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'05), Verona, Italy, july 2005. Google ScholarDigital Library
- N. Halbwachs, F. Lagnier, and C. Ratel. Programming and verifying real-time systems by means of the synchronous data-flow programming language LUSTRE. IEEE Transactions on Software Engineering, 18(9):785--793, September 1992. Google ScholarDigital Library
- N. Halbwachs, Y.-E. Proy, and P. Roumanoff. Verification of real-time systems using linear relation analysis. Formal Methods in System Design: An International Journal, 11(2):157--185, August 1997. Google ScholarDigital Library
- B. Jeannet. Dynamic partitioning in linear relation analysis. application to the verification of reactive systems. Formal Methods in System Design, 23(1):5--37, July 2003. Google ScholarDigital Library
- G. Lalire, M. Argoud, and B. Jeannet. Interproc : an interprocedural analyzer for imparative languages. http://pop-art.inrialpes.fr/people/bjeannet/bjeannet-forge/interproc, 2009.Google Scholar
- P. Le Guernic and T. Gautier. Advanced Topics in Data-Flow Computing, chapter Data-Flow to von Neumann: the SIGNAL approach, pages 413--438. Prentice-Hall, J.-L. Gaudiot and L. Bic eds., 1991.Google Scholar
- P. Le Guernic, J.-P. Talpin, and J.-C. Le Lann. Polychrony for System Design. Journal for Circuits, Systems and Computers, 12(3):261--304, April 2003.Google Scholar
- G. Magklis, G. Semeraro, D. Albonesi, S. Dropsho, S. Dwarkadas, and M. Scott. Dynamic frequency and voltage scaling for a multipleclock- domain microprocessor. Micro, IEEE, 23(6):62--68, November 2003. ISSN 0272-1732. doi: 10.1109/MM.2003.1261388. Google ScholarDigital Library
- J. Muttersbach, T. Villiger, and W. Fichtner. Practical design of globally asychronous locally synchronous systems. In International Symposium on Advanced Research in Asynchronous Circuits and Systems (ASYNC'00), pages 52--61, 2000. Google ScholarDigital Library
- M. Nebut. Specification and analysis of synchronous reactions. Formal Aspects of Computing, 16(3):263--291, august 2004. Google ScholarCross Ref
- A. Stump and M. Deters. The SMT-COMP 2009 Website, 2009. http://www.smtcomp.org/2009.Google Scholar
Index Terms
- Static analysis of synchronous programs in signal for efficient design of multi-clocked embedded systems
Recommendations
Static analysis of synchronous programs in signal for efficient design of multi-clocked embedded systems
LCTES '10In this paper, we propose a sound abstraction for an efficient static analysis of synchronous programs describing multi-clock embedded systems in Signal. This abstraction combines the Boolean theory and numeric interval approximation to adequately ...
SystemJ: A GALS language for system level design
In this paper we present the syntax, semantics, and compilation of a new system-level programming language called SystemJ. SystemJ is a multiclock language supporting the Globally Asynchronous Locally Synchronous (GALS) model of computation. The ...
An Implementation of Constructive Synchronous Programs in POLIS
Design tools for embedded reactive systems commonly use a model of computation that employs both synchronous and asynchronous communication styles. We form a junction between these two with an implementation of synchronous languages and circuits (...
Comments