Skip to main content

Towards Verification of Multicore Motor-Drive Controllers in Aerospace

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9338))

Abstract

It is a known fact that development of models on the design stage of a product, constitutes a highly important stage proving early evidence of error absence for the proposed artifact. Meanwhile, advances in the embedded systems domain push for rapid architecture product changes based on current state-of-the-art solutions. Multicore systems have exhibit enormous benefits due to parallelization of task execution, increasing availability of resources in multiple domains such as the automotive and telecommunication. Such a premise creates the need to invest into new verification methodologies that will re-assure the safe and efficient transition of new solutions like multicores, especially in the demanding aerospace world. In this paper we describe current challenges and trends on the development of safe and efficient methods for power controllers’ verification in multicore-based hardware platforms, such as motor-drive applications. We outline current industrial practices and describe common toolsets, workflows and techniques used in the aerospace domain. Then our discussion focus on formal verification techniques that could provide efficient solutions for verifying power control algorithms in aerospace applications. We conclude with remarks about an ongoing verification effort for power control of a multicore-based motor drive towards producing certification evidence.

This is a preview of subscription content, log in via an institution.

Buying options

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

References

  1. Bhatt D., Madl G., Oglesby D., Schloegel K.: Towards scalable verification of commercial avionics software. In: Proceedings of the AIAA Infotech@Aerospace Conference, April 2010

    Google Scholar 

  2. Dutertre, B., Stavridou, V.: A model of non-interference for integrating mixed-criticality software component. In: Weinstock, C., Rushby, J. (eds.) DCCA, vol. 112, pp. 301–316 (2008)

    Google Scholar 

  3. RTCA Inc., Document RTCA/DO-178B. Federal Aviation Administration, January 11, Advisory Circular 20–115B (1993)

    Google Scholar 

  4. Paulitsch, M., Ruess, H., Sorea, M.: Non-functional avionics requirements communications in computer and information. Sci. 17, 369–384 (2009)

    Google Scholar 

  5. Durrieu, G., Laurent, O., Seguin, C., Wiels, V.: Formal proof and test case generation for critical embedded systems using scade. In: Jacquart, R. (ed.) BIS. IFIP AICT, vol. 156, pp. 499–504. Springer, Cambridge (2004)

    Chapter  Google Scholar 

  6. Alur, R., Kanade, A., Ramesh, S., Shashidhar, K.: Symbolic analysis for improving simulation coverage of simulink/stateflow models. In: Proceedings of EMSOFT, pp. 89–98 (2008)

    Google Scholar 

  7. DO-178B, Software Considerations in Airborne Systems and Equipment Certification. Requirements and Technical Concepts for Aviation, (This document is known as EUROCAE ED-12B in Europe) Washington, DC, December 1992

    Google Scholar 

  8. Nowotsch, J., Paulitsch, M.: Leveraging multicore computing architectures in avionics. In: European Dependable Computing Conference, pp. 132–143 (2012)

    Google Scholar 

  9. Knapp, A., Merz, S.: Model checking and code generation for UML state machines and collaborations. In: Proceedings of 5th Workshop on Tools for System Design and Verification (FM-TOOLS 2002), Report 2002–11, p. 6 (2002)

    Google Scholar 

  10. Rushby J.: Formal methods and the certification of critical systems, Technical report SRI-CSL-93-7, 4551, Computer Science Laboratory, SRI International, Menlo Park, CA (1993)

    Google Scholar 

  11. Amjad, H.: Verification of AMBA using a combination of model checking and theorem proving, electronic notes in theoretical computer science. In: Proceedings of the 5th International Workshop on Automated Verification of Critical Systems (AVoCS 2005), vol. 145, pp. 45–61 (2006)

    Google Scholar 

  12. DOD-HDBK-763 Human Engineering Procedures Guide, 27 February 1987

    Google Scholar 

  13. EUROCAE: European Organisation for Civil Aviation Equipment. http://www.eurocae.org

  14. FAA: Federal Aviation Administration. http://www.faa.gov

  15. Hollzman, G.: The model checker SPIN. IEEE Trans. Soft. Eng. 23(5), 279–295 (1997)

    Article  Google Scholar 

  16. Roboam, X., Sareni, B., Andrade, A.D.: More electricity in the air: toward optimized electrical networks embedded in more-electrical aircraft. IEEE Ind. Electron. Mag. 6, 6–17 (2012)

    Article  Google Scholar 

  17. Roboam, X.: New trends and challenges of electrical networks embedded in “more electrical aircraft”. In: 2011 IEEE International Symposium on Industrial Electronics (ISIE), pp. 26–31 (2011)

    Google Scholar 

  18. Rosero, J.A., Ortega, J.A., Aldabas, E., Romeral, L.: Moving towards a more electric aircraft. IEEE Aerosp. Electron. Syst. Mag. 22, 3–9 (2007)

    Article  Google Scholar 

  19. Wenping, C., Mecrow, B.C., Atkinson, G.J., Bennett, J.W., Atkinson, D.J.: Overview of electric motor technologies used for more electric aircraft (MEA). IEEE Trans. Ind. Electron. 59, 3523–3531 (2012)

    Article  Google Scholar 

  20. Boldea, I.: Control issues in adjustable speed drives. IEEE Ind. Electron. Mag. 2, 32–50 (2008)

    Article  Google Scholar 

  21. Holmes, D.G., Lipo, T.A.: Pulse Width Modulation for Power Converters. Principles and Practice. Wiley-Interscience, New York (2003)

    Google Scholar 

  22. Xilinx Zynq-7000 All Programmable SoC ZC702 Evaluation Kit. http://www.xilinx.com/products/boards-and-kits/ek-z7-zc702-g.html

  23. Guidelines for Development of Civil Aircraft and Systems ARP4754A. http://www.sae.org/technical/standards/arp4754a

Download references

Acknowledgments

This work is supported by the \(EMC^2\) ARTEMIS project: Embedded Multi-Core systems for Mixed Criticality applications in dynamic and changeable real-time environments. UTRC is supported jointly by the European Commission and the Irish Development Agency (IDA), Project Number: 621429.

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Stylianos Basagiannis .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Basagiannis, S., Gonzalez-Espin, F. (2015). Towards Verification of Multicore Motor-Drive Controllers in Aerospace. In: Koornneef, F., van Gulijk, C. (eds) Computer Safety, Reliability, and Security. SAFECOMP 2014. Lecture Notes in Computer Science(), vol 9338. Springer, Cham. https://doi.org/10.1007/978-3-319-24249-1_17

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-24249-1_17

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-24248-4

  • Online ISBN: 978-3-319-24249-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics