Abstract
This article presents a methodology for generating a real-time mission controller of a submarine robot. The initial description of the mission considers the granularity constraints associated with the actors defining the mission. This methodology incorporates a formal analysis of the different possibilities for success of the mission from the models of each component involved in the description of the mission. This article ends illustrating this methodology with the generation of a real robotic mission for marine biodiversity assessment.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
The events Rx_EV_RELEASE and Rx_EV_ERROROK are also only present in the example to simulate the release of the resource.
References
Edgar, G.J., Barrett, N.S., Morton, A.J.: Biases associated with the use of underwater visual census techniques to quantify the density and size-structure of fish populations. J. Exp. Mar. Biol. Ecol. 308(2), 269–290 (2004)
Adolf, F., Andert, F.: Onboard mission management for a VTOL UAV using sequence and supervisory control. Cutting Edge Robot. 2010, 301–317 (2010)
NATO and RTO, Coalition Battle Management Language (C-BML), Technical report (2012)
Meduna, A.: Formal Languages and Computation: Models and Their Applications. CRC Press, Boca Raton (2014)
Fernández-Perdomo, E., Cabrera-Gómez, J., Domínguez-Brito, A.C., Hernández-Sosa, D.: Mission specification in underwater robotics. J. Phys. Agents 4(1), 25–34 (2010)
Berry, G., Gonthier, G.: The esterel synchronous programming language: design, semantics, implementation. Sci. Comput. Program. 19, 87–152 (1992)
Ingham, M., Ragno, R., Williams, B.C.: A reactive model-based programming language for robotic space explorers. In: Proceedings of ISAIRAS-01 (2001)
Marchand, H., Rutten, É., Le Borgne, M., Samaan, M.: Formal verification of programs specified with signal: application to a power transformer station controller. Sci. Comput. Program. 41(1), 85–104 (2001)
Marchand, H., Bournai, P., Le Borgne, M., Le Guernic, P.: Synthesis of discrete controllers based on the signal environment. In: Boel, R., Stremersch, G. (eds.) Discrete Event Systems. ECC, vol. 569, pp. 479–480. Springer, Boston (2000)
Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous data flow programming language LUSTRE. Proc. IEEE 79(9), 1305–1320 (1991)
Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8(3), 231–274 (1987)
Basu, A., Bensalem, S., Bozga, M., Combaz, J., Jaber, M., Thanh-Hung, N., Sifakis, J.: Rigorous component-based system design using the BIP framework. IEEE Softw. 28, 41–48 (2011)
Basu, A., Mounier, L., Poulhiès, M., Pulou, J., Sifakis, J.: Using BIP for modeling and verification of networked systems - a case study on TinyOS-based networks. In: Proceedings of the 6th IEEE International Symposium on Network Computing and Applications, NCA 2007, pp. 257–260 (2007)
Ropars, B., Lasbouygues, A., Lapierre, L., Andreu, D.: Thruster’s dead-zones compensation for the actuation system of an underwater vehicle. In: ECC: European Control Conference, Linz, Austria, July 2015
Jaiem, L., Lapierre, L., GodaryDejean, K., Crestani, D.: Toward performance guarantee for autonomous mobile robotic mission: an approach for hardware and software resources management. In: TAROS 2016, Sheffield, UK (2016)
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Inf. Comput. 98(2), 142–170 (1992)
Alur, R.: Timed Automata. University of Pennsylvania, Technical report (1998)
Berthomieu, B., Ribet, P.O., Vernadat, F.: The tool tina-construction of abstract state spaces for petri nets and time petri nets. Int. J. Prod. Res. 42(14), 2741–2756 (2004)
Acknowledgment
The authors graciously thank the CUFR, FEDER, NUMEV and Agglo Beziers Mediterranee for their support to this work.
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Louis, S., Godary-Dejean, K., Lapierre, L., Claverie, T., Villéger, S. (2017). Formal Method for Mission Controller Generation of a Mobile Robot. In: Gao, Y., Fallah, S., Jin, Y., Lekakou, C. (eds) Towards Autonomous Robotic Systems. TAROS 2017. Lecture Notes in Computer Science(), vol 10454. Springer, Cham. https://doi.org/10.1007/978-3-319-64107-2_48
Download citation
DOI: https://doi.org/10.1007/978-3-319-64107-2_48
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-64106-5
Online ISBN: 978-3-319-64107-2
eBook Packages: Computer ScienceComputer Science (R0)