Model checking for nonlinear dynamic circuits

点击翻译按钮获取中文摘要

Der vorliegende Antrag umfasst eine Methode zum automatischen Eigenschaftsbeweis (Model-Checking) nichtlinearer dynamischer analoger Schaltungen. Die positiven Erfahrungen, die mit Eigenschaftsbeweisern bei digitalen Schaltungen gemacht wurden motivieren dazu, auch für analoge Schaltungen ein entsprechendes Werkzeug zu entwickeln. Die dazu notwendige Formalisierung des Entwurfsverifikationsprozesses wird zu einer erheblichen Reduzierung der Entwurfsfehler, der notwendigen Redesigns und damit zu einer erheblichen Produktivitätssteigerung im Analogdesign führen. Das zu entwickelnde Werkzeug führt eine speziell auf das nichtlineare dynamische analoge System angepasste Diskretisierung und Relationsberechnung im Zustandsraum durch. Das entstehende Modell wird bezüglich der Eigenschaften geprüft, die in der für diesen Zweck erweiterten Sprache CTL beschrieben werden.