Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Generation of Search Behavior by a Modification of Q-MDP Value Method Read chapter Read first chapter

2016 | OriginalPaper | Chapter

Engineering Approaches and Methods to Verify Software in Autonomous Systems

Authors : G. Cicala, A. Khalili, G. Metta, L. Natale, S. Pathak, L. Pulina, A. Tacchella

Published in: Intelligent Autonomous Systems 13

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

We present three computer-augmented software engineering approaches to ensure dependability at different levels of control architectures in autonomous robots. For each approach, we outline the methodological framework, our current achievements, and open issues. Albeit our results are still preliminary, we believe that furthering research along these lines can provide cost-effective techniques to make autonomous robots safe and thus fit for commercial purposes.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Architecture Challenges for Intelligent Autonomous Machines
next chapter A Knowledge-Based Approach to Crack Detection in Thermographic Images
Footnotes
1
Experiments with ESBMC are performed on an Intel Core i7-3770 quad core at 3.40 GHz with 32 GB RAM, equipped with Ubuntu 12.04 LTS 64 bit.
 
2
Notice that most of the overall time is spent in network communication between the learner and system wrapper, in resetting the system, and other overhead tasks; less that 1 % of time was actually needed for the “learning algorithm”. All the identification experiments have been carried out on a Dell laptop with Core2Duo 2.53GHz CPU and 4GB of RAM on Ubuntu 12.04.
 
3
This behavior is the default because in the implementation of control loops it is preferable to reduce the communication latency at the cost of dropping (late) packets.
 
4
[0, 1] denotes a closed subinterval of \(\mathbb {R}\), i.e., every \(x \in \mathbb {R}\) such that \(0 \le x \le 1\).
 
5
Table T can handle (i) deterministic actions, i.e., a is such that \(\forall s \in S. |T(s,a)|=1\); (ii) nondeterministic actions, i.e.,a is such that for all \(s \in S\), both \(|T(s,a)| = k\) and \(n_i=1/k\) for all \(1 \le i \le k\); and (iii) probabilistic actions, i.e., arbitrary values of \(n_i\).
 
6
The radius \(\rho \) is not needed because we keep it fixed throughout learning and simulation. In a pure defense play, this choice does not hamper the robot’s ability to defend the goal area.
 
7
Simulation and learning are performed on an Intel Core i5-480M quad core at 2.67 GHz with 4GB RAM, equipped with Ubuntu 12.04 LTS 64 bit.
 
8
Verification and repair are performed on a Intel Core i3-2330M quad core at 2.20 GHz with similar RAM and OS. Verification of policies is carried out with state-of-the-art probabilistic model checkers, namely comics [29] (version 1.0), mrmc [30] (version 1.4.1), and prism [31] (version 4.0.3). All tools are run in their default configuration with the exception of comics, for which the option –concrete is selected instead of the default –abstract.
 
9
mrmc does not implement counterexample generation, and in prism this is still a beta-stage feature.
 
Literature
1.
M. Bajracharya, M. Maimone, and D. Helmick. Autonomy for mars rovers: Past, present, and future. Computer, 41(12):44–50, 2008.
2.
M. Beetz, U. Klank, I. Kresse, A. Maldonado, L. Mosenlechner, D. Pangercic, T. Ruhr, and M. Tenorth. Robotic roommates making pancakes. In Humanoid Robots (Humanoids), 2011 11th IEEE-RAS International Conference on, pages 529–536. IEEE, 2011.
3.
G. Pratt and J. Manzo. The DARPA Robotics Challenge [Competitions]. Robotics & Automation Magazine, IEEE, 20(2):10–12, 2013.
4.
C. Belta, A. Bicchi, M. Egerstedt, E. Frazzoli, E. Klavins, and G.J. Pappas. Symbolic planning and control of robot motion [grand challenges of robotics]. Robotics & Automation Magazine, IEEE, 14(1):61–70, 2007.
5.
R. Jhala and R. Majumdar. Software model checking. ACM Computing Surveys (CSUR), 41(4):21, 2009.
6.
S. Scherer, F. Lerda, and E. M. Clarke. Model checking of robotic control systems. In Proceedings of ISAIRAS 2005 Conference, pages 5–8, 2005.
7.
M. Shahbaz. Reverse Engineering Enhanced State Models of Black Box Software Components to Support Integration Testing. PhD thesis, Institut Polytechnique de Grenoble, Grenoble, France, 2008.
8.
9.
P. Fitzpatrick, G. Metta, and L. Natale. Towards long-lived robot genes. Robotics and Autonomous systems, 56(1):29–45, 2008.
10.
R.S. Sutton and A.G. Barto. Reinforcement Learning - An Introduction. MIT Press, 1998.
11.
J.A. Bagnell and S. Schaal. Special issue on Machine Learning in Robotics (Editorial). The International Journal of Robotics Research, 27(2):155–156, 2008.
12.
J.H. Gillula and C.J. Tomlin. Guaranteed Safe Online Learning via Reachability: tracking a ground target using a quadrotor. In ICRA, pages 2723–2730, 2012.
13.
M. Kwiatkowska, G. Norman, and D. Parker. Stochastic model checking. Formal methods for performance evaluation, pages 220–270, 2007.
14.
Rudolf Emil Kalman et al. Contributions to the theory of optimal control. Bol. Soc. Mat. Mexicana, 5(2):102–119, 1960.
15.
P. Lancaster and L. Rodman. Algebraic riccati equations. Oxford University Press, 1995.
16.
MATLAB. version 8.1.0 (R2013a). The MathWorks Inc., Natick, Massachusetts, 2013.
17.
L. Cordeiro, B. Fischer, and J. Marques-Silva. SMT-Based Bounded Model Checking for Embedded ANSI-C Software. Int.l Conf. on Automated Software Engineering, pages 137–148, 2009.
18.
N. Mohamed, J. Al-Jaroodi, and I. Jawhar. Middleware for robotics: A survey. In Robotics, Automation and Mechatronics, 2008 IEEE Conference on, pages 736–742. IEEE, 2008.
19.
G. Metta, L. Natale, F. Nori, G. Sandini, D. Vernon, L. Fadiga, C. von Hofsten, K. Rosander, M. Lopes, J. Santos-Victor, et al. The iCub Humanoid Robot: An Open-Systems Platform for Research in Cognitive Development. Neural networks: the official journal of the International Neural Network Society, 2010.
20.
M. Quigley, K. Conley, B. Gerkey, J. Faust, T. Foote, J. Leibs, R. Wheeler, and A. Y. Ng. ROS: an open-source Robot Operating System. In ICRA workshop on open source software, volume 3, 2009.
21.
D. Angluin. Learning regular sets from queries and counterexamples. Information and computation, 75(2):87–106, 1987.
22.
A. Gargantini. Conformance testing. Model-Based Testing of Reactive Systems, pages 87–111, 2005.
23.
O. Niese. An integrated approach to testing complex systems. PhD thesis, Universität Dortmund, Dortmund, Germany, December 2003.
24.
F. Aarts and F. Vaandrager. Learning I/O automata. CONCUR 2010-Concurrency Theory, pages 71–85, 2010.
25.
A. Khalili and A. Tacchella. Learning nondeterministic Mealy machines. Technical report, University of Genoa, 2013.
26.
D. C. Bentivegna, C. G. Atkeson A. Ude, and G. Cheng. Learning to Act from Observation and Practice. International Journal of Humanoid Robotics, 1(4), December 2004.
27.
G. Metta, L. Natale, S. Pathak, L. Pulina, and A. Tacchella. Safe and effective learning: A case study. In ICRA, pages 4809–4814, 2010.
28.
S. Pathak, L. Pulina, G. Metta, and A. Tacchella. Ensuring safety of policies learned by reinforcement: Reaching objects in the presence of obstacles with the iCub. In IROS, pages 170–175, 2013.
29.
E. Abrahám, N. Jansen, R. Wimmer, J. Katoen, and B. Becker. DTMC model checking by SCC reduction. In Quantitative Evaluation of Systems (QEST), 2010 Seventh International Conference on the, pages 37–46. IEEE, 2010.
30.
J.P. Katoen, I.S. Zapreev, E.M. Hahn, H. Hermanns, and D.N. Jansen. The ins and outs of the probabilistic model checker MRMC. Performance evaluation, 68(2):90–104, 2011.
31.
M. Kwiatkowska, G. Norman, and D. Parker. Prism: Probabilistic symbolic model checker. Computer Performance Evaluation: Modelling Techniques and Tools, pages 113–140, 2002.
32.
L. Pulina and A. Tacchella. An Abstraction-Refinement Approach to Verification of Artificial Neural Networks. In 22nd International Conference on Computer Aided Verification (CAV 2010), volume 6174 of Lecture Notes in Computer Science, pages 243–257. Springer, 2010.
33.
X.C. Ding, S.L. Smith, C. Belta, and D. Rus. MDP optimal control under temporal logic constraints. In Decision and Control and European Control Conference (CDC-ECC), 2011 50th IEEE Conference on, pages 532–538. IEEE, 2011.
Metadata
Title
Engineering Approaches and Methods to Verify Software in Autonomous Systems
Authors
G. Cicala
A. Khalili
G. Metta
L. Natale
S. Pathak
L. Pulina
A. Tacchella
Copyright Year
2016
Book
Intelligent Autonomous Systems 13

Print ISBN: 978-3-319-08337-7

Electronic ISBN: 978-3-319-08338-4

Copyright Year: 2016

DOI
https://doi.org/10.1007/978-3-319-08338-4_121

Premium Partner

    Image Credits