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
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
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
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)
RTCA Inc., Document RTCA/DO-178B. Federal Aviation Administration, January 11, Advisory Circular 20–115B (1993)
Paulitsch, M., Ruess, H., Sorea, M.: Non-functional avionics requirements communications in computer and information. Sci. 17, 369–384 (2009)
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)
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)
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
Nowotsch, J., Paulitsch, M.: Leveraging multicore computing architectures in avionics. In: European Dependable Computing Conference, pp. 132–143 (2012)
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)
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)
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)
DOD-HDBK-763 Human Engineering Procedures Guide, 27 February 1987
EUROCAE: European Organisation for Civil Aviation Equipment. http://www.eurocae.org
FAA: Federal Aviation Administration. http://www.faa.gov
Hollzman, G.: The model checker SPIN. IEEE Trans. Soft. Eng. 23(5), 279–295 (1997)
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)
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)
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)
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)
Boldea, I.: Control issues in adjustable speed drives. IEEE Ind. Electron. Mag. 2, 32–50 (2008)
Holmes, D.G., Lipo, T.A.: Pulse Width Modulation for Power Converters. Principles and Practice. Wiley-Interscience, New York (2003)
Xilinx Zynq-7000 All Programmable SoC ZC702 Evaluation Kit. http://www.xilinx.com/products/boards-and-kits/ek-z7-zc702-g.html
Guidelines for Development of Civil Aircraft and Systems ARP4754A. http://www.sae.org/technical/standards/arp4754a
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
Corresponding author
Editor information
Editors and Affiliations
Rights 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)