Skip to main content

2018 | OriginalPaper | Buchkapitel

Verification of CAN-BUS Communication on Robots Based on xMAS

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

With the development of robot systems, distributed control systems become more and more widespread, which leads to much more complex communication specifications and hardware structure designs. Since the communication structure has important influence on robot security and real-time property, we proposed using formal method to verify the repeater with xMAS and ACL2 in this paper. Giving out the data flow logic information can also keep the low level properties while avoiding state explosion. The formalization method and model logic can also be used in many areas.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

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!

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!

Literatur
1.
Zurück zum Zitat Kaufmann, M., Manolios, P., Moore, J.: Computer aided reasoning: ACL2 Case Studies. Kluwer Acdemic Pub, Dordrecht (2002) Kaufmann, M., Manolios, P., Moore, J.: Computer aided reasoning: ACL2 Case Studies. Kluwer Acdemic Pub, Dordrecht (2002)
2.
Zurück zum Zitat Ya, G., Xiaojuan, Li., Yong G.: Theorem Prover ACL2-based Verification of the node Communication in the robot operating system ROS. J. Chin. Comput. Syst. 35(9), 2126–2130 (2014) Ya, G., Xiaojuan, Li., Yong G.: Theorem Prover ACL2-based Verification of the node Communication in the robot operating system ROS. J. Chin. Comput. Syst. 35(9), 2126–2130 (2014)
3.
Zurück zum Zitat Li, Y., Li, X., Guan, Y.: xMAS-based Formal Verification of SpaceWire Credit Logic. Comput. Sci. 43(2), 113–117 (2016) Li, Y., Li, X., Guan, Y.: xMAS-based Formal Verification of SpaceWire Credit Logic. Comput. Sci. 43(2), 113–117 (2016)
4.
Zurück zum Zitat Chatterjee, S., Kishinevsky, M.: Automatic generation of inductive invariants from high-level microarchitectural models of communication fabrics[J]. Formal Methods Syst. Des. 40(2), 147–169 (2012)CrossRefMATH Chatterjee, S., Kishinevsky, M.: Automatic generation of inductive invariants from high-level microarchitectural models of communication fabrics[J]. Formal Methods Syst. Des. 40(2), 147–169 (2012)CrossRefMATH
5.
Zurück zum Zitat Verbeek, F.: Formal verification of on-chip communication fabrics. UB, Nijmegen (2013) Verbeek, F.: Formal verification of on-chip communication fabrics. UB, Nijmegen (2013)
6.
Zurück zum Zitat Chatterjee, S., Kishinevsky, M., Ogras, U.Y.: Quick formal modeling of communication fabrics to enable verification. High level design validation & test workshop IEEE international 29(3), 42–49 (2010) Chatterjee, S., Kishinevsky, M., Ogras, U.Y.: Quick formal modeling of communication fabrics to enable verification. High level design validation & test workshop IEEE international 29(3), 42–49 (2010)
7.
Zurück zum Zitat Gotmanov, A., Chatterjee, S., Kishinevsky, M.: Verifying deadlock-freedom of communication fabrics, verification, model checking, and abstract interpretation, pp. 214–231. Springer, Berlin Heidelberg (2011)CrossRefMATH Gotmanov, A., Chatterjee, S., Kishinevsky, M.: Verifying deadlock-freedom of communication fabrics, verification, model checking, and abstract interpretation, pp. 214–231. Springer, Berlin Heidelberg (2011)CrossRefMATH
8.
Zurück zum Zitat Verbeek, F., Schmaltz, J.: Hunting deadlocks efficiently in microarchitectural models of communication fabrics. In: Bjesse, P., Slobodová, A. (ed.) Proceedings of the 11th Conference on Formal Methods in Computer Aided Design (FMCAD 2011). pp. 223–231. [s.l.], IEEE/ACM, (2011) Verbeek, F., Schmaltz, J.: Hunting deadlocks efficiently in microarchitectural models of communication fabrics. In: Bjesse, P., Slobodová, A. (ed.) Proceedings of the 11th Conference on Formal Methods in Computer Aided Design (FMCAD 2011). pp. 223–231. [s.l.], IEEE/ACM, (2011)
9.
Zurück zum Zitat Joosten, S.J.C., Schmaltz, J.: Automatic extraction of micro-architectural models of communication fabrics from register transfer level designs, Design, Automation & Test in Europe Conference & Exhibition (DATE). IEEE 2015, 1413–1418 (2015) Joosten, S.J.C., Schmaltz, J.: Automatic extraction of micro-architectural models of communication fabrics from register transfer level designs, Design, Automation & Test in Europe Conference & Exhibition (DATE). IEEE 2015, 1413–1418 (2015)
10.
Zurück zum Zitat Joosten, S.S., Verbeek, F.F., Schmaltz, J.J.: WickedXmas : designing and verifying on-chip communication fabrics. S.l, S.n (2014) Joosten, S.S., Verbeek, F.F., Schmaltz, J.J.: WickedXmas : designing and verifying on-chip communication fabrics. S.l, S.n (2014)
11.
Zurück zum Zitat Borrione, D., Helmy, A., Pierre, L., et al.: A generic model for formally verifying NoC communication architectures: A Case Study, International Symposium on Networks-on-chip, pp. 127–136. IEEE Computer Society, US (2007) Borrione, D., Helmy, A., Pierre, L., et al.: A generic model for formally verifying NoC communication architectures: A Case Study, International Symposium on Networks-on-chip, pp. 127–136. IEEE Computer Society, US (2007)
12.
Zurück zum Zitat Gastel, B V., Schmaltz, J.: A formalisation of XMAS. Eprint Arxiv (2013) Gastel, B V., Schmaltz, J.: A formalisation of XMAS. Eprint Arxiv (2013)
Metadaten
Titel
Verification of CAN-BUS Communication on Robots Based on xMAS
verfasst von
Xiujuan Cao
Copyright-Jahr
2018
DOI
https://doi.org/10.1007/978-3-319-69096-4_86