Establishing Reachset Conformance for the Formal Analysis of Analog Circuits.

Research output: Chapter in book/report/conference proceedingConference contributionResearchpeer review

Authors

  • Niklas Kochdumper
  • Ahmad Tarraf
  • Malgorzata Rechmal
  • Markus Olbrich
  • Lars Hedrich
  • Matthias Althoff

Research Organisations

External Research Organisations

  • Technical University of Munich (TUM)
  • Goethe University Frankfurt
View graph of relations

Details

Original languageEnglish
Title of host publication2020 25th Asia and South Pacific Design Automation Conference (ASP-DAC)
Pages199-204
Number of pages6
ISBN (electronic)9781728141237
Publication statusPublished - 2020

Publication series

NameProceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC
Volume2020-January

Abstract

We present the first work on the automated generation of reachset conformant models for analog circuits. Our approach applies reachset conformant synthesis to add nondeterminism to piecewise-linear circuit models so that they enclose all recorded behaviors of the real system. To achieve this, we present a novel technique to compute the required nondeterminism for the piecewise-linear models. The effectiveness of our approach is demonstrated on a real analog circuit. Since the resulting models enclose all measurements, they can be used for formal verification.

ASJC Scopus subject areas

Cite this

Establishing Reachset Conformance for the Formal Analysis of Analog Circuits. / Kochdumper, Niklas; Tarraf, Ahmad; Rechmal, Malgorzata et al.
2020 25th Asia and South Pacific Design Automation Conference (ASP-DAC). 2020. p. 199-204 9045120 (Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC; Vol. 2020-January).

Research output: Chapter in book/report/conference proceedingConference contributionResearchpeer review

Kochdumper, N, Tarraf, A, Rechmal, M, Olbrich, M, Hedrich, L & Althoff, M 2020, Establishing Reachset Conformance for the Formal Analysis of Analog Circuits. in 2020 25th Asia and South Pacific Design Automation Conference (ASP-DAC)., 9045120, Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC, vol. 2020-January, pp. 199-204. https://doi.org/10.1109/ASP-DAC47756.2020.9045120
Kochdumper, N., Tarraf, A., Rechmal, M., Olbrich, M., Hedrich, L., & Althoff, M. (2020). Establishing Reachset Conformance for the Formal Analysis of Analog Circuits. In 2020 25th Asia and South Pacific Design Automation Conference (ASP-DAC) (pp. 199-204). Article 9045120 (Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC; Vol. 2020-January). https://doi.org/10.1109/ASP-DAC47756.2020.9045120
Kochdumper N, Tarraf A, Rechmal M, Olbrich M, Hedrich L, Althoff M. Establishing Reachset Conformance for the Formal Analysis of Analog Circuits. In 2020 25th Asia and South Pacific Design Automation Conference (ASP-DAC). 2020. p. 199-204. 9045120. (Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC). doi: 10.1109/ASP-DAC47756.2020.9045120
Kochdumper, Niklas ; Tarraf, Ahmad ; Rechmal, Malgorzata et al. / Establishing Reachset Conformance for the Formal Analysis of Analog Circuits. 2020 25th Asia and South Pacific Design Automation Conference (ASP-DAC). 2020. pp. 199-204 (Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC).
Download
@inproceedings{04000fc8461d46f882d4f952de30b44c,
title = "Establishing Reachset Conformance for the Formal Analysis of Analog Circuits.",
abstract = "We present the first work on the automated generation of reachset conformant models for analog circuits. Our approach applies reachset conformant synthesis to add nondeterminism to piecewise-linear circuit models so that they enclose all recorded behaviors of the real system. To achieve this, we present a novel technique to compute the required nondeterminism for the piecewise-linear models. The effectiveness of our approach is demonstrated on a real analog circuit. Since the resulting models enclose all measurements, they can be used for formal verification.",
author = "Niklas Kochdumper and Ahmad Tarraf and Malgorzata Rechmal and Markus Olbrich and Lars Hedrich and Matthias Althoff",
note = "Funding information: ACKNOWLEDGMENTS The authors gratefully acknowledge financial support by the German Research Foundation (DFG) project faveAC under grant AL 1185/5 1.",
year = "2020",
doi = "10.1109/ASP-DAC47756.2020.9045120",
language = "English",
isbn = "978-1-7281-4124-4",
series = "Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC",
pages = "199--204",
booktitle = "2020 25th Asia and South Pacific Design Automation Conference (ASP-DAC)",

}

Download

TY - GEN

T1 - Establishing Reachset Conformance for the Formal Analysis of Analog Circuits.

AU - Kochdumper, Niklas

AU - Tarraf, Ahmad

AU - Rechmal, Malgorzata

AU - Olbrich, Markus

AU - Hedrich, Lars

AU - Althoff, Matthias

N1 - Funding information: ACKNOWLEDGMENTS The authors gratefully acknowledge financial support by the German Research Foundation (DFG) project faveAC under grant AL 1185/5 1.

PY - 2020

Y1 - 2020

N2 - We present the first work on the automated generation of reachset conformant models for analog circuits. Our approach applies reachset conformant synthesis to add nondeterminism to piecewise-linear circuit models so that they enclose all recorded behaviors of the real system. To achieve this, we present a novel technique to compute the required nondeterminism for the piecewise-linear models. The effectiveness of our approach is demonstrated on a real analog circuit. Since the resulting models enclose all measurements, they can be used for formal verification.

AB - We present the first work on the automated generation of reachset conformant models for analog circuits. Our approach applies reachset conformant synthesis to add nondeterminism to piecewise-linear circuit models so that they enclose all recorded behaviors of the real system. To achieve this, we present a novel technique to compute the required nondeterminism for the piecewise-linear models. The effectiveness of our approach is demonstrated on a real analog circuit. Since the resulting models enclose all measurements, they can be used for formal verification.

UR - http://www.scopus.com/inward/record.url?scp=85083027861&partnerID=8YFLogxK

U2 - 10.1109/ASP-DAC47756.2020.9045120

DO - 10.1109/ASP-DAC47756.2020.9045120

M3 - Conference contribution

SN - 978-1-7281-4124-4

T3 - Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC

SP - 199

EP - 204

BT - 2020 25th Asia and South Pacific Design Automation Conference (ASP-DAC)

ER -