Formale Eigenschaftsprüfung für nichtlineare dynamische analoge Schaltungen

• Antragsteller: Professor Dr.-Ing. Erich Barke
• Fachliche Zuordnung: Elektronische Halbleiter, Bauelemente und Schaltungen, Integrierte Systeme, Sensorik, Theoretische Elektrotechnik
• Förderung: Förderung von 2002 bis 2006
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 5396611

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.

• DFG-Verfahren: Sachbeihilfen