{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,15]],"date-time":"2026-02-15T08:51:26Z","timestamp":1771145486419,"version":"3.50.1"},"reference-count":61,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2019,3,7]],"date-time":"2019-03-07T00:00:00Z","timestamp":1551916800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2020,4]]},"DOI":"10.1007\/s10009-019-00513-7","type":"journal-article","created":{"date-parts":[[2019,3,7]],"date-time":"2019-03-07T14:34:05Z","timestamp":1551969245000},"page":"219-247","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":22,"title":["A formal approach to AADL model-based software engineering"],"prefix":"10.1007","volume":"22","author":[{"given":"Hana","family":"Mkaouar","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bechir","family":"Zalila","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J\u00e9r\u00f4me","family":"Hugues","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mohamed","family":"Jmaiel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,3,7]]},"reference":[{"key":"513_CR1","unstructured":"AS5506A: SAE Architecture Analysis and Design Language (AADL) Version 2.0 (2009)"},{"key":"513_CR2","unstructured":"AS5506\/2: SAE Architecture Analysis and Design Language (AADL) Annex Volume 2 (2011)"},{"key":"513_CR3","doi-asserted-by":"crossref","unstructured":"Abdoul, T., Champeau, J., Dhaussy, P., Pillain, P.Y., Roger, J.: AADL execution semantics transformation for formal verification. In: 13th IEEE International Conference on Engineering of Complex Computer Systems, pp. 263\u2013268. IEEE (2008)","DOI":"10.1109\/ICECCS.2008.24"},{"key":"513_CR4","doi-asserted-by":"publisher","first-page":"651","DOI":"10.1007\/978-3-642-24559-6_43","volume-title":"Formal Methods and Software Engineering","author":"K Bae","year":"2011","unstructured":"Bae, K., \u00d6lveczky, P.C., Al-Nayeem, A., Meseguer, J.: Synchronous AADL and its formal analysis in Real-Time Maude. In: Qin, S., Qiu, Z. (eds.) Formal Methods and Software Engineering, pp. 651\u2013667. Springer, Berlin (2011)"},{"key":"513_CR5","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/978-3-319-06410-9_7","volume-title":"FM 2014: Formal Methods","author":"K Bae","year":"2014","unstructured":"Bae, K., \u00d6lveczky, P.C., Meseguer, J.: Definition, semantics, and analysis of multirate synchronous AADL. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014: Formal Methods, pp. 94\u2013109. Springer, Cham (2014)"},{"key":"513_CR6","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/978-3-642-28872-2_4","volume-title":"Fundamental Approaches to Software Engineering","author":"K Bae","year":"2012","unstructured":"Bae, K., \u00d6lveczky, P.C., Meseguer, J., Al-Nayeem, A.: The SynchAADL2Maude tool. In: de Lara, J., Zisman, A. (eds.) Fundamental Approaches to Software Engineering, pp. 59\u201362. Springer, Berlin (2012)"},{"key":"513_CR7","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-642-01924-1_15","volume-title":"Reliable Software Technologies\u2014Ada-Europe 2009","author":"B Berthomieu","year":"2009","unstructured":"Berthomieu, B., Bodeveix, J.P., Chaudet, C., Dal Zilio, S., Filali, M., Vernadat, F.: Formal verification of AADL specifications in the TOPCASED environment. In: Kordon, F., Kermarrec, Y. (eds.) Reliable Software Technologies\u2014Ada-Europe 2009, pp. 207\u2013221. Springer, Berlin (2009)"},{"key":"513_CR8","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1016\/j.scico.2014.05.014","volume":"106","author":"L Besnard","year":"2015","unstructured":"Besnard, L., Bouakaz, A., Gautier, T., Le Guernic, P., Ma, Y., Talpin, J.P., Yu, H.: Timed behavioural modelling and affine scheduling of embedded software architectures in the AADL using Polychrony. Sci. Comput. Program. 106, 54\u201377 (2015)","journal-title":"Sci. Comput. Program."},{"key":"513_CR9","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1016\/j.scico.2015.03.003","volume":"106","author":"JP Bodeveix","year":"2015","unstructured":"Bodeveix, J.P., Filali, M., Garnacho, M., Spadotti, R., Yang, Z.: Towards a verified transformation from AADL to the formal component-based language FIACRE. Sci. Comput. Program. 106, 30\u201353 (2015). (Special Issue: Architecture-Driven Semantic Analysis of Embedded Systems)","journal-title":"Sci. Comput. Program."},{"key":"513_CR10","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-642-04468-7_15","volume-title":"Computer Safety, Reliability, and Security","author":"M Bozzano","year":"2009","unstructured":"Bozzano, M., Cimatti, A., Katoen, J.P., Nguyen, V.Y., Noll, T., Roveri, M.: The COMPASS approach: correctness, modelling and performability of aerospace systems. In: Buth, B., Rabe, G., Seyfarth, T. (eds.) Computer Safety, Reliability, and Security, pp. 173\u2013186. Springer, Berlin (2009)"},{"issue":"5","key":"513_CR11","doi-asserted-by":"publisher","first-page":"754","DOI":"10.1093\/comjnl\/bxq024","volume":"54","author":"M Bozzano","year":"2010","unstructured":"Bozzano, M., Cimatti, A., Katoen, J.P., Nguyen, V.Y., Noll, T., Roveri, M.: Safety, dependability and performance analysis of extended AADL models. Comput. J. 54(5), 754\u2013775 (2010)","journal-title":"Comput. J."},{"key":"513_CR12","doi-asserted-by":"publisher","first-page":"562","DOI":"10.1007\/978-3-642-14295-6_48","volume-title":"Computer Aided Verification","author":"M Bozzano","year":"2010","unstructured":"Bozzano, M., Cimatti, A., Katoen, J.P., Nguyen, V.Y., Noll, T., Roveri, M., Wimmer, R.: A model checker for AADL. In: Touili, T., Cook, B., Jackson, P. (eds.) Computer Aided Verification, pp. 562\u2013565. Springer, Berlin (2010)"},{"issue":"4","key":"513_CR13","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1145\/340396.340450","volume":"19","author":"A Burns","year":"1999","unstructured":"Burns, A.: The Ravenscar profile. ACM SIGAda Ada Lett. 19(4), 49\u201352 (1999)","journal-title":"ACM SIGAda Ada Lett."},{"key":"513_CR14","unstructured":"Champelovier, D., Clerc, X., Garavel, H., Guerte, Y., Lang, F., McKinty, C., Powazny, V., Serwe, W., Smeding, G.: Reference Manual of the LNT to LOTOS Translator. Technical report (2018)"},{"key":"513_CR15","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-642-01648-6_2","volume-title":"Models in Software Engineering","author":"MY Chkouri","year":"2009","unstructured":"Chkouri, M.Y., Robert, A., Bozga, M., Sifakis, J.: Translating AADL into BIP-application to the verification of real-time systems. In: Chaudron, M.R.V. (ed.) Models in Software Engineering, pp. 5\u201319. Springer, Berlin (2009)"},{"issue":"12","key":"513_CR16","doi-asserted-by":"publisher","first-page":"1104","DOI":"10.1016\/S0140-3664(99)00240-6","volume":"23","author":"JP Courtiat","year":"2000","unstructured":"Courtiat, J.P., Santos, C.A., Lohr, C., Outtaj, B.: Experience with RT-LOTOS, a temporal extension of the LOTOS formal description technique. Comput. Commun. 23(12), 1104\u20131123 (2000)","journal-title":"Comput. Commun."},{"key":"513_CR17","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-642-19811-3_9","volume-title":"Fundamental Approaches to Software Engineering","author":"P Crouzen","year":"2011","unstructured":"Crouzen, P., Lang, F.: Smart reduction. In: Giannakopoulou, D., Orejas, F. (eds.) Fundamental Approaches to Software Engineering, pp. 111\u2013126. Springer, Berlin (2011)"},{"key":"513_CR18","volume-title":"Model-Based Engineering with AADL: An Introduction to the SAE Architecture Analysis and Design Language. SEI Series in Software Engineering","author":"P Feiler","year":"2012","unstructured":"Feiler, P., Gluch, D.: Model-Based Engineering with AADL: An Introduction to the SAE Architecture Analysis and Design Language. SEI Series in Software Engineering. Pearson Education, London (2012)"},{"key":"513_CR19","unstructured":"Garavel, H., Hautbois, R.P.: An experiment with the LOTOS formal description technique on the flight warning computer of airbus 330\/340 aircrafts. In: Proceedings of the first AMAST International Workshop on Real-Time Systems. Citeseer (1993)"},{"key":"513_CR20","first-page":"377","volume-title":"Formal Techniques for Networked and Distributed Systems","author":"H Garavel","year":"2001","unstructured":"Garavel, H., Lang, F.: SVL: a scripting language for compositional verification. In: Kim, M., Chin, B., Kang, S., Lee, D. (eds.) Formal Techniques for Networked and Distributed Systems, pp. 377\u2013392. Springer, Boston (2001)"},{"issue":"4","key":"513_CR21","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/s00236-015-0226-1","volume":"52","author":"H Garavel","year":"2015","unstructured":"Garavel, H., Lang, F., Mateescu, R.: Compositional verification of asynchronous concurrent systems using CADP. Acta Inform. 52(4), 337\u2013392 (2015)","journal-title":"Acta Inform."},{"issue":"2","key":"513_CR22","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/s10009-012-0244-z","volume":"15","author":"H Garavel","year":"2013","unstructured":"Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: a toolbox for the construction and analysis of distributed processes. Int. J. Softw. Tools Technol. Transf. 15(2), 89\u2013107 (2013)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"513_CR23","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-68270-9_1","volume-title":"ModelEd, TestEd, TrustEd: Essays Dedicated to Ed Brinksma on the Occasion of His 60th Birthday","author":"H Garavel","year":"2017","unstructured":"Garavel, H., Lang, F., Serwe, W.: From LOTOS to LNT. In: Katoen, J.P., Langerak, R., Rensink, A. (eds.) ModelEd, TestEd, TrustEd: Essays Dedicated to Ed Brinksma on the Occasion of His 60th Birthday, pp. 3\u201326. Springer, Cham (2017)"},{"key":"513_CR24","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/j.tcs.2005.09.064","volume":"351","author":"H Garavel","year":"2006","unstructured":"Garavel, H., Serwe, W.: State space reduction for process algebra specifications. Theor. Comput. Sci. 351, 131\u2013145 (2006)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"513_CR25","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/j.tcs.2003.10.009","volume":"313","author":"D Geniet","year":"2004","unstructured":"Geniet, D., Dubernard, J.P.: Scheduling hard sporadic tasks with regular languages and generating functions. Theor. Comput. Sci. 313(1), 119\u2013132 (2004)","journal-title":"Theor. Comput. Sci."},{"key":"513_CR26","doi-asserted-by":"crossref","unstructured":"Gui, S., Luo, L., Li, Y., Wang, L.: Formal schedulability analysis and simulation for AADL. In: 2008 International Conference on Embedded Software and Systems, pp. 429\u2013435. IEEE (2008)","DOI":"10.1109\/ICESS.2008.63"},{"issue":"4","key":"513_CR27","first-page":"115","volume":"7","author":"ME Hamdane","year":"2013","unstructured":"Hamdane, M.E., Chaoui, A., Strecker, M.: From AADL to timed automaton-a verification approach. Int. J. Softw. Eng. Appl. 7(4), 115\u2013126 (2013)","journal-title":"Int. J. Softw. Eng. Appl."},{"key":"513_CR28","doi-asserted-by":"crossref","unstructured":"Hamid, I., Najm, E.: Real-time connectors for deterministic data-flow. In: 13th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA 2007), pp. 173\u2013182. IEEE (2007)","DOI":"10.1109\/RTCSA.2007.58"},{"key":"513_CR29","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-540-68624-8_4","volume-title":"Reliable Software Technologies\u2014Ada-Europe 2008","author":"I Hamid","year":"2008","unstructured":"Hamid, I., Najm, E.: Operational semantics of Ada Ravenscar. In: Kordon, F., Vardanega, T. (eds.) Reliable Software Technologies\u2014Ada-Europe 2008, pp. 44\u201358. Springer, Berlin (2008)"},{"key":"513_CR30","doi-asserted-by":"crossref","unstructured":"Hecht, M., Lam, A., Vogl, C.: A tool set for integrated software and hardware dependability analysis using the architecture analysis and design language (AADL) and error-model annex. In: 2011 16th IEEE International Conference on Engineering of Complex Computer Systems, pp. 361\u2013366 (2011)","DOI":"10.1109\/ICECCS.2011.44"},{"issue":"3","key":"513_CR31","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1016\/j.sysarc.2015.02.003","volume":"61","author":"K Hu","year":"2015","unstructured":"Hu, K., Zhang, T., Yang, Z., Tsai, W.T.: Exploring AADL verification tool through model transformation. J. Syst. Archit. 61(3), 141\u2013156 (2015)","journal-title":"J. Syst. Archit."},{"key":"513_CR32","doi-asserted-by":"crossref","unstructured":"Jahier, E., Halbwachs, N., Raymond, P., Nicollin, X., Lesens, D.: Virtual execution of AADL models via a translation into synchronous programs. In: Proceedings of the 7th ACM and IEEE International Conference on Embedded Software, pp. 134\u2013143. ACM, New York, NY, USA (2007)","DOI":"10.1145\/1289927.1289951"},{"key":"513_CR33","doi-asserted-by":"crossref","unstructured":"Johnsen, A., Lundqvist, K., Hanninen, K., Pettersson, P., Torelm, M.: AQAF: an architecture quality assurance framework for systems modeled in AADL. In: 2016 12th International ACM SIGSOFT Conference on Quality of Software Architectures (QoSA), pp. 31\u201340. IEEE (2016)","DOI":"10.1109\/QoSA.2016.9"},{"key":"513_CR34","doi-asserted-by":"crossref","unstructured":"Johnsen, A., Lundqvist, K., Pettersson, P., Jaradat, O.: Automated verification of AADL-specifications using UPPAAL. In: 2012 IEEE 14th International Symposium on High-Assurance Systems Engineering, pp. 130\u2013138. IEEE (2012)","DOI":"10.1109\/HASE.2012.22"},{"key":"513_CR35","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-642-01924-1_17","volume-title":"Reliable Software Technologies\u2014Ada-Europe 2009","author":"G Lasnier","year":"2009","unstructured":"Lasnier, G., Zalila, B., Pautet, L., Hugues, J.: Ocarina: an environment for AADL models analysis and automatic code generation for high integrity applications. In: Kordon, F., Kermarrec, Y. (eds.) Reliable Software Technologies\u2014Ada-Europe 2009, pp. 237\u2013250. Springer, Berlin (2009)"},{"issue":"3","key":"513_CR36","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/s001650050015","volume":"10","author":"L L\u00e9onard","year":"1998","unstructured":"L\u00e9onard, L., Leduc, G.: A formal definition of time in LOTOS. Form. Asp. Comput. 10(3), 248\u2013266 (1998)","journal-title":"Form. Asp. Comput."},{"issue":"1","key":"513_CR37","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1145\/321738.321743","volume":"20","author":"CL Liu","year":"1973","unstructured":"Liu, C.L., Layland, J.W.: Scheduling algorithms for multiprogramming in a hard-real-time environment. J. ACM 20(1), 46\u201361 (1973)","journal-title":"J. ACM"},{"issue":"1","key":"513_CR38","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1023\/A:1021701221847","volume":"24","author":"K Lundqvist","year":"2003","unstructured":"Lundqvist, K., Asplund, L.: A Ravenscar-compliant run-time kernel for safety-critical systems. Real Time Syst. 24(1), 29\u201354 (2003)","journal-title":"Real Time Syst."},{"issue":"6","key":"513_CR39","doi-asserted-by":"publisher","first-page":"869","DOI":"10.1109\/TSE.2012.74","volume":"39","author":"I Malavolta","year":"2013","unstructured":"Malavolta, I., Lago, P., Muccini, H., Pelliccione, P., Tang, A.: What industry needs from architectural languages: a survey. IEEE Trans. Softw. Eng. 39(6), 869\u2013891 (2013)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"3","key":"513_CR40","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1016\/S0167-6423(02)00094-1","volume":"46","author":"R Mateescu","year":"2003","unstructured":"Mateescu, R., Sighireanu, M.: Efficient on-the-fly model-checking for regular alternation-free mu-calculus. Sci. Comput. Program. 46(3), 255\u2013281 (2003). (Special issue on Formal Methods for Industrial Critical Systems)","journal-title":"Sci. Comput. Program."},{"key":"513_CR41","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-540-68237-0_12","volume-title":"FM 2008: Formal Methods","author":"R Mateescu","year":"2008","unstructured":"Mateescu, R., Thivolle, D.: A model checking language for concurrent value-passing systems. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008: Formal Methods, pp. 148\u2013164. Springer, Berlin (2008)"},{"key":"513_CR42","unstructured":"Mkaouar, H.: A formal approach for real-time systems engineering. Ph.D. thesis, University of Sfax, Tunisia (2019)"},{"key":"513_CR43","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-319-19584-1_10","volume-title":"Reliable Software Technologies\u2014Ada-Europe 2015","author":"H Mkaouar","year":"2015","unstructured":"Mkaouar, H., Zalila, B., Hugues, J., Jmaiel, M.: From AADL model to LNT specification. In: de la Puente, J.A., Vardanega, T. (eds.) Reliable Software Technologies\u2014Ada-Europe 2015, pp. 146\u2013161. Springer, Cham (2015)"},{"key":"513_CR44","doi-asserted-by":"crossref","unstructured":"Mkaouar, H., Zalila, B., Hugues, J., Jmaiel, M.: An Ocarina extension for AADL formal semantics generation. In: Proceedings of the 33rd Annual ACM Symposium on Applied Computing, pp. 1402\u20131409. ACM, New York, NY, USA (2018)","DOI":"10.1145\/3167132.3167282"},{"key":"513_CR45","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-3-540-68624-8_3","volume-title":"Reliable Software Technologies\u2014Ada-Europe 2008","author":"I Ober","year":"2008","unstructured":"Ober, I., Halbwachs, N.: On the timed automata-based verification of Ravenscar systems. In: Kordon, F., Vardanega, T. (eds.) Reliable Software Technologies\u2014Ada-Europe 2008, pp. 30\u201343. Springer, Berlin (2008)"},{"key":"513_CR46","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-642-13464-7_5","volume-title":"Formal Techniques for Distributed Systems","author":"PC \u00d6lveczky","year":"2010","unstructured":"\u00d6lveczky, P.C., Boronat, A., Meseguer, J.: Formal semantics and analysis of behavioral AADL models in Real-Time Maude. In: Hatcliff, J., Zucca, E. (eds.) Formal Techniques for Distributed Systems, pp. 47\u201362. Springer, Berlin (2010)"},{"key":"513_CR47","unstructured":"Renault, X.: Mise en \u0153uvre de notations standardis\u00e9es, formelles et semi-formelles dans un processus de d\u00e9veloppement de systemes embarqu\u00e9s temps-r\u00e9el r\u00e9partis. Ph.D. thesis, Universit\u00e9 Pierre et Marie Curie-Paris VI (2009)"},{"key":"513_CR48","doi-asserted-by":"crossref","unstructured":"Renault, X., Kordon, F., Hugues, J.: Adapting models to model checkers, a case study: analysing AADL using Time or Colored Petri Nets. In: 2009 IEEE\/IFIP International Symposium on Rapid System Prototyping, pp. 26\u201333. IEEE (2009)","DOI":"10.1109\/RSP.2009.30"},{"key":"513_CR49","doi-asserted-by":"crossref","unstructured":"Renault, X., Kordon, F., Hugues, J.: From AADL architectural models to Petri Nets: Checking model viability. In: 2009 IEEE International Symposium on Object\/Component\/Service-Oriented Real-Time Distributed Computing (ISORC), pp. 313\u2013320. IEEE (2009)","DOI":"10.1109\/ISORC.2009.11"},{"key":"513_CR50","doi-asserted-by":"crossref","unstructured":"Rolland, J.F., Bodeveix, J.P., Filali, M., Chemouil, D., Thomas, D.: Modes in asynchronous systems. In: 13th IEEE International Conference on Engineering of Complex Computer Systems (iceccs 2008), pp. 282\u2013287. IEEE (2008)","DOI":"10.1109\/ICECCS.2008.28"},{"key":"513_CR51","unstructured":"RTCA\/DO-333: Formal Methods Supplement to DO-178C and DO-278A (2011)"},{"key":"513_CR52","doi-asserted-by":"crossref","unstructured":"Rugina, A., Kanoun, K., Ka\u00c3\u0107niche, M.: The ADAPT tool: From AADL architectural models to stochastic Petri nets through model transformation, pp. 85\u201390 (2008)","DOI":"10.1109\/EDCC-7.2008.14"},{"key":"513_CR53","doi-asserted-by":"crossref","unstructured":"Singhoff, F., Legrand, J., Nana, L., Marc\u00e9, L.: Cheddar: a flexible real time scheduling framework. In: ACM SIGAda Ada Letters, vol. 24, pp. 1\u20138. ACM (2004)","DOI":"10.1145\/1046191.1032298"},{"key":"513_CR54","doi-asserted-by":"crossref","unstructured":"Sokolsky, O., Lee, I., Clarke, D.: Schedulability analysis of AADL models. In: Proceedings of the 20th International Conference on Parallel and Distributed Processing, pp. 179\u2013179. IEEE Computer Society, Washington, DC, USA (2006)","DOI":"10.1109\/IPDPS.2006.1639421"},{"key":"513_CR55","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/978-3-642-01924-1_16","volume-title":"Reliable Software Technologies\u2014Ada-Europe 2009","author":"O Sokolsky","year":"2009","unstructured":"Sokolsky, O., Lee, I., Clarke, D.: Process-algebraic interpretation of AADL models. In: Kordon, F., Kermarrec, Y. (eds.) Reliable Software Technologies\u2014Ada-Europe 2009, pp. 222\u2013236. Springer, Berlin (2009)"},{"issue":"3","key":"513_CR56","doi-asserted-by":"publisher","first-page":"1234","DOI":"10.1109\/TII.2013.2258165","volume":"9","author":"V Vyatkin","year":"2013","unstructured":"Vyatkin, V.: Software engineering in industrial automation: state-of-the-art review. IEEE Trans. Ind. Inform. 9(3), 1234\u20131249 (2013)","journal-title":"IEEE Trans. Ind. Inform."},{"key":"513_CR57","first-page":"42","volume-title":"From AADL to Timed Abstract State Machines: A Verified Model Transformation","author":"Z Yang","year":"2014","unstructured":"Yang, Z., Hu, K., Ma, D., Bodeveix, J.P., Pi, L., Talpin, J.P.: From AADL to Timed Abstract State Machines: A Verified Model Transformation, pp. 42\u201368. Elsevier, Amsterdam (2014)"},{"issue":"10","key":"513_CR58","doi-asserted-by":"publisher","first-page":"1157","DOI":"10.1016\/j.sysarc.2013.08.004","volume":"59","author":"H Yu","year":"2013","unstructured":"Yu, H., Ma, Y., Gautier, T., Besnard, L., Le Guernic, P., Talpin, J.P.: Polychronous modeling, analysis, verification and simulation for timed software architectures. J. Syst. Archit. 59(10), 1157\u20131170 (2013)","journal-title":"J. Syst. Archit."},{"issue":"5","key":"513_CR59","doi-asserted-by":"publisher","first-page":"627","DOI":"10.1007\/s11704-013-2307-z","volume":"7","author":"H Yu","year":"2013","unstructured":"Yu, H., Ma, Y., Gautier, T., Besnard, L., Talpin, J.P., Le Guernic, P., Sorel, Y.: Exploring system architectures in AADL via Polychrony and SynDEx. Front. Comput. Sci. 7(5), 627\u2013649 (2013)","journal-title":"Front. Comput. Sci."},{"key":"513_CR60","doi-asserted-by":"publisher","first-page":"27421","DOI":"10.1109\/ACCESS.2017.2770323","volume":"5","author":"F Zhang","year":"2017","unstructured":"Zhang, F., Zhao, Y., Ma, D., Niu, W.: Formal verification of behavioral AADL models by stateful timed CSP. IEEE Access 5, 27421\u201327438 (2017)","journal-title":"IEEE Access"},{"key":"513_CR61","unstructured":"Zhang, Y., Dong, Y., Zhang, Y., Zhou, W.: A study of the AADL mode based on timed automata. In: 2011 IEEE 2nd International Conference on Software Engineering and Service Science, pp. 224\u2013227. IEEE (2011)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-019-00513-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-019-00513-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-019-00513-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,25]],"date-time":"2020-03-25T23:05:02Z","timestamp":1585177502000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-019-00513-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,3,7]]},"references-count":61,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2020,4]]}},"alternative-id":["513"],"URL":"https:\/\/doi.org\/10.1007\/s10009-019-00513-7","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,3,7]]},"assertion":[{"value":"7 March 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}