{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T05:17:43Z","timestamp":1742966263837,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642220449"},{"type":"electronic","value":"9783642220456"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-22045-6_8","type":"book-chapter","created":{"date-parts":[[2011,6,27]],"date-time":"2011-06-27T13:16:46Z","timestamp":1309180606000},"page":"116-132","source":"Crossref","is-referenced-by-count":7,"title":["A Formal Approach for Incremental Construction with an Application to Autonomous Robotic Systems"],"prefix":"10.1007","author":[{"given":"Saddek","family":"Bensalem","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lavindra","family":"de Silva","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andreas","family":"Griesmayer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Felix","family":"Ingrand","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Axel","family":"Legay","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rongjie","family":"Yan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/3-540-36575-3_13","volume-title":"Programming Languages and Systems","author":"K. Altisen","year":"2003","unstructured":"Altisen, K., Clodic, A., Maraninchi, F., Rutten, \u00c9.: Using controller-synthesis techniques to build property-enforcing layers. In: Degano, P. (ed.) ESOP 2003. LNCS, vol.\u00a02618, pp. 174\u2013188. Springer, Heidelberg (2003)"},{"key":"8_CR2","first-page":"269","volume":"9","author":"T. Amnell","year":"2002","unstructured":"Amnell, T., Fersman, E., Pettersson, P., Yi, W., Sun, H.: Code synthesis for timed automata. Nordic J. of Computing\u00a09, 269\u2013300 (2002)","journal-title":"Nordic J. of Computing"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-24756-2_1","volume-title":"Integrated Formal Methods","author":"T. Ball","year":"2004","unstructured":"Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and static driver verifier: Technology transfer of formal methods inside microsoft. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol.\u00a02999, pp. 1\u201320. Springer, Heidelberg (2004)"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time components in BIP. In: ICSEFM, pp. 3\u201312 (2006)","DOI":"10.1109\/SEFM.2006.27"},{"key":"8_CR5","unstructured":"Bensalem, S., Bozga, M., Legay, A., Nguyen, T.-H., Sifakis, J., Yan, R.: Incremental component-based construction and verification using invariants. In: FMCAD, pp. 257\u2013265 (2010)"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"614","DOI":"10.1007\/978-3-642-02658-4_45","volume-title":"Computer Aided Verification","author":"S. Bensalem","year":"2009","unstructured":"Bensalem, S., Bozga, M., Nguyen, T.-H., Sifakis, J.: D-finder: A tool for compositional deadlock detection and verification. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 614\u2013619. Springer, Heidelberg (2009)"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-540-88387-6_7","volume-title":"Automated Technology for Verification and Analysis","author":"S. Bensalem","year":"2008","unstructured":"Bensalem, S., Bozga, M., Sifakis, J., Nguyen, T.-H.: Compositional verification for component-based systems and application. In: Cha, S(S.), Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol.\u00a05311, pp. 64\u201379. Springer, Heidelberg (2008)"},{"key":"8_CR8","unstructured":"Bensalem, S., de Silva, L., Gallien, M., Ingrand, F., Yan, R.: \u201cRock solid\u201d software: A verifiable and correct by construction controller for rover and spacecraft functional layers. In: ISAIRAS, pp. 859\u2013866 (2010)"},{"issue":"1","key":"8_CR9","first-page":"1","volume":"16","author":"S. Bensalem","year":"2009","unstructured":"Bensalem, S., Gallien, M.: Toward a more dependable software architecture for autonomous robots. Special issue on Software Engineering for Robotics of the IEEE RAM\u00a016(1), 1\u201311 (2009)","journal-title":"Special issue on Software Engineering for Robotics of the IEEE RAM"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/978-3-642-20398-5_32","volume-title":"NASA Formal Methods","author":"S. Bensalem","year":"2011","unstructured":"Bensalem, S., Griesmayer, A., Legay, A., Nguyen, T.-H., Sifakis, J., Yan, R.: D-Finder 2: Towards Efficient Correctness of Incremental Design. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol.\u00a06617, pp. 453\u2013458. Springer, Heidelberg (2011)"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Bensalem, S., Legay, A., Nguyen, T.-H., Sifakis, J., Yan, R.: Incremental invariant generation for compositional design. In: TASE, pp. 157\u2013167 (2010)","DOI":"10.1109\/TASE.2010.23"},{"issue":"5-6","key":"8_CR12","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D. Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker BLAST: Applications to software engineering. STTT\u00a09(5-6), 505\u2013525 (2007)","journal-title":"STTT"},{"key":"8_CR13","unstructured":"BIP Framework, http:\/\/www-verimag.imag.fr\/Rigorous-Design-of-Component-Based.html"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Bonakdarpour, B., Bozga, M., Jaber, M., Quilbeuf, J., Sifakis, J.: From high-level component-based models to distributed implementations. In: EMSOFT, pp. 209\u2013218 (2010)","DOI":"10.1145\/1879021.1879049"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"Boussinot, F., de Simone, R.: The ESTEREL Language. Proceeding of the IEEE, 1293\u20131304 (1991)","DOI":"10.1109\/5.97299"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Bozga, M., Jaber, M., Sifakis, J.: Source-to-source architecture transformation for performance optimization in bip. In: SIES, pp. 152\u2013160 (2009)","DOI":"10.1109\/SIES.2009.5196211"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Bruyninckx, H.: Open robot control software: the orocos project. In: ICRA, Seoul, Korea, pp. 2523\u20132528 (2001)","DOI":"10.1109\/ROBOT.2001.933002"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Espiau, B., Kapellos, K., Jourdan, M.: Formal verification in robotics: Why and how. In: IFRR, The Seventh International Symposium of Robotics Research, Munich, pp. 201\u2013213. Cambridge Press (1995)","DOI":"10.1007\/978-1-4471-1021-7_26"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Fleury, S., Herrb, M., Chatila, R.: G en o M: A tool for the specification and the implementation of operating modules in a distributed robot architecture. In: IROS, pp. 842\u2013848 (1997)","DOI":"10.1109\/IROS.1997.655108"},{"key":"8_CR20","unstructured":"G en o M, http:\/\/www.openrobots.org\/wiki\/genom"},{"key":"8_CR21","unstructured":"Goldman, R.P., Musliner, D.J., Pelican, M.J.: Using model checking to plan hard real-time controllers. In: Proc. of AIPS Workshop on Model-Theoretic Approaches to Planning (2000)"},{"key":"8_CR22","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1145\/503272.503279","volume-title":"POPL","author":"T.A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL, pp. 58\u201370. ACM, New York (2002)"},{"issue":"7","key":"8_CR23","doi-asserted-by":"publisher","first-page":"559","DOI":"10.1002\/rob.20206","volume":"24","author":"F. Ingrand","year":"2007","unstructured":"Ingrand, F., Lacroix, S., Lemai, S., Py, F.: Decisional autonomy of planetary rovers. Journal of Field Robotics\u00a024(7), 559\u2013580 (2007)","journal-title":"Journal of Field Robotics"},{"issue":"4","key":"8_CR24","first-page":"82","volume":"14","author":"J. Jackson","year":"2007","unstructured":"Jackson, J.: Microsoft robotics studio: A technical introduction. IEEE RAM\u00a014(4), 82\u201387 (2007)","journal-title":"IEEE RAM"},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"Montemerlo, M., Roy, N., Thrun, S.: Perspectives on standardization in mobile robot programming: The carnegie mellon navigation (carmen) toolkit. In: Proc. IEEE\/RSJ Int. Conf. Intelligent Robots and Systems, Las Vegas, NV, pp. 2436\u20132441 (2003)","DOI":"10.1109\/IROS.2003.1249235"},{"key":"8_CR26","unstructured":"Nesnas, I.A., Wright, A., Bajracharya, M., Simmons, R., Estlin, T.: Claraty and challenges of developing interoperable robotic software. In: IROS, Las Vegas, NV (October 2003) invited paper"},{"key":"8_CR27","unstructured":"Quigley, M., Gerkey, B., Conley, K., Faust, J., Foote, T., Leibs, J., Berger, E., Wheeler, R., Ng, A.: Ros: an open-source robot operating system. In: International Conference on Robotics and Automation, Kobe, Japan (2009)"},{"key":"8_CR28","first-page":"29","volume-title":"ACSD","author":"L. Thiele","year":"2007","unstructured":"Thiele, L., Bacivarov, I., Haid, W., Huang, K.: Mapping applications to tiled multiprocessor embedded systems. In: ACSD, pp. 29\u201340. IEEE, Los Alamitos (2007)"},{"key":"8_CR29","doi-asserted-by":"crossref","unstructured":"Vaughan, R., Gerkey, B.: Reusable robot software and the player\/stage project. In: Software Engineering for Experimental Robotics, pp. 267\u2013289 (2007)","DOI":"10.1007\/978-3-540-68951-5_16"},{"key":"8_CR30","unstructured":"Williams, B.C., Ingham, M.D., Chung, S., Elliott, P., Hofbaur, M., Sullivan, G.T.: Model-Based Programming of Fault-Aware Systems. In: AI, pp. 61\u201375 winter (2003)"}],"container-title":["Lecture Notes in Computer Science","Software Composition"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22045-6_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,6]],"date-time":"2025-03-06T19:02:11Z","timestamp":1741287731000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22045-6_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642220449","9783642220456"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22045-6_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}