Subscribe

Issue No.05 - May (2010 vol.21)

pp: 641-657

Abdoulaye Gamatié , CNRS, Villeneuve d'Ascq

Thierry Gautier , INRIA, Rennes

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TPDS.2009.125

ABSTRACT

This paper presents the design of distributed embedded systems using the synchronous multiclock model of the Signal language. It proposes a methodology that ensures a correct-by-construction functional implementation of these systems from high-level models. It shows the capability of the synchronous approach to apply formal techniques and tools that guarantee the reliability of the designed systems. Such a capability is necessary and highly worthy when dealing with safety-critical systems. The proposed methodology is demonstrated through a case study consisting of a simple avionic application, which aims to pragmatically help the reader to understand the manipulated formal concepts, and to apply them easily in order to solve system correctness issues encountered in practice. The application functionality is first modeled as well as its distribution on a generic hardware architecture. This relies on the endochrony and endo-isochrony properties of Signal specifications, defined previously. The considered architectures include asynchronous communication mechanisms, which are also modeled in Signal and proved to achieve message exchanges correctly. Furthermore, the synchronizability of the different parts in the resulting system is addressed after its deployment on a specific execution platform with multirate clocks. After all these steps, a distributed code can be automatically generated.

INDEX TERMS

Distributed embedded systems, correct-by-construction design methodology, safety-critical domains, formal validation, synchronous model, asynchronous mechanisms, multiclock, Signal language

CITATION

Abdoulaye Gamatié, Thierry Gautier, "The Signal Synchronous Multiclock Approach to the Design of Distributed Embedded Systems",

*IEEE Transactions on Parallel & Distributed Systems*, vol.21, no. 5, pp. 641-657, May 2010, doi:10.1109/TPDS.2009.125REFERENCES

- [1] Airlines Electronic Eng. Committee (AEEC), "ARINC 629: IMA Multi-Transmitter Databus Parts 1-4," 1990.
- [2] Airlines Electronic Eng. Committee (AEEC), "ARINC 659: Backplane Data Bus," Dec. 1993.
- [3] Airlines Electronic Eng. Committee (AEEC), "ARINC Specification 653: Avionics Application Software Standard Interface," Jan. 1997.
- [4] Airlines Electronics Eng. Committee (AEEC), "ARINC 664: Aircraft Data Network, Part 7: Avionics Full-Duplex Switched Ethernet (AFDX) Network," 2005.
- [5] P. Amagbegnon, L. Besnard, and P. Le Guernic, "Implementation of the Data-Flow Synchronous Language Signal,"
Proc. Conf. Programming Language Design and Implementation (PLDI '95), pp. 163-173, 1995.- [6] P. Aubry, "Mises en œuvre Distribuées de Programmes Synchrones," PhD thesis, Inst. de Formation Supérieur en Informatique et Comm., Univ. de Rennes I (in French), 1997.
- [7] N.C. Audsley and A.J. Wellings, "Analysing APEX Applications,"
Proc. Real Time Systems Symp. (RTSS '96), 1996.- [8] A. Benveniste, "Safety Critical Embedded Systems: The Sacres Approach,"
Proc. Symp. Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT '98), Sept. 1998.- [9] A. Benveniste, B. Caillaud, and P. Le Guernic, "From Synchrony to Asynchrony,"
Proc. Int'l Conf. Concurrency Theory (CONCUR '99), pp. 162-177, 1999.- [10] A. Benveniste, P. Caspi, S. Edwards, N. Halbwachs, P. Le Guernic, and R. de Simone, "The Synchronous Languages Twelve Years Later,"
Proc. IEEE, vol. 91, no. 1, pp. 64-83, Jan. 2003.- [11] A. Benveniste, P. Caspi, P. Le Guernic, H. Marchand, J.P. Talpin, and S. Tripakis, "A Protocol for Loosely Time-Triggered Architectures,"
Proc. Conf. Embedded Software (EMSOFT '02), J. Sifakis and A. Sangiovanni-Vincentelli, eds., 2002.- [12] G. Berry and E. Sentovich, "An Implementation of Constructive Synchronous Programs in POLIS,"
Formal Methods in System Design, vol. 17, no. 2, pp. 135-161, 2000.- [13] G. Berry and E. Sentovich, "Multiclock Esterel,"
Proc. 11th Conf. Correct Hardware Design and Verification Methods (CHARME '01), pp. 110-125, 2001.- [14] L. Besnard, T. Gautier, and P. Le Guernic,
Signal Reference Manual, www.irisa.fr/espressoPolychrony, 2007.- [15] L. Besnard, T. Gautier, and J.-P. Talpin, "Code Generation Strategies in the Polychrony Environment," Research Report RR-6894, Institut National de Recherche en Informatique et en Automatique, 2009.
- [16] P. Caspi, A. Curic, A. Maignan, C. Sofronis, S. Tripakis, and P. Niebert, "From Simulink to SCADE/Lustre to TTA: A Layered Approach for Distributed Embedded Applications,"
Proc. Conf. Languages, Compilers, and Tools for Embedded Systems (LCTES '03), pp. 153-162, 2003.- [17] D. Chapiro, "Globally Asynchronous Locally Synchronous Systems," PhD thesis, Stanford Univ., 1984.
- [18] B. Chéron, "Transformations Syntaxiques de Programmes Signal," PhD thesis, Université de Rennes I, Sept. 1991.
- [19] G. Coulouris, J. Dollimore, and T. Kindberg,
Distributed Systems: Concepts and Design, fourth ed. Addison-Wesley Longman Publishing Co., Inc., 2005.- [20] M.J. Fischer, N.A. Lynch, and M.S. Paterson, "Impossibility of Distributed Consensus with One Faulty Process,"
J. ACM, vol. 32, no. 2, pp. 374-382, 1985.- [21] A. Gamatié and T. Gautier, "The Signal Approach to the Design of System Architectures,"
Proc. IEEE Conf. Eng. of Computer-Based Systems (ECBS '03), Apr. 2003.- [22] A. Gamatié, T. Gautier, and P. Le Guernic, "Towards Static Analysis of Signal Programs Using Interval Techniques,"
Proc. Workshop Synchronous Languages, Applications, and Programming (SLAP '06), Mar. 2006.- [23] A. Gamatié, T. Gautier, P. Le Guernic, and J.-P. Talpin, "Polychronous Design of Embedded Real-Time Applications,"
ACM Trans. Software Eng. Methodology, vol. 16, no. 2, p. 9, 2007.- [24] M.K. Ganai and A. Gupta, "Efficient BMC for Multi-Clock Systems with Clocked Specifications,"
Proc. Conf. Asia South Pacific Design Automation, pp. 310-315, 2007.- [25] T. Gautier and P. Le Guernic, "Code Generation in the Sacres Project,"
Proc. Safety-Critical Systems Symp. (SSS '99), Feb. 1999.- [26] A. Girault, "Sur la Répartition de Programmes Synchrones," PhD thesis, Inst. Nat'l Polytechnique de Grenoble (in French), 1994.
- [27] A. Girault, "A Survey of Automatic Distribution Method for Synchronous Programs,"
Proc. Workshop Synchronous Languages, Applications and Programs (SLAP '05), F. Maraninchi, M. Pouzet, and V. Roy, eds., Apr. 2005.- [28] A. Girault and C. Ménier, "Automatic Production of Globally Asynchronous Locally Synchronous Systems,"
Proc. Workshop Embedded Software (EMSOFT '02), A. Sangiovanni-Vincentelli and J. Sifakis, eds., pp. 266-281, 2002.- [29] A. Girault, X. Nicollin, and M. Pouzet, "Automatic Rate Desynchronization of Embedded Reactive Programs,"
ACM Trans. Embedded Computing Systems, vol. 5, no. 3, pp. 687-717, Aug. 2006.- [30] T. Grandpierre, "Modélisation D'architectures Parallèles Hétérogènes Pour la Génération Automatique D'exécutifs Distribués Temps Réel Optimisés," PhD thesis, Univ. de Paris-Sud (in French), Nov. 2000.
- [31] T. Grandpierre and Y. Sorel, "From Algorithm and Architecture Specifications to Automatic Generation of Distributed Real-Time Executives: A Seamless Flow of Graphs Transformations,"
Proc. Conf. Formal Methods and Models for Codesign (MEMOCODE '03), June 2003.- [32] R. Gupta, S. Pande, K. Psarris, and V. Sarkar, "Compilation Techniques for Parallel Systems,"
Parallel Computing, vol. 25, nos. 13/14, pp. 1741-1783, 1999.- [33] O. Hainque, "Etude D'un Environnement D'exécution Temps-réel, Distribué et Tolérant Aux Pannes Pour le Modèle Synchrone," PhD thesis, École Nat'l Supérieure des Télécomm. (in French), 2000.
- [34] N. Halbwachs and S. Baghdadi, "Synchronous Modeling of Asynchronous Systems,"
Proc. Conf. Embedded Software (EMSOFT '02), Oct. 2002.- [35] N. Halbwachs and L. Mandel, "Simulation and Verification of Asynchronous Systems by Means of a Synchronous Model,"
Proc. Sixth Int'l Conf. Application of Concurrency to System Design (ACSD '06), June 2006.- [36] A. Kountouris and P. Le Guernic, "Profiling of Signal Programs and Its Application in the Timing Evaluation of Design Implementations,"
Proc. IEE Colloq. HW-SW Cosynthesis for Reconfigurable Systems, pp. 6/1-6/9, Feb. 1996.- [37] P. Le Guernic, J.-P. Talpin, and J.-C. Le Lann, "Polychrony for System Design,"
J. Circuits, Systems and Computers, vol. 12, no. 3, pp. 261-304, Apr. 2003.- [38] N. Lopez, M. Simonot, and V. Donzeau-Gouge, "A Methodological Process for the Design of a Large System: Two Industrial Case-Studies,"
Electronic Notes in Theoretical Computer Science, vol. 66, no. 2, pp. 84-103, 2002.- [39] O. Maffeïs, "Ordonnancements de Graphes de Flots Synchrones: Application à la Mise en œuvre de Signal," PhD thesis, Inst. de Formation Supérieur en Informatique et Comm., Univ. de Rennes I (in French), Jan. 1993.
- [40] H. Marchand, P. Bournai, M. Le Borgne, and P. Le Guernic, "Synthesis of Discrete-Event Controllers Based on the Signal Environment,"
Discrete Event Dynamic System: Theory and Applications, vol. 10, no. 4, pp. 325-346, Oct. 2000.- [41] M.R. Mousavi, P. Le Guernic, J.-P. Talpin, S.K. Shukla, and T. Basten, "Modeling and Validating Globally Asynchronous Design in Synchronous Frameworks,"
Proc. Conf. Design, Automation, and Test in Europe (DATE), pp. 384-389, 2004.- [42] J. Muttersbach, T. Villiger, H. Kaeslin, N. Felber, and W. Fichtner, "Globally-Asynchronous Locally-Synchronous Architectures to Simplify the Design of On-Chip Systems,"
Proc. 12th IEEE Int'l ASIC/SOC Conf., 1999.- [43] I.M. Smarandache, T. Gautier, and P. Le Guernic, "Validation of Mixed Signal-Alpha Real-Time Systems through Affine Calculus on Clock Synchronisation Constraints,"
Proc. World Congress Formal Methods (2), pp. 1364-1383, 1999.- [44] A. Tanenbaum and M. van Steen,
Distributed Systems: Principles and Paradigms, second ed. Prentice Hall, 2007.- [45] P. Veríssimo, "On the Role of Time in Distributed Systems,"
Proc. Sixth IEEE Workshop Future Trends of Distributed Computer Systems (FTDCS '97), pp. 316-323, Oct. 1997. |