{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,25]],"date-time":"2026-02-25T17:14:05Z","timestamp":1772039645574,"version":"3.50.1"},"reference-count":24,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2009,11,11]],"date-time":"2009-11-11T00:00:00Z","timestamp":1257897600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2010,2]]},"DOI":"10.1007\/s10009-009-0131-4","type":"journal-article","created":{"date-parts":[[2009,11,10]],"date-time":"2009-11-10T03:27:24Z","timestamp":1257823644000},"page":"1-7","source":"Crossref","is-referenced-by-count":14,"title":["Toward a wider use of formal methods for aerospace systems design and verification"],"prefix":"10.1007","volume":"12","author":[{"given":"Yamine","family":"Ait Ameur","sequence":"first","affiliation":[]},{"given":"Fr\u00e9d\u00e9ric","family":"Boniol","sequence":"additional","affiliation":[]},{"given":"Virginie","family":"Wiels","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2009,11,11]]},"reference":[{"key":"131_CR1","unstructured":"A\u00eft Ameur, Y., Boniol, F., Wiels, V. (eds.): ISoLA 2007, Workshop On Leveraging Applications of Formal Methods, Verification and Validation, Poitiers-Futuroscope, France, December 12\u201314, 2007, Revue des Nouvelles Technologies de l\u2019Information, vol RNTI-SM-1, C\u00e9padu\u00e8s-\u00c9ditions (2007)"},{"key":"131_CR2","doi-asserted-by":"crossref","unstructured":"B\u00e9rard, B., Laroussinie, F., Petit, A., Schnoebelen, P.: Systems and Software Verification. Model-Checking Techniques and Tools. Springer (2001)","DOI":"10.1007\/978-3-662-04558-9"},{"key":"131_CR3","doi-asserted-by":"crossref","unstructured":"Bernard, R., Aubert, J.J., Bieber, P., Merlini, C., Metge, S.: Experiments in model-based safety analysis: flight controls. In: Workshop on Dependable Control of Discrete Systems, DCDS\u201907, IFAC, New York (2007)","DOI":"10.3182\/20070613-3-FR-4909.00010"},{"key":"131_CR4","unstructured":"Bieber, P., Blanquart, J., Durrieu, G., Lesens, D., Lucotte, J., Tardy, F., Turin, M., Seguin, C., Conquet, E.: Integration of formal fault analysis in ASSERT: case studies and lessons learnt. In: Embedded Real-Time Systems (ERTS). Toulouse, France (2008)"},{"key":"131_CR5","doi-asserted-by":"crossref","unstructured":"Bochot, T., Virelizier, P., Waeselynck, H., Wiels, V.: Model checking flight control systems: the airbus experience. In: ICSE Companion, pp 18\u201327 (2009)","DOI":"10.1109\/ICSE-COMPANION.2009.5070960"},{"key":"131_CR6","unstructured":"Boniol, F., Wiels, V., Ledinot, E.: Experiences using model checking to verify real time properties of a landing gear control system. In: Embedded Real-Time Systems (ERTS). Toulouse, France (2006)"},{"key":"131_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P.: Proving the absence of run-time errors in safety-critical avionics code. In: EMSOFT \u201907: Proceedings of the 7th ACM and IEEE International Conference on Embedded Software, pp 7\u20139. ACM, New York (2007). doi: 10.1145\/1289927.1289932 , http:\/\/dx.doi.org\/10.1145\/1289927.1289932","DOI":"10.1145\/1289927.1289932"},{"key":"131_CR8","unstructured":"Cousot, P.: The verification grand challenge and abstract interpretation. In: Meyer, B., Woodcock, J. (eds.) Verified Software: Theories Tools, Experiments, Lecture Notes in Computer Science, vol. 4171, pp. 227\u2013240. Springer, Berlin (2007)"},{"key":"131_CR9","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Basic concepts of abstract interpretation. In: Jacquart, R. (ed.) IFIP Congress Topical Sessions, pp. 359\u2013366. Kluwer (2004)","DOI":"10.1007\/978-1-4020-8157-6_27"},{"issue":"1","key":"131_CR10","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1109\/18.61109","volume":"37","author":"R.L. Cruz","year":"1991","unstructured":"Cruz R.L. (1991) A calculus for network delay, part i: network elements in isolation. IEEE Trans. Inf Theory 37(1): 114\u2013131","journal-title":"IEEE Trans. Inf Theory"},{"key":"131_CR11","unstructured":"Duprat, S., Souyris, J., Favre-F\u00e9lix, D.: Formal verification workbench for Airbus avionic software. In: Embedded Real-Time Systems (ERTS). Toulouse, France (2006)"},{"key":"131_CR12","doi-asserted-by":"crossref","unstructured":"Feiler, P.H., Gluch, D.P., Hudak, J.: The architecture & analysis design language (aadl): an introduction. Technical Report, Carnegie Mellon University, cMU\/SEI-2006-TN-011 (2006)","DOI":"10.21236\/ADA455842"},{"key":"131_CR13","doi-asserted-by":"crossref","unstructured":"Ferdinand, C., Heckmann, R.: aiT: worst case execution time prediction by static program analysis. In: IFIP Congress Topical Sessions 2004, pp. 377\u2013384 (2004)","DOI":"10.1007\/978-1-4020-8157-6_29"},{"key":"131_CR14","doi-asserted-by":"crossref","unstructured":"Ferdinand, C., Heckmann, R., Langenbach, M., Martin, F., Schmidt, M., Theiling, H., Thesing, S., Wilhelm, R.: Reliable and precise wcet determination for a real-life processor. In: EMSOFT \u201901: Proceedings of the First International Workshop on Embedded Software, pp. 469\u2013485. Springer, London (2001)","DOI":"10.1007\/3-540-45449-7_32"},{"issue":"2","key":"131_CR15","first-page":"95","volume":"221","author":"J. Gauthier","year":"2007","unstructured":"Gauthier J., Leduc X., Rauzy A. (2007) Assessment of large automatically generated fault trees by means of binary decision diagrams. J Risk Reliab 221(2): 95\u2013105","journal-title":"J Risk Reliab"},{"key":"131_CR16","doi-asserted-by":"crossref","unstructured":"Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous data-flow programming language LUSTRE. In: Proceedings of the IEEE, vol. 79(9), pp. 1305\u20131320 (1991)","DOI":"10.1109\/5.97300"},{"key":"131_CR17","doi-asserted-by":"crossref","unstructured":"Havelund, K., Skou, A., Larsen, K., Lund, K.: Formal modeling and analysis of an audio\/video protocol: an industrial case study using uppaal. In: Society, I.C. (ed.) Proceedings of the 18th IEEE Real-Time Systems Symposium (RTSS \u201997), pp. 2\u201313 (1997)","DOI":"10.1109\/REAL.1997.641264"},{"key":"131_CR18","unstructured":"ITU-T: Specification and description language. http:\/\/www.itu.int\/ITU-T\/studygroups\/com10\/languages\/Z.100_1199.pdf (1999)"},{"key":"131_CR19","doi-asserted-by":"crossref","unstructured":"Le Boudec, J.Y., Thiran, P.: Network Calculus: a theory of deterministic queuing systems for the Internet. Lecture Notes in Computer Science (LNCS) 2050. Springer (2001)","DOI":"10.1007\/3-540-45318-0"},{"key":"131_CR20","unstructured":"Moore, J.: The avionics handbook. In: Spitzer, C.R. (ed.) Advanced Distributed Architectures, pp. 33-1\u201333-12. CRC Press, Boca Raton (2001)"},{"key":"131_CR21","doi-asserted-by":"crossref","unstructured":"Randimbivololona, F., Souyris, J., Baudin, P., Pacalet, A., Raguideau, J., Schoen, D.: Applying formal proof techniques to avionics software: a pragmatic approach. p. 719 (1999). doi: 10.1007\/3-540-48118-4_45 , http:\/\/dx.doi.org\/10.1007\/3-540-48118-4_45","DOI":"10.1007\/3-540-48118-4_45"},{"key":"131_CR22","doi-asserted-by":"crossref","unstructured":"Souyris, J.: Industrial experience of abstract interpretation-based static analyzers. In: Jacquart, R. (ed.) IFIP Congress Topical Sessions, pp. 393\u2013400. Kluwer (2004). http:\/\/dblp.uni-trier.de\/db\/conf\/ifip\/ifip2004bis.html#Souyris04","DOI":"10.1007\/978-1-4020-8157-6_31"},{"key":"131_CR23","unstructured":"Souyris, J., Pavec, E.L., Himbert, G., Borios, G., J\u00e9gu, V. Heckmann, R. (2007) Computing the worst case execution time of an avionics program by abstract interpretation. In: Wilhelm, R. (ed.) 5th International Workshop on Worst-Case Execution Time (WCET) Analysis, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, Dagstuhl, Germany. http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2007\/810"},{"key":"131_CR24","volume-title":"Embedded Systems Handbook","author":"R. Zurawski","year":"2004","unstructured":"Zurawski R. (2004) Embedded Systems Handbook. CRC Press, Inc., Boca Raton, FL, USA"}],"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-009-0131-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-009-0131-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-009-0131-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T03:25:25Z","timestamp":1559100325000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-009-0131-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,11,11]]},"references-count":24,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2010,2]]}},"alternative-id":["131"],"URL":"https:\/\/doi.org\/10.1007\/s10009-009-0131-4","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,11,11]]}}}