{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,7]],"date-time":"2025-07-07T04:05:56Z","timestamp":1751861156569,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642019234"},{"type":"electronic","value":"9783642019241"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-01924-1_15","type":"book-chapter","created":{"date-parts":[[2009,6,5]],"date-time":"2009-06-05T17:25:15Z","timestamp":1244222715000},"page":"207-221","source":"Crossref","is-referenced-by-count":42,"title":["Formal Verification of AADL Specifications in the Topcased Environment"],"prefix":"10.1007","author":[{"given":"Bernard","family":"Berthomieu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Paul","family":"Bodeveix","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christelle","family":"Chaudet","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Silvano","family":"Dal Zilio","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mamoun","family":"Filali","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fran\u00e7ois","family":"Vernadat","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"15_CR1","unstructured":"SAE Aerospace. Architecture Analysis & Design Language (AADL).AS-5506, SAE International (2004)"},{"key":"15_CR2","unstructured":"Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time systems in BIP. In: Proc. of SEFM \u2013 IEEE Software Engineering and Formal Methods (2006)"},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"Chkouri, M., Robert, A., Bozga, M., Sifakis, J.: Translating AADL into BIP \u2013 application to the verification of real-time systems. In: Proc. of MoDELS ACES-MB \u2013 Model Based Architecting and Construction of Embedded Systems (2008)","DOI":"10.1007\/978-3-642-01648-6_2"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Franca, R.B., Bodeveix, J.-P., Chemouil, D., Filali, M., Thomas, D., Rolland, J.-F.: The AADL behaviour annex, experiments and roadmap. In: Proc. of ICECCS \u2013 IEEE International Conference on Engineering of Complex Computer Systems (2007)","DOI":"10.1109\/ICECCS.2007.41"},{"key":"15_CR5","unstructured":"Muller, P.-A., Fleurey, F., Vojtisek, D., Drey, Z., Pollet, D., Fondement, F., Studer, P., J\u00e9z\u00e9uel, J.-M.: On executable meta-languages applied to model transformations. In: Proc. of MoDELS \u2013 Model Transformations In Practice (2005)"},{"key":"15_CR6","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: Proc. of EMSOFT \u2013 ACM & IEEE international conference on Embedded software (2007)","DOI":"10.1145\/1289927.1289951"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Jouault, F., Kurtev, I.: Transforming Models with ATL. In: Proc. of MoDELS \u2013 Model Transformations in Practice (2005)","DOI":"10.1007\/11663430_14"},{"key":"15_CR8","unstructured":"OAW, http:\/\/www.openarchitectureware.org\/"},{"key":"15_CR9","unstructured":"OCL, UML 2.0 Object Constraint Language"},{"issue":"9","key":"15_CR10","first-page":"1036","volume":"24","author":"P.M. Merlin","year":"1976","unstructured":"Merlin, P.M., Farber, D.J.: Recoverability of communication protocols: Implications of a theoretical study. IIEEE Transactions on Computers\u00a024(9), 1036\u20131043 (1976)","journal-title":"IIEEE Transactions on Computers"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"Berthomieu, B., Ribet, P.-O., Vernadat, F.: The tool TINA \u2013 Construction of Abstract State Spaces for Petri Nets and Time Petri Nets. International Journal of Production Research\u00a042(14) (2004)","DOI":"10.1080\/00207540412331312688"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Garavel, H., Lang, F., Mateescu, R., Serve, W.: CADP: A Toolbox for the Construction and Analysis of Distributed Processes. In: Proc. of CAV \u2013 Int. Conf. On Computer Aided Verification (2007)","DOI":"10.1007\/978-3-540-73368-3_18"},{"key":"15_CR13","unstructured":"Berthomieu, B., Bodeveix, J.P., Filali, M., Garavel, H., Lang, F., Peres, F., Saad, R., Stoecker, J., Vernadat, F.: The syntax and semantics of Fiacre.Research Report LAAS 07264 (2007)"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Pi, L., Bodeveix, J.-P., Filali, M.: Modeling AADL Data Communication with BIP (preprint, 2009)","DOI":"10.1007\/978-3-642-01924-1_14"},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-540-24756-2_8","volume-title":"Integrated Formal Methods","author":"S. Chaki","year":"2004","unstructured":"Chaki, S., Clarke, E.M., Ouaknine, J., Sharygina, N., Sinha, N.: State\/Event-based Software Model Checking. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol.\u00a02999, pp. 128\u2013147. Springer, Heidelberg (2004)"},{"key":"15_CR16","unstructured":"Rolland, J.-F., Bodeveix, J.-P., Chemouil, D., Filali, M., Thomas, D.: Towards a formal semantics for AADL execution model. In: Proc. of ERTS \u2013 European Congress on Embedded Real-Time Software (2008)"},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"Rolland, J.-F., Bodeveix, J.-P., Filali, M., Thomas, D., Chemouil, D.: Modes in asynchronous systems. In: Proc. of UML&AADL (2008)","DOI":"10.1109\/ICECCS.2008.28"},{"key":"15_CR18","unstructured":"Topcased: Toolkit in OPen-source for Critical Applications and SystEms Development, http:\/\/www.topcased.org"},{"key":"15_CR19","volume-title":"Handbook of Real-Time and Embedded Systems","author":"B. Berthomieu","year":"2007","unstructured":"Berthomieu, B., Vernadat, F.: State Space Abstractions for Time Petri Nets. In: Handbook of Real-Time and Embedded Systems. Chapman and Hall, Boca Raton (2007)"},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"Farines, J.-M., Berthomieu, B., Bodeveix, J.-P., Dissaux, P., Farail, P., Filali, M., Gaufillet, P., Hafidi, H., Lambert, J.-L., Michel, P., Vernadat, F.: The Cotre Project: Rigorous Software Development for Real Time Systems in Avionics. In: Proc. of FMICS \u2013 Formal Methods for Industrial Critical Systems. ENTCS, vol.\u00a080 (2003)","DOI":"10.1016\/S1571-0661(04)80819-3"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"Andr\u00e9, C., Mallet, F., de Simone, R.: Modeling of immediate vs. delayed data communications: from AADL to UML Marte. In: Forum on specification & Design Languages (2007)","DOI":"10.1007\/978-1-4020-8297-9_11"},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"Feiler, P.: Efficient embedded runtime systems through port communication optimization. In: Proc. of ICECCS \u2013 IEEE International Conference on Engineering of Complex Computer Systems (2008)","DOI":"10.1109\/ICECCS.2008.20"},{"key":"15_CR23","unstructured":"Vergnaud, T.: Mod\u00e9lisation des syst\u00e8mes temps-r\u00e9el r\u00e9partis embarqu\u00e9s pour la g\u00e9n\u00e9ration automatique d\u2019applications formellement v\u00e9rifi\u00e9es.PhD Thesis, \u00c9cole nationale sup\u00e9rieure des t\u00e9l\u00e9communications (2006)"},{"key":"15_CR24","unstructured":"The SEI AADL Team. An Extensible Open Source AADL Tool Environment (OSATE). Software Engineering Institute (2006)"}],"container-title":["Lecture Notes in Computer Science","Reliable Software Technologies \u2013 Ada-Europe 2009"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-01924-1_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,9]],"date-time":"2025-02-09T23:35:07Z","timestamp":1739144107000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-01924-1_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642019234","9783642019241"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-01924-1_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}