Exploring system architectures in AADL via Polychrony and SynDEx

Abstract

Architecture analysis & design language (AADL) has been increasingly adopted in the design of embedded systems, and corresponding scheduling and formal verification have been well studied. However, little work takes code distribution and architecture exploration into account, particularly considering clock constraints, for distributed multi-processor systems. In this paper, we present an overview of our approach to handle these concerns, together with the associated toolchain, AADL-Polychrony-SynDEx. First, in order to avoid semantic ambiguities of AADL, the polychronous/multiclock semantics of AADL, based on a polychronous model of computation, is considered. Clock synthesis is then carried out in Polychrony, which bridges the gap between the polychronous semantics and the synchronous semantics of SynDEx. The same timing semantics is always preserved in order to ensure the correctness of the transformations between different formalisms. Code distribution and corresponding scheduling is carried out on the obtained SynDEx model in the last step, which enables the exploration of architectures originally specified in AADL. Our contribution provides a fast yet efficient architecture exploration approach for the design of distributed real-time and embedded systems. An avionic case study is used here to illustrate our approach.

Keywords

Polychrony / Signal / AADL / SynDEx / architecture exploration / modeling / timing analysis / scheduling / distribution

References

[1] SAE(Society of Automotive Engineers) Aerospace. Aerospace Standard AS5506A: architecture analysis and design language (AADL). SAE AS5506A, 2009

[2] Feiler P, Gluch D. Model-based engineering with AADL. Addison Wesley Professional, September 2012

[3] Singhoff F, Legrand J, Nana L, Marcé L. Scheduling and memory requirements analysis with AADL. Ada Letters. 2005, 1−10

[4] Bozzano M, Cimatti A, Katoen J P, Nguyen V, Noll T, Roveri M. Safety, dependability, and performance analysis of extended AADL models. The Computer Journal, 2011, 54(5): 754−775

[5] Feiler P, Hansson J. Flow latency analysis with the architecture analysis and design language (AADL). Technical Report, CMU, 2007

[6] Chkouri M, Robert A, Bozga M,Sifakis J. Models in software engineering. Translating AADL into BIP-Application to the Verification of Real-Time Systems. Springer-Verlag, 2009

[7] Hugues J, Zalila B, Pautet L, Kordon F. From the Prototype to the final embedded system using the ocarina AADL tool suite. ACM Transactions in Embedded Computing Systems (TECS), 2008, 7(4): 42:1−42:25

[8] Yang Z, Hu K, Ma D, Pi L. Towards a formal semantics for AADL behavior annex. In: Proceedings of the 2009. Conference on Design, Automation and Test in Europe. 2009, 1166−1171

[9] Ma Y, Yu H, Gautier T, Le Guernic P, Talpin J P, Besnard L, Heitz M. Toward polychronous analysis and validation for timed software architectures in aadl. In: Proceedings of the 2013 Conference on Design, Automation and Test in Europe. 2013, 1173−1178

[10] Benveniste A, Caspi P, Edwards S, Halbwachs N, Le Guernic P, de Simone R. The synchronous languages twelve years later. Proceedings of the IEEE, 2003, 9(1): 64−83

[11] Le Guernic P, Talpin J P, Le LannJ C. Polychrony for system design. Journal for Circuits, Systems and Computers, 2002, 12: 261−304

[12] Talpin J P, Le Guernic P, Shukla S, Doucet F, Gupta R. Formal refinement checking in a system-level design methodology. Fundamenta Informaticae, 2004, 62(2): 243−273

[13] Sorel Y. Massively parallel computing systems with real time constraints: the “algorithm architecture adequation” methodology. In: Proceedings of the 1st International Conference on Massively Parallel Computing Systems. 1994, 44−53

[14] The polychrony toolset. http://www.irisa.fr/espresso/Polychrony/

[15] Gamatié A. Designing embedded systems with the SIGNAL programming language. Springer, 2010

[16] Sorel Y. SynDEx: system-level CAD software for optimizing distributed real-time embedded systems. ERCIM News, 2004, 59: 68−69

[17] Jahier E, Halbwachs N, Raymond P. Synchronous modeling and validation of priority inheritance schedulers. In: Fundamental Approaches to Software Engineering, Springer, 2009, 140−154

[18] Girault A. A survey of automatic distribution method for synchronous programs. In: Maraninchi F, Pouzet M, Roy V, eds, Proceedings of the 2005 International Workshop on Synchronous Languages, Applications and Programs, ENTCS. April 2005

[19] Cost-efficient methods and processes for safety relevant embedded systems (CESAR project).

[20] Besnard L, Gautier T, Le Guernic P, Talpin J P. Compilation of polychromous data flow equations. In: Shukla S, Talpin J P, eds, . Synthesis of Embedded Software: Frameworks and Methodologies for Correctness by Construction, Springer, 2010, 1−40

[21] An industry working group focusing on open source tools for the development of embedded Systems.

[22] Eclipse modeling framework project (EMF). http://www.eclipse.org/modeling/emf/

[23] OSATE V2 project.

[24] Abramsky S, Jung A. Domain theory. In: Abramsky S, Gabbay D, Maibaum T, eds, . Handbook of Logic in Computer Science, volume 3, 1−168. Oxford University Press, 1994

[25] Kahn G. The semantics of a simple language for parallel programming. Information Procesing, 1974, 471−475

[26] Plotkin G. A powerdomain construction. SIAM Journal on Computing, 1976, 5: 452−487

[27] Sorel Y. Syndex: system-level cad software for optimizing distributed real-time embedded systems. Journal ERCIM News, 2004, 59: 68−69

[28] The syndex software. http://www.syndex.org

[29] Grandpierre T, Sorel Y. From algorithm and architecture specification to automatic generation of distributed real-time executives: a seamless flow of graphs transformations. In: Proceedings of the 1st ACM/IEEE International Conference on Formal Methods andModels for Codesign (MEMOCODE’03). 2003, 123132

[30] Dennis J. First version of a dataflow procedure language. In: Lecture notes in computer science, volume 19, 362−376. Springer-Verlag, 1974

[31] Harel D, Pnueli A. On the development of reactive systems. In: Apt K, ed, Logics and Models of Concurrent Systems. Springer Verlag, New York, 1985

[32] Grandpierre T. Modèisation d’architectures parallèes hétérogènes pour la génération automatique d’exéutifs distribués temps réel optimisés. PhD thesis, Universitéde Paris Sud, Spéialité éectronique, 2000

[33] Liu C, Layland J. Scheduling algorithms for multiprogramming in a hard real-time environment. Journal of ACM, 1973, 14(2): 46−61

[34] Grandpierre T, Lavarenne C, Sorel Y. Optimized rapid prototyping for real-time embedded heterogeneous multiprocessors. In: Proceedings of the 7th International Workshop on Hardware/Software Co design, CODES’99. 1999, 74−78

[35] Kermia O, Sorel Y. A rapid heuristic for scheduling non-preemptive dependent periodic tasks onto multiprocessor. In: Proceedings of ISCA 20th International Conference on Parallel and Distributed Computing Systems, PDCS’07. September 2007, 1−6

[36] Ndoye F, Sorel Y. Safety critical multiprocessor real-time scheduling with exact preemption cost. In: Proceedings of the 8th International Conference on Systems, ICONS’13. January, 2013, 127−136

[37] Ma Y, Yu H, Gautier T, Talpin J P, Besnard L, Le Guernic P. System synthesis from AADL using polychrony. In: Proceedings of the 2011 Electronic System Level Synthesis Conference. 2011, 1−6

[38] SmarandacheI, Gautier T, Le GuernicP. Validation of mixed Signal-Alpha real-time systems through affine calculus on clock synchronization constraints. In: Proceedings of the 1999 World Congress on Formal Methods. 1999, 1364−1383

[39] Brandt J, Gemünde M,Schneider K, Shukla S, Talpin J PRepresentation of synchronous, asynchronous, and polychronous components by clocked guarded actions. Design Automation for Embedded Systems, 2012, 1−35

[40] Yu H, Talpin J P, Besnard L, Gautier T, Marchand H, Le Guernic P. Polychronous controller synthesis from MARTE CCSL timing specifications. In: Proceedings of the 9th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE’ 11). 2011, 21−30

[41] Pan Q, Gautier T, Besnard L, Sorel Y. Signal to SynDEx: translations between synchronous formalisms. 2003

[42] Pimentel A, Erbas C, Polstra S. A systematic approach to exploring embedded system architectures at multiple abstraction levels. IEEE Transactions on Computers, 2006, 55(2): 99−112

[43] Gries M. Methods for evaluating and covering the design space during early design development. Integration, the VLSI Journal, 2004, 38(2): 131−183

[44] Osek. http://www.osek-vdx.org/

[45] Ma Y. Compositional modeling of globally asynchronous locally synchronous (GALS) architectures in a polychronous model of compotation. PhD thesis, University of Rennes 1, 2010

[46] Yu H, Ma Y, Glouche Y, Talpin J P, Besnard L, Gautier T, Guernic L P, Toom A, Laurent O. System-level co-simulation of integrated avionics using polychrony. In: Proceedings of the 2011 ACM Symposium on Applied Computing (SAC’11). 2011, 354−359

[47] Sokolsky O, Lee I, Clarke D. Schedulability analysis of AADL models. In: Proceedings of the 20th International Conference on Parallel and Distributed Processing. 2006, 179

[48] Gui S, Luo L, Li Y, Wang L. Formal schedulability analysis and simulation for AADL. In: Proceedings of the 2008 International Conference on Embedded Software and Systems (ICESS). 2008, 429−435

[49] Berthomieu B, Bodeveix J P, Farail P, Filali M, Garavel H, Gaufillet P, Lang F, Vernadat F. Fiacre: an intermediate language for model verification in the topcased environment. In: Proceedings of the 2008 International Conference of Embedded Real Time Software. 2008

RIGHTS & PERMISSIONS

2013 Higher Education Press and Springer-Verlag Berlin Heidelberg