{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:50:42Z","timestamp":1740099042760,"version":"3.37.3"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319747804"},{"type":"electronic","value":"9783319747811"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-74781-1_28","type":"book-chapter","created":{"date-parts":[[2018,2,1]],"date-time":"2018-02-01T10:22:24Z","timestamp":1517480544000},"page":"406-422","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["A Framework for Analyzing Adaptive Autonomous Aerial Vehicles"],"prefix":"10.1007","author":[{"given":"Ian A.","family":"Mason","sequence":"first","affiliation":[]},{"given":"Vivek","family":"Nigam","sequence":"additional","affiliation":[]},{"given":"Carolyn","family":"Talcott","sequence":"additional","affiliation":[]},{"given":"Alisson","family":"Brito","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,2,2]]},"reference":[{"key":"28_CR1","unstructured":"Arduplane, arducopter, ardurover. https:\/\/github.com\/ArduPilot\/ardupilot"},{"key":"28_CR2","unstructured":"Ascens: Autonomic service-component ensembles. http:\/\/www.ascens-ist.eu"},{"issue":"12","key":"28_CR3","doi-asserted-by":"crossref","first-page":"1235","DOI":"10.1016\/j.scico.2010.10.002","volume":"77","author":"K Bae","year":"2012","unstructured":"Bae, K., \u00d6lveczky, P.C., Feng, T.H., Lee, E.A., Tripakis, S.: Verifying hierarchical ptolemy II discrete-event models using real-time maude. Sci. Comput. Program. 77(12), 1235\u20131271 (2012)","journal-title":"Sci. Comput. Program."},{"key":"28_CR4","doi-asserted-by":"crossref","unstructured":"Barros, J., Brito, A., Oliveira, T., Nigam, V.: A framework for the analysis of UAV strategies using co-simulation. In: SBESC (2016)","DOI":"10.1109\/SBESC.2016.011"},{"issue":"2","key":"28_CR5","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/256303.256306","volume":"44","author":"S Bistarelli","year":"1997","unstructured":"Bistarelli, S., Montanari, U., Rossi, F.: Semiring-based constraint satisfaction and optimization. J. ACM 44(2), 201\u2013236 (1997)","journal-title":"J. ACM"},{"key":"28_CR6","unstructured":"Why BNSF railway is using drones to inspect thousands of miles of rail lines. http:\/\/fortune.com\/2015\/05\/29\/bnsf-drone-program\/"},{"key":"28_CR7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71999-1","volume-title":"All About Maude: A High-Performance Logical Framework","author":"M Clavel","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: All About Maude: A High-Performance Logical Framework. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71999-1"},{"key":"28_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/978-3-319-44802-2_5","volume-title":"Rewriting Logic and Its Applications","author":"YG Dantas","year":"2016","unstructured":"Dantas, Y.G., Lemos, M.O.O., Fonseca, I.E., Nigam, V.: Formal specification and verification of a selective defense for TDoS attacks. In: Lucanu, D. (ed.) WRLA 2016. LNCS, vol. 9942, pp. 82\u201397. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-44802-2_5"},{"key":"28_CR9","doi-asserted-by":"crossref","unstructured":"Dantas, Y.G., Nigam, V., Fonseca, I.E.: A selective defense for application layer DDos attacks. In: JISIC (2014)","DOI":"10.1109\/JISIC.2014.21"},{"key":"28_CR10","doi-asserted-by":"crossref","unstructured":"Das, J., Cross, G., Qu, A.M.C., Tokekar, P., Mulgaonkar, Y., Kumar, V.: Devices, systems, and methods for automated monitoring enabling precision agriculture. In: CASE (2015)","DOI":"10.1109\/CoASE.2015.7294123"},{"key":"28_CR11","unstructured":"Autonomous taxi drones. https:\/\/www.forbes.com\/sites\/parmyolson\/2017\/02\/14\/dubai-autonomous-taxi-drones-ehang\/#54543d934702"},{"key":"28_CR12","doi-asserted-by":"crossref","unstructured":"H\u00f6lzl, M., Rauschmayer, A., Wirsing, M.: Engineering of software-intensive systems. In: Software-Intensive Systems and New Computing Paradigms (2008)","DOI":"10.1007\/978-3-540-89437-7_1"},{"key":"28_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/978-3-642-24933-4_12","volume-title":"Formal Modeling: Actors, Open Systems, Biological Systems","author":"M H\u00f6lzl","year":"2011","unstructured":"H\u00f6lzl, M., Wirsing, M.: Towards a system model for ensembles. In: Agha, G., Danvy, O., Meseguer, J. (eds.) Formal Modeling: Actors, Open Systems, Biological Systems. LNCS, vol. 7000, pp. 241\u2013261. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24933-4_12"},{"key":"28_CR14","unstructured":"The JSBSim flight dynamics model. http:\/\/www.jsbsim.org"},{"key":"28_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-319-44878-7_14","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"M Kanovich","year":"2016","unstructured":"Kanovich, M., Ban Kirigin, T., Nigam, V., Scedrov, A., Talcott, C.: Timed multiset rewriting and the verification of time-sensitive distributed systems. In: Fr\u00e4nzle, M., Markey, N. (eds.) FORMATS 2016. LNCS, vol. 9884, pp. 228\u2013244. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-44878-7_14"},{"key":"28_CR16","unstructured":"Kernbach, S., Schmickl, T., Timmis, J.: Collective adaptive systems: challenges beyond evolvability. In: Fundamentals of Collective Adaptive Systems. European Commission (2009)"},{"key":"28_CR17","unstructured":"Networked cyber physical systems. http:\/\/ncps.csl.sri.com"},{"key":"28_CR18","doi-asserted-by":"crossref","unstructured":"Kim, M., Stehr, M.-O., Kim, J., Ha, S.: An application framework for loosely coupled networked cyber-physical systems. In: EUC (2010)","DOI":"10.1109\/EUC.2010.30"},{"key":"28_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/978-3-540-75454-1_19","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"M Kim","year":"2007","unstructured":"Kim, M., Stehr, M.-O., Talcott, C., Dutt, N., Venkatasubramanian, N.: Combining formal verification with observed system execution behavior to tune system parameters. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 257\u2013273. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-75454-1_19"},{"key":"28_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/978-3-540-72952-5_18","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"M Kim","year":"2007","unstructured":"Kim, M., Stehr, M.-O., Talcott, C., Dutt, N., Venkatasubramanian, N.: A probabilistic formal analysis approach to cross layer optimization in distributed embedded systems. In: Bonsangue, M.M., Johnsen, E.B. (eds.) FMOODS 2007. LNCS, vol. 4468, pp. 285\u2013300. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-72952-5_18"},{"key":"28_CR21","doi-asserted-by":"crossref","unstructured":"Kim, M., Stehr, M.-O., Talcott, C., Dutt, N., Venkatasubramanian, N.: XTune: a formal methodology for cross-layer tuning of mobile embedded systems. Trans. Embed. Comput. Syst. (2011)","DOI":"10.1145\/2362336.2362340"},{"key":"28_CR22","unstructured":"Knightscope. http:\/\/www.knightscope.com"},{"issue":"1\u20133","key":"28_CR23","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1016\/j.apal.2007.11.006","volume":"152","author":"R Lassaigne","year":"2008","unstructured":"Lassaigne, R., Peyronnet, S.: Probabilistic verification and approximation schemes. Ann. Pure Appl. Log. 152(1\u20133), 122\u2013131 (2008)","journal-title":"Ann. Pure Appl. Log."},{"key":"28_CR24","unstructured":"Liquid robotics. http:\/\/liquidr.com"},{"key":"28_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-319-34096-8_4","volume-title":"Formal Methods for the Quantitative Evaluation of Collective Adaptive Systems","author":"M Loreti","year":"2016","unstructured":"Loreti, M., Hillston, J.: Modelling and analysis of collective adaptive systems with CARMA and its tools. In: Bernardo, M., De Nicola, R., Hillston, J. (eds.) SFM 2016. LNCS, vol. 9700, pp. 83\u2013119. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-34096-8_4"},{"key":"28_CR26","doi-asserted-by":"crossref","unstructured":"Mason, I.A., Talcott, C.L.: IOP: the interoperability platform and IMaude: an interactive extension of maude. In: WRLA 2004 (2004)","DOI":"10.1016\/j.entcs.2004.06.016"},{"key":"28_CR27","unstructured":"MAVLink micro air vehicle marshalling\/communication library. https:\/\/github.com\/ArduPilot\/mavlink.git"},{"key":"28_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/978-3-319-45741-3_23","volume-title":"Computer Security \u2013 ESORICS 2016","author":"V Nigam","year":"2016","unstructured":"Nigam, V., Talcott, C., Aires Urquiza, A.: Towards the automated verification of cyber-physical security protocols: bounding the number of timed intruders. In: Askoxylakis, I., Ioannidis, S., Katsikas, S., Meadows, C. (eds.) ESORICS 2016. LNCS, vol. 9879, pp. 450\u2013470. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-45741-3_23"},{"key":"28_CR29","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: Abstraction and completeness for real-time maude. In: WRLA (2007)","DOI":"10.1016\/j.entcs.2007.06.005"},{"issue":"1\u20132","key":"28_CR30","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1007\/s10990-007-9001-5","volume":"20","author":"PC \u00d6lveczky","year":"2007","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: Semantics and pragmatics of real-time maude. High.-Order Symb. Comput. 20(1\u20132), 161\u2013196 (2007)","journal-title":"High.-Order Symb. Comput."},{"key":"28_CR31","unstructured":"Inventory robotics. http:\/\/www.pinc.com\/inventory-robotics-cycle-counting-drones"},{"key":"28_CR32","doi-asserted-by":"crossref","unstructured":"Sen, K., Viswanathan, M., Agha, G.A.: VESTA: a statistical model-checker and analyzer for probabilistic systems. In: QEST (2005)","DOI":"10.1109\/QEST.2005.42"},{"key":"28_CR33","unstructured":"SITL (2016). http:\/\/python.dronekit.io\/about\/index.html"},{"key":"28_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-34096-8_1","volume-title":"Formal Methods for the Quantitative Evaluation of Collective Adaptive Systems","author":"C Talcott","year":"2016","unstructured":"Talcott, C., Nigam, V., Arbab, F., Kapp\u00e9, T.: Formal specification and analysis of robust adaptive distributed cyber-physical systems. In: Bernardo, M., De Nicola, R., Hillston, J. (eds.) SFM 2016. LNCS, vol. 9700, pp. 1\u201335. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-34096-8_1"},{"key":"28_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/978-3-319-15545-6_18","volume-title":"Software, Services, and Systems","author":"C Talcott","year":"2015","unstructured":"Talcott, C., Arbab, F., Yadav, M.: Soft agents: exploring soft constraints to model robust adaptive distributed cyber-physical agent systems. In: De Nicola, R., Hennicker, R. (eds.) Software, Services, and Systems. LNCS, vol. 8950, pp. 273\u2013290. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-15545-6_18"},{"key":"28_CR36","unstructured":"Drone swarms: The buzz of the future. https:\/\/www.vlab.org\/events\/drone-swarms\/"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-74781-1_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T00:20:24Z","timestamp":1570666824000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-74781-1_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319747804","9783319747811"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-74781-1_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}