Polychronous automata and their use for formal validation of AADL models

doi:10.1007/s11704-017-6134-5

Front. Comput. Sci.

2019, Vol. 13

Issue (4) : 677-697 https://doi.org/10.1007/s11704-017-6134-5

RESEARCH ARTICLE

Polychronous automata and their use for formal validation of AADL models

Thierry GAUTIER¹(

), Clément GUY¹, Alexandre HONORAT¹, Paul LE GUERNIC¹, Jean-Pierre TALPIN¹, Loïc BESNARD²

¹. Univ. Rennes, Inria, Rennes-Bretagne-Atlantique Research Centre, F-35000 Rennes, France
². Univ. Rennes, CNRS, IRISA, F-35000 Rennes, France

Download: PDF(843 KB)
Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks

Abstract

This paper investigates how state diagrams can be best represented in the polychronous model of computation (MoC) and proposes to use this model for code validation of behavior specifications in architecture analysis & design language (AADL). In this relational MoC, the basic objects are signals, which are related through dataflow equations. Signals are associated with logical clocks, which provide the capability to describe systems in which components obey multiple clock rates. We propose a model of finite-state automata, called polychronous automata, which is based on clock relationships. A specificity of this model is that an automaton is submitted to clock constraints, which allows one to specify a wide range of control-related configurations, being either reactive or restrictive with respect to their control environment. A semantic model is defined for these polychronous automata, which relies on boolean algebra of clocks. Based on a previously defined modeling method for AADL software architectures using the polychronous MoC, the proposed model is used as a formal model for the AADL behavior annex. This is illustrated with a case study involving an adaptive cruise control system.

Keywords architecture modeling formal semantics finitestate automaton polychronous model synchronous concurrency code generation AADL

Corresponding Author(s): Thierry GAUTIER

Just Accepted Date: 01 August 2017 Online First Date: 06 August 2018 Issue Date: 29 May 2019

Cite this article:

Thierry GAUTIER,Clément GUY,Alexandre HONORAT, et al. Polychronous automata and their use for formal validation of AADL models[J]. Front. Comput. Sci., 2019, 13(4): 677-697.

URL:

https://academic.hep.com.cn/fcs/EN/10.1007/s11704-017-6134-5
https://academic.hep.com.cn/fcs/EN/Y2019/V13/I4/677

1	PLe Guernic, J PTalpin, J CLe Lann. Polychrony for system design. Journal of Circuits, Systems and Computers, 2003, 12(3): 261–303 https://doi.org/10.1142/S0218126603000763
2	ABenveniste, PCaspi, SEdwards , N Halbwachs, PLe Guernic, Rde Simone. The synchronous languages twelve years later. Proceedings of the IEEE, 2003, 91(1): 64–83 https://doi.org/10.1109/JPROC.2002.805826
3	GBerry, G Gonthier. The ESTEREL synchronous programming language: design, semantics, implementation. Science of Computer Programming, 1992, 19(2): 87–152 https://doi.org/10.1016/0167-6423(92)90005-V
4	NHalbwachs, PCaspi, PRaymond, D Pilaud. The synchronous dataflow programming language LUSTRE. Proceedings of the IEEE, 1991, 79(9): 1305–1320 https://doi.org/10.1109/5.97300
5	PLe Guernic, T Gautier, MLe Borgne, CLe Maire. Programming realtime applications with Signal. Proceedings of the IEEE, 1991, 79(9): 1321–1336 https://doi.org/10.1109/5.97301
6	AGamatié. Designing Embedded Systems with the SIGNAL Programming Language. Springer Science & Business Media, 2009
7	HYu, YMa, YGlouche, J P Talpin, LBesnard, TGautier, P Le Guernic, AToom, OLaurent. System-level co-simulation of integrated avionics using Polychrony. In: Procecdings of the 2011 ACM Symposium on Applied Computing. 2011, 354–359 https://doi.org/10.1145/1982185.1982263
8	Aerospace Standard AS5506A: Architecture Analysis and Design Language (AADL). Google Scholar, 2009
9	HYu, YMa, TGautier, L Besnard, J PTalpin, PLe Guernic, YSorel . Exploring system architectures in AADL via Polychrony and SynDEx. Frontiers of Computer Science, 2013, 7(5): 627–649 https://doi.org/10.1007/s11704-013-2307-z
10	HYu, YMa, TGautier, L Besnard, PLe Guernic , J PTalpin. Polychronous modeling, analysis, verification and simulation for timed software architectures. Journal of Systems Architecture, 2013, 59(10): 1157–1170 https://doi.org/10.1016/j.sysarc.2013.08.004
11	GBerry. Scade: Synchronous Design and Validation of Embedded Control Software. Next Generation Design and Verification Methodologies for Distributed Embedded Control Systems. Springer, Dordrecht, 2007
12	STripakis, C Stergiou, CShaver, E ALee. A modular formal semantics for Ptolemy. Mathematical Structures in Computer Science, 2013, 23: 834–881 https://doi.org/10.1017/S0960129512000278
13	E ALee, S Tripakis. Modal models in Ptolemy. In: Proceedings of the 3rd International Workshop on Equation-Based Object-Oriented Modeling Languages and Tools (EOOLT 2010). 2010, 1–11
14	GHamon, JRushby. An operational semantics for Stateflow. In: Proceedings of International Conference on Fundamental Approaches to Software Engineering. 2004, 229–243 https://doi.org/10.1007/978-3-540-24721-0_17
15	FMaraninchi, Y Rémond. Mode-automata: a new domain-specific construct for the development of safe critical systems. Science of Computer Programming, 2003, 46(3): 219–254 https://doi.org/10.1016/S0167-6423(02)00093-X
16	J LColaço, B Pagano, MPouzet. A conservative extension of synchronous data-flow with state machines. In: Proceedings of the 5th ACM International Conference on Embedded Software. 2005, 173–182 https://doi.org/10.1145/1086228.1086261
17	DHarel. Statecharts: a visual formalism for complex systems. Science of Computer Programming, 1987, 8(3): 231–274 https://doi.org/10.1016/0167-6423(87)90035-9
18	YWang, J PTalpin, ABenveniste, PLe Guernic. A semantics of UML state-machines using synchronous pre-order transition systems. In: Proceedings of the 3rd IEEE International Symposium on Object- Oriented Real-Time Distributed Computing. 2000, 96–103
19	CAndré. Semantics of SyncCharts. Technical Report ISRN I3S/RR– 2003–24–FR, I3S Laboratory, Sophia-Antipolis, France, 2003
20	Rvon Hanxleden, B Duderstadt, CMotika, SSmyth, M Mendler, JAguado, SMercer, O O’Brien. SCCharts: proceedings of sequentially constructive statecharts for safety-critical applications. In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 2014
21	R VHanxleden, M Mendler, JAguado, BDuderstadt, I Fuhrmann, CMotika, SMercer, O O’Brien. Sequentially constructive concurrency—a conservative extension of the synchronous model of computation. ACM Transaction on Embedded Computing Systems (TECS), 2014, 13(4S): 144 https://doi.org/10.1145/2627350
22	IRadojevic, ZSalcic, PRoop. Design of distributed heterogeneous embedded systems in DDFCharts. IEEE Transactions on Parallel and Distributed Systems, 2011, 22(2): 296–308 https://doi.org/10.1109/TPDS.2010.69
23	J PTalpin, C Brunette, TGautier, AGamatié. Polychronous mode automata. In: Proceedings of the 6th ACM & IEEE International Conference on Embedded Software. 2006, 83–92 https://doi.org/10.1145/1176887.1176900
24	PRaymond, YRoux, EJahier. Lutin: a language for specifying and executing reactive scenarios. EURASIP Journal on Embedded Systems, 2008, 2008(1): 753821 https://doi.org/10.1155/2008/753821
25	FCadoret, EBorde, SGardoll, L Pautet. Design patterns for rule-based refinement of safety critical embedded systems models. In: Proceedings of the 19th International Conference on Engineering of Complex Computer Systems, 2012, 67–76
26	P CÖlveczky, A Boronat, JMeseguer. Formal semantics and analysis of behavioral AADL models in real-time maude. In: Proceedings of the 12th IFIP WG 6.1 International Conference and the 30th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Systems. 2010, 47–62 https://doi.org/10.1007/978-3-642-13464-7_5
27	ZYang, KHu, J PBodeveix, LPi, DMa, J PTalpin. Two formal semantics of a subset of the AADL. In: Proceedings of the 16th IEEE International Conference on Engineering of Complex Computer Systems. 2011, 344–349 https://doi.org/10.1109/ICECCS.2011.41
28	LBesnard, T Gautier, PLe Guernic, J P.TalpinCompilation of Polychronous Data Flow Equations. Synthesis of Embedded Software. Springer, Boston, 2010
29	LBesnard, T Gautier, PLe Guernic. SIGNAL V4-INRIA version: reference manual. Access Through the ESPRESSO Website, 2010
30	SAbramsky, AJung. Domain theory. Handbook of Logic in Computer Science, Oxford: Oxford University Press, 1994, 1–168
31	KGilles. The semantics of a simple language for parallel programming. Information Processing, 1974, 74: 471–475
32	G DPlotkin. A powerdomain construction. SIAM Journal on Computing, 1976, 5(3): 452–487 https://doi.org/10.1137/0205035
33	NHalbwachs, P Raymond, CRatel. Generating efficient code from data-flow programs. In: Proceedings of the 3rd International Symposium on Programming Language Implementation and Logic Programming. 1991, 207–218 https://doi.org/10.1007/3-540-54444-5_100
34	HMarchand, P Bournai, MLe Borgne. Synthesis of discrete-event controllers based on the Signal environment. Discrete Event Dynamic System, 2000, 10(4): 325–346 https://doi.org/10.1023/A:1008311720696
35	YSorel. SynDEx: system-level CAD software for optimizing distributed real-time embedded systems. Journal ERCIM News, 2004, 59: 68–69
36	Wikipedia. Autonomous cruise control system—Wikipedia, The Free Encyclopedia, 2015
37	E ALee, D G Messerschmitt . Synchronous data flow. Proceedings of the IEEE, 1987, 75(9): 1235–1245 https://doi.org/10.1109/PROC.1987.13876
38	LBesnard, T Gautier, PLe Guernic, CGuy, J PTalpin, B RLarson, E Borde. Formal semantics of behavior specifications in the architecture analysis and design language standard. Cyber-Physical System Design from an Architecture Analysis Viewpoint. Springer, Singapore, 2017, 53–79
39	LBesnard, A Bouakaz, TGautier, PLe Guernic, YMa, J PTalpin, H Yu. Timed behavioural modelling and affine scheduling of embedded software architectures in the AADL using Polychrony. Science of Computer Programming, 2015, 106: 54–77 https://doi.org/10.1016/j.scico.2014.05.014
40	ABouakaz. Real-time scheduling of dataflow graphs. PhD Thesis, Université de Rennes 1, 2013
41	J PTalpin, T Gautier . Precise deadlock detection for polychronous dataflow specifications. In: Proceedings of Electronic System Level Synthesis Conference (ESLsyn). 2014, 1–6
42	LBesnard, EBorde, PDissaux, T Gautier, PLe Guernic, J PTalpin. Logically timed specifications in the AADL: a synchronous model of computation and communication (recommendations to the SAE committee on AADL). Technical Report, 2014

[1]

Download

[1]	Kai HU, Zhangbo DUAN, Jiye WANG, Lingchao GAO, Lihong SHANG. Template-based AADL automatic code generation[J]. Front. Comput. Sci., 2019, 13(4): 698-714.
[2]	Jing LIU, Tengfei LI, Zuohua DING, Yuqing QIAN, Haiying SUN, Jifeng HE. AADL+: a simulation-based methodology for cyber-physical systems[J]. Front. Comput. Sci., 2019, 13(3): 516-538.
[3]	Zhibin YANG,Jean-Paul BODEVEIX,Mamoun FILALI,Kai HU,Yongwang ZHAO,Dianfu MA. Towards a verified compiler prototype for the synchronous language SIGNAL[J]. Front. Comput. Sci., 2016, 10(1): 37-53.
[4]	Luxi CHEN,Linpeng HUANG,Chen LI,Tao ZAN. Integrating behavior analysis into architectural modeling[J]. Front. Comput. Sci., 2015, 9(1): 15-33.
[5]	Huafeng YU, Yue MA, Thierry GAUTIER, Lo?c BESNARD, Jean-Pierre TALPIN, Paul Le GUERNIC, Yves SOREL. Exploring system architectures in AADL via Polychrony and SynDEx[J]. Front Comput Sci, 2013, 7(5): 627-649.
[6]	Kai HU, Teng ZHANG, Zhibin YANG. Multi-threaded code generation from Signal program to OpenMP[J]. Front Comput Sci, 2013, 7(5): 617-626.
[7]	Zheng WANG, Geguang PU, Jiangwen LI, Yuxiang CHEN, Yongxin ZHAO, Mingsong CHEN, Bin GU, Mengfei YANG, Jifeng HE. A novel requirement analysis approach for periodic control systems[J]. Front Comput Sci, 2013, 7(2): 214-235.

Viewed

Full text

Abstract

Cited

Shared

Discussed