Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
DeepAlgebra - An Outline of a Program Kapitel lesen Erstes Kapitel lesen

2017 | OriginalPaper | Buchkapitel

Formalization of Transform Methods Using HOL Light

verfasst von : Adnan Rashid, Osman Hasan

Erschienen in: Intelligent Computer Mathematics

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

Transform methods, like Laplace and Fourier, are frequently used for analyzing the dynamical behaviour of engineering and physical systems, based on their transfer function, and frequency response or the solutions of their corresponding differential equations. In this paper, we present an ongoing project, which focuses on the higher-order logic formalization of transform methods using HOL Light theorem prover. In particular, we present the motivation of the formalization, which is followed by the related work. Next, we present the task completed so far while highlighting some of the challenges faced during the formalization. Finally, we present a roadmap to achieve our objectives, the current status and the future goals for this project.

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Vorheriges Kapitel Proof Mining with Dependent Types
Nächstes Kapitel Combining Refinement and Signal-Temporal Logic for Biological Systems
Fußnoten
Literatur
1.
Abad, G.: Power Electronics and Electric Drives for Traction Applications. Wiley, Hoboken (2016)CrossRef
2.
Akbarpour, B., Tahar, S.: A methodology for the formal verification of FFT algorithms in HOL. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 37–51. Springer, Heidelberg (2004). doi:10.​1007/​978-3-540-30494-4_​4 CrossRef
3.
Beerends, R.J., Morsche, H.G., Van den Berg, J.C., Van de Vrie, E.M.: Fourier and Laplace Transforms. Cambridge University Press, Cambridge (2003)CrossRefMATH
4.
Bogart, T.F.: Laplace Transforms and Control Systems Theory for Technology: Including Microprocessor-Based Control Systems. Wiley, New York (1982)
5.
Born, M., Wolf, E.: Principles of Optics: Electromagnetic Theory of Propagation, Interference and Diffraction of Light. Elsevier, Amsterdam (1980)MATH
6.
Boyce, W.E., DiPrima, R.C., Haines, C.W.: Elementary Differential Equations and Boundary Value Problems, vol. 9. Wiley, New York (1969)MATH
7.
Bracewell, R.N.: The Fourier Transform and its Applications. McGraw-Hill, New York (1978)MATH
8.
9.
Chapin, L.: Communication Systems (1978)
10.
11.
Chu, E.: Discrete and Continuous Fourier Transforms: Analysis, Applications and Fast Algorithms. CRC Press, Boca Raton (2008)MATH
12.
Davidson, D.B.: Computational Electromagnetics for RF and Microwave Engineering. Cambridge University Press, Cambridge (2005)CrossRef
13.
Devasahayam, S.R.: Signals and Systems in Biomedical Engineering: Signal Processing and Physiological Systems Modeling. Springer Science & Business Media, New York (2012)
14.
Dorf, R.C., Bishop, R.H.: Modern Control Systems. Prentice Hall, Eindhoven (1998)MATH
15.
Dougherty, G.: Digital Image Processing for Medical Applications. Cambridge University Press, Cambridge (2009)
16.
Du, K.L., Swamy, M.N.S.: Wireless Communication Systems: From RF Subsystems to 4G Enabling Technologies. Cambridge University Press, Cambridge (2010)CrossRef
17.
Fortmann, T.E., Hitz, K.L.: An introduction to linear control systems. CRC Press, Boca Raton (1977)MATH
18.
Gamboa, R.A.: Mechanically verifying the correctness of the fast fourier transform in ACL2. In: Rolim, J. (ed.) IPPS 1998. LNCS, vol. 1388, pp. 796–806. Springer, Heidelberg (1998). doi:10.​1007/​3-540-64359-1_​743 CrossRef
19.
Gamboa, R.A.: The correctness of the fast fourier transform: a structured proof in ACL2. Formal Methods Syst. Des. 20(1), 91–106 (2002)CrossRefMATH
20.
Gaskill, J.D.: Linear Systems, Fourier Transforms, and Optics, 1st edn. Wiley, New York (1978)
21.
Gaydecki, P.: Foundations of Digital Signal Processing: Theory, Algorithms and Hardware Design. Institution of Engineering and Technology, Stevenage (2004)CrossRefMATH
22.
Gorini, V., Frigerio, A.: Fundamental Aspects of Quantum Theory, vol. 144. Springer Science & Business Media, USA (2012)MATH
23.
24.
25.
26.
27.
Hasan, O., Tahar, S.: Formal Verification Methods. Encyclopedia of Information Science and Technology, pp. 7162–7170. IGI Global Pub., Hershey (2015)
28.
Hilbe, J.M.: Astrostatistical Challenges for the New Astronomy, vol. 1. Springer Science & Business Media, New York (2012)
29.
30.
Jin, J.M.: Theory and Computation of Electromagnetic Fields. Wiley, Hoboken (2011)
31.
Kriezis, E.E., Chrissoulidis, D., Papagiannakis, A.: Electromagnetics and Optics. World Scientific, Singapore (1992)CrossRef
32.
Madhow, U.: Introduction to Communication Systems. Cambridge University Press, Cambridge (2014)MATH
33.
McLachlan, N.W.: Laplace Transforms and their Applications to Differential Equations. Courier Corporation, Cedar City (2014)
34.
Nise, N.S.: Control Systems Engineering. Wiley, New York (2007)MATH
35.
Ogata, K., Yang, Y.: Modern Control Engineering. Prentice-Hall, Englewood Cliffs (1970)
36.
Oppenheim, A.V., Willsky, A.S., Hamid Nawab, S.: Signals and Systems. Prentice Hall Processing Series, 2nd edn. Prentice Hall Inc., Upper Saddle River (1996)
37.
Papoulis, A.: Signal Analysis, vol. 2. McGraw-Hill, New York (1977)MATH
38.
Pytel, A., Kiusalaas, J.: Engineering Mechanics: Dynamics. Nelson Education, Scarborough (2016)
39.
40.
Rashid, M.H.: Power Electronics: Circuits, Devices, and Applications. Pearson Education India, Delhi (2009)
41.
Siddique, U., Mahmoud, M.Y., Tahar, S.: On the formalization of Z-transform in HOL. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 483–498. Springer, Cham (2014). doi:10.​1007/​978-3-319-08970-6_​31
42.
Siebert, W.M.: Circuits, Signals, and Systems, vol. 2. MIT press, Cambridge (1986)
43.
44.
Stark, H.: Application of Optical Fourier Transforms. Elsevier, Burlington (2012)
45.
Taqdees, S.H., Hasan, O.: Formalization of laplace transform using the multivariable calculus theory of HOL-light. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 744–758. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-45221-5_​50 CrossRef
46.
47.
Thomas, R.E., Rosa, A.J., Toussaint, G.J.: The Analysis and Design of Linear Circuits, Binder Ready Version. Wiley, New York (2016)
48.
Ziemer, R., Tranter, W.H.: Principles of Communications: System Modulation and Noise. Wiley, Chichester (2006)
Metadaten
Titel
Formalization of Transform Methods Using HOL Light
verfasst von
Adnan Rashid
Osman Hasan
Copyright-Jahr
2017
Buch
Intelligent Computer Mathematics

Print ISBN: 978-3-319-62074-9

Electronic ISBN: 978-3-319-62075-6

Copyright-Jahr: 2017

DOI
https://doi.org/10.1007/978-3-319-62075-6_22

Premium Partner

    Bildnachweise