AVACS: Automatic Verification and Analysis of Complex Systems

Am "SFB" sind neben IRA die Freiburger Lehrstühle für Künstliche Intelligenz, Softwaretechnik und Betriebssysteme sowie Forschergruppen der Universitäten Oldenburg, Saarbrücken, der Tschechischen Akademie der Wissenschaften in Prag und des Max-Planck-Instituts Saarbrücken beteiligt. Der Projektinhalt ist die Analyse und formale Verifikation komplexer Systeme. Das neue European Train Control Standard wird als Fallstudie zur Erprobung der entwickelten Methoden dienen. Die Wissenschaftler unseres Lehrstuhls werden insbesondere ihre Kompetenz im Bereich der Basistechnologien in den SFB einbringen. Die Genehmigung des SFB für zunächst acht Jahre (mit einer Verlängerungsmöglichkeit für bis zu weiteren vier Jahren) bietet vor allem jungen Forschern eine ausgezeichnete Möglichkeit, strategische Kompetenz in Verifikation von hybriden und Echtzeitsystemen aufzubauen. Wir sehen diesen Vertrauensbeweis seitens der DFG auch als eine Bestätigung unserer bisherigen Forschungsarbeit. Wie kaum ein anderes Gebiet muss sich die Informationstechnik der Herausforderung stellen, dass ihre Artefakte flexibel und mit vergleichsweise geringem Aufwand technisch machbar sind, bei gleichzeitiger Verdoppelung der technischen Leistungsfähigkeit ihrer Basiskomponenten alle 2 Jahre. Dies hat dazu geführt, dass komplexe Computer-basierte Systeme gebaut und flächendeckend eingesetzt werden, von deren korrektem Verhalten man sich zwar durch Testen zu überzeugen versucht, deren Funktionsweise man in ihrer Gesamtheit aber nicht überschaut. Was technisch gemacht wird übersteigt bei weitem das, was man analytisch versteht. Dieses ist nicht nur vom wissenschaftlichen Standpunkt unbefriedigend, es birgt auch ein hohes Risiko für Leib und Leben der Menschen, die diesen Systemen etwa in Haushalt, Auto, Bahn, Flugzeug, Kraftwerken, Industrieanlagen ausgesetzt sind, ganz abgesehen von den hohen ökonomischen Schäden, wenn es durch Fehler zur Zerstörung teurer Anlagen (Ariane V) kommt oder wenn Schadensersatzleistungen anderer Art notwendig werden. Der Transregio SFB AVACS widmet sich besonders den Systemen, die in sicherheitskritischen Bereichen eingesetzt werden und dort physikalische und technische Prozesse kontrollieren und steuern, wie etwa im Transportwesen bei Auto, Eisenbahn und Flugzeug. Die Komplexität der in diesen Anwendungen verwendeten Systeme hat mehrere Ursachen. Erstens, wenn physikalische Prozesse beobachtet und gesteuert werden, kommt es zur Interaktion von diskreten und kontinuierlichen Systemen, die mathematisch besonders komplex sind in ihrer Modellierung und Analyse. Steuerungsvorgänge müssen in vorgegebenen Zeitschranken ablaufen und Steuersignale so berechnen, dass der physikalische Prozess innerhalb des sicheren Bereiches bleibt. Eine zweite Ursache von Komplexität liegt in der Architektur dieser Systeme, wo eine große Anzahl von Komponenten miteinander vernetzt sind, miteinander kommunizieren und in kooperierender Weise die Funktion des Gesamtsystems bestimmen. Drittens sind solche Systeme mobil sowohl im physikalischen, wie im informationstechnischen Sinn. Mobile Computerprogamme und -systeme müssen in ständig wechselnden Umgebungen mit oftmals unbekannten Parametern zuverlässig und fehlertolerant funktionieren. Die für AVACS ins Auge gefassten Forschungsziele beruhen auf der Erkenntnis, dass Systemzuverlässigkeit nur dann flächendeckend entscheidend verbessert werden kann, wenn kritische Eigenschaften sowohl in der Spezifikation wie in der Realisierung mit automatisierten Techniken, also auf Knopfdruck, vom Softwareingenieur analysisert und überprüft werden können. Die kombinatorische Komplexität der Systemzustände ist zu hoch, die mathematischen und logischen Fähigkeiten der Ingenieure oft nicht ausreichend, und der zeitliche Aufwand zu groß, als dass nichtautomatische Methoden in großem Stil einsetzbar wären. Die Vision von AVACS ist es, dass nach Ablauf des Projektes die Zeitanforderungen auch an hochgradig vernetzte Systeme automatisch überprüft werden können, sowohl auf der Modellebene, wie auch für die auf der realen Hardware ablaufenden Maschinenprogramme. AVACS wird dabei in neue Größenordnungen von Systemkomplexität (Anzahl der Systemzustände, Nutzung moderner Hardwarekomponenten, algorithmisch optimierte Controller mit spezialisierten Datenstrukturen) vorstoßen. Bei den hybriden Systemen, wo diskrete Controller kontinuierliche wie diskontinuierliche physikalische Prozesse beobachten und steuern, wird AVACS wesentlich realistischere Systemmodelle als bisher betrachtet beherrschen helfen und gleichzeitig die Differenziertheit der an diesen Modellen automatisch überprüfbaren Aussagen über Stabilität und Sicherheit wesentlich verfeinern. Schließlich wird AVACS Methoden entwickeln, die eine neue Qualität der Analyse des globalen Zusammenspiels von Teilkomponenten komplexer Systeme herstellen. Hierzu zählen Techniken zur Untersuchung der Interaktion von Steuergeräten in Bezug auf die Realisierung einer Gesamtfunktionalität, zur Analyse von Kooperationsmechanismen bei sich dynamisch ändernden Kommunikationstopologien sowie zum formalen Nachweis globaler Verfügbarkeitsanforderungen. Durch die in AVACS geplanten Arbeiten werden Analysen dieser wichtigen Systemeigenschaften zum Teil erstmalig automatisiert und auch für solche Systeme einsetzbar werden, die sich bisher aufgrund ihrer Komplexität entsprechenden Untersuchungen entzogen. Zur Verwirklichung dieser Vision braucht es die Kombination von Methoden der mathematischen Semantik komplexer Systeme (Fundierung) mit algorithmisch-deduktiver Experise (Automatisierung), wie sie im AVACS-Konsortium gegeben ist.

Weitere Informationen: http://ira.informatik.uni-freiburg.de/src/projects_view.php?projectID=7

Projektbeginn: 2004
Projektende: (unbegrenzt)

Becker B

Albert-Ludwigs-Universität Freiburg
Rechnerarchitektur
Prof. Dr. Bernd Becker
Georges-Köhler-Allee 051
79110 Freiburg i. Br.

Telefon: 0761 203 8140
Fax: 0761 203 8142
http://ira.informatik.uni-freiburg.de

• Braitling
• Miller
• Scheibler
• Lewis
• Wimmer
• Kupferschmid
• Schubert
• Ábrahám
• Schmiedle
• Polian
• Eisinger
• Herbstritt
• Kalinnik
• Marin P
• Reimer S
• Gitina K

• Dominik Erb, Karsten Scheibler, Michael A. Kochte, Matthias Sauer, Hans-Joachim Wunderlich, Bernd Becker: Mixed 01X-RSL-Encoding for Fast and Accurate ATPG with Unknowns 21st Asia and South Pacific Design Automation Conference, 2016. : http://dx.doi.org/10.1109/ASPDAC.2016.7428101
• Karsten Scheibler, Dominik Erb, Bernd Becker: Accurate CEGAR-based ATPG in Presence of Unknown Values for Large Industrial Designs Conf. on Design, Automation and Test in Europe, 2016. : http://ieeexplore.ieee.org/xpl/articleDetails.jsp?reload=true&arnumber=7459448 (in Druck)
• Karsten Scheibler, Dominik Erb, Bernd Becker: Applying Tailored Formal Methods to X-ATPG GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, 2016. : http://dx.doi.org/10.6094/UNIFR/10647
• Dominik Erb, Karsten Scheibler, Matthias Sauer, Sudhakar M. Reddy, Bernd Becker: Multi-Cycle Circuit Parameter Independent ATPG for Interconnect Open Defects 33rd VLSI Test Symposium (VTS), 2015. : http://dx.doi.org/10.1109/VTS.2015.7116296 (in Druck)
• Karina Gitina, Ralf Wimmer, Sven Reimer, Matthias Sauer, Christoph Scholl, Bernd Becker: Solving DQBF Through Quantifier Elimination Conf. on Design, Automation and Test in Europe, 2015. (in Druck)
• Karsten Scheibler, Dominik Erb, Bernd Becker: Improving Test Pattern Generation in Presence of Unknown Values beyond Restricted Symbolic Logic to be published at European Test Symposium (ETS), 2015. : http://dx.doi.org/10.1109/ETS.2015.7138738 (in Druck)
• Karsten Scheibler, Leonore Winterer, Ralf Wimmer, Bernd Becker: Towards Verification of Artificial Neural Networks GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, 2015. : http://www.avacs.org/fileadmin/Publikationen/Open/scheibler.mbmv2015.pdf (in Druck)
• Dominik Erb, Karsten Scheibler, Matthias Sauer, Bernd Becker: Efficient SMT-based ATPG for Interconnect Open Defects Conf. on Design, Automation and Test in Europe, 2014. : http://dx.doi.org/10.7873/DATE.2014.138
• Dominik Erb, Karsten Scheibler, Matthias Sauer, Sudhakar M. Reddy, Bernd Becker: Circuit Parameter Independent Test Pattern Generationfor Interconnect Open Defects 23nd IEEE Asian Test Symposium (ATS), 2014. : http://dx.doi.org/10.1109/ATS.2014.34
• Dominik Erb, Karsten Scheibler, Michael Kochte, Matthias Sauer, Hans-Joachim Wunderlich, Bernd Becker: Test Pattern Generation in Presence of Unknown ValuesBased on Restricted Symbolic Logic Int'l Test Conf., 2014. : http://dx.doi.org/10.1109/TEST.2014.7035350
• Karsten Scheibler, Bernd Becker: Implication Graph Compression inside the SMT Solver iSAT3 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, 2014. : http://www.avacs.org/fileadmin/Publikationen/Open/scheibler.mbmv2014.pdf
• Karsten Scheibler, Bernd Becker: Using Interval Constraint Propagation for Pseudo-Boolean Constraint Solving Formal Methods in Computer-Aided Design, 2014. : http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD14/proceedings/32_scheibler.pdf
• Matthias Sauer, Sven Reimer, Sudhakar M. Reddy, Bernd Becker: Efficient SAT-based Circuit Initialization for Large Designs Int'l Conf. on VLSI Design, 2014. : http://dx.doi.org/10.1109/VLSID.2014.18
• Sven Reimer, Matthias Sauer, Paolo Marin, Bernd Becker: QBF with Soft Variables International Workshop on Automated Verification of Critical Systems (AVOCS), 2014. (in Druck)
• Sven Reimer, Matthias Sauer, Tobias Schubert, Bernd Becker: Using MaxBMC for Pareto-Optimal Circuit Initialization Conf. on Design, Automation and Test in Europe, 2014. : http://dx.doi.org/10.7873/DATE2014.161
• Sven Reimer, Matthias Sauer, Tobias Schubert, Bernd Becker: Incremental Encoding and Solving of Cardinality Constraints International Symposium on Automated Technology for Verification and Analysis, 2014; 8837: 297-313, Springer International Publishing (Hrsg). : http://dx.doi.org/10.1007/978-3-319-11936-6_22
• Karina Gitina, Sven Reimer, Matthias Sauer, Ralf Wimmer, Christoph Scholl, Bernd Becker: Equivalence Checking for Partial Implementations Revisited GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, 2013: 61-70, Universität Rostock ITMZ (Hrsg).
• Karina Gitina, Sven Reimer, Matthias Sauer, Ralf Wimmer, Christoph Scholl, Bernd Becker: Equivalence Checking of Partial Designs using Dependency Quantified Boolean Formulae Int'l Conf. on Computer Design, 2013: 396-403, IEEE Computer Society (Hrsg). : http://dx.doi.org/10.1109/ICCD.2013.6657071
• Karsten Scheibler, Matthias Sauer, Kohei Miyase, Bernd Becker: Controlling Small-Delay Test Power Consumption using Satisfibility Modulo Theory Solving GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen”, 2013. : http://www.avacs.org/fileadmin/Publikationen/Open/scheibler.tuz2013.pdf
• Karsten Scheibler, Stefan Kupferschmid, Bernd Becker: Recent Improvements in the SMT Solver iSAT GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, 2013. : http://www.avacs.org/fileadmin/Publikationen/Open/scheibler.mbmv2013.pdf
• Matthias Sauer, Sven Reimer, Ilia Polian, Tobias Schubert, Bernd Becker: Provably Optimal Test Cube Generation Using Quantified Boolean Formula Solving ASP Design Automation Conf., 2013. : http://dx.doi.org/10.1109/ASPDAC.2013.6509651
• Matthias Sauer, Sven Reimer, Stefan Kupferschmid, Tobias Schubert, Paolo Marin, Bernd Becker: Applying BMC, Craig Interpolation and MAX-SAT to Functional Justification in Sequential Circuits RCRA International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion, 2013.
• Matthias Sauer, Sven Reimer, Tobias Schubert, Ilia Polian, Bernd Becker: Efficient SAT-Based Dynamic Compaction and Relaxation for Longest Sensitizable Paths Conf. on Design, Automation and Test in Europe, 2013: 448-453. : http://dx.doi.org/10.7873/DATE.2013.100
• Stefan Kupferschmid: Über Craigsche Interpolation und deren Anwendung in der formalen ModellprüfungDer Andere Verlag, 1. Auflage, 2013 (Design, Test and Verification of Embedded Systems).
• Ulrich Loup, Karsten Scheibler, Florian Corzilius, Erika Ábrahám, Bernd Becker: A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition CADE, 2013; 7898: 193-207, Springer (Hrsg). : http://dx.doi.org/10.1007/978-3-642-38574-2_13
• Matthias Sauer, Stefan Kupferschmid, Alexander Czutro, Ilia Polian, Sudhakar M. Reddy, Bernd Becker: Functional Justification in Sequential Circuits using SAT and Craig Interpolation GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen”, 2012.
• Matthias Sauer, Stefan Kupferschmid, Alexander Czutro, Ilia Polian, Sudhakar M. Reddy, Bernd Becker: Functional Test of Small-Delay Faults using SAT and Craig Interpolation Int'l Test Conf., 2012: 1-8. : http://dx.doi.org/10.1109/TEST.2012.6401550
• Matthias Sauer, Stefan Kupferschmid, Alexander Czutro, Sudhakar M. Reddy, Bernd Becker: Analysis of Reachable Sensitisable Paths in Sequential Circuits with SAT and Craig Interpolation Int'l Conf. on VLSI Design, 2012. : http://dx.doi.org/10.1109/VLSID.2012.101
• Sven Reimer, Florian Pigorsch, Christoph Scholl, Bernd Becker: Enhanced Integration of QBF Solving Techniques GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, 2012: 133-143.
• Andreas Eggers, Evgeny Kruglov, Stefan Kupferschmid, Karsten Scheibler, Tino Teige, Christoph Weidenbach: Superposition modulo non-linear arithmetic Int'l Symp. on Frontiers of Combining Systems, 2011: 119-134, Springer (Hrsg). : http://dx.doi.org/10.1007/978-3-642-24364-6_9
• Ernst Althaus, Bernd Becker, Daniel Dumitriu, Stefan Kupferschmid: Integration of an LP solver into interval constraint propagation Int'l Conf. on Combinatorial optimization and applications, 2011: 343-356, Springer (Hrsg). : http://dx.doi.org/10.1007/978-3-642-22616-8_27
• Stefan Kupferschmid, Bernd Becker: Craig interpolation in the presence of non-linear constraints Formal Modeling and Analysis of Timed Systems, 2011: 240-255, Springer (Hrsg). : http://dx.doi.org/10.1007/978-3-642-24310-3_17
• Stefan Kupferschmid, Bernd Becker: Craigsche Interpolation für Boolesche Kombinationen linearer und nichtlinearer Ungleichungen 2011: 279-288, OFFIS-Institut für Informatik (Hrsg).
• Stefan Kupferschmid, Bernd Becker, Tino Teige, Martin Fränzle: Proof Certificates and Non-linear Arithmetic Constraints IEEE Design and Diagnostics of Electronic Circuits and Systems, 2011: 429-434. : http://dx.doi.org/10.1109/DDECS.2011.5783131
• Stefan Kupferschmid, Matthew Lewis, Tobias Schubert, Bernd Becker: Incremental preprocessing methods for use in BMC Formal Methods in System Design, 2011; 39: 185-204. : http://dx.doi.org/10.1007/s10703-011-0122-4
• Sven Reimer, Florian Pigorsch, Christoph Scholl, Bernd Becker: Integration of Orthogonal QBF Solving Techniques Conf. on Design, Automation and Test in Europe, 2011: 149-154. : http://dx.doi.org/10.1109/DATE.2011.5763034
• Christian Miller, Stefan Kupferschmid, Bernd Becker: Exploiting Craig Interpolants in Bounded Model Checking for Incomplete Designs GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, 2010; 13: 77-86.
• Christian Miller, Stefan Kupferschmid, Matthew Lewis, Bernd Becker: Encoding Techniques, Craig Interpolants and Bounded Model Checking for Incomplete Designs Theory and Applications of Satisfiability Testing, 2010: 194-208, Springer (Hrsg). : http://dx.doi.org/10.1007/978-3-642-14186-7_17
• Natalia Kalinnik, Erika Ábrahám, Tobias Schubert, Ralf Wimmer, Bernd Becker: Exploiting Different Strategies for the Parallelization of an SMT Solver GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, 2010: 97-106, Fraunhofer Verlag (Hrsg).
• Stefan Kupferschmid, Matthew Lewis, Tobias Schubert, Bernd Becker: Incremental Preprocessing Methods for use in BMC Int'l Workshop on Hardware Verification, 2010.
• Andreas Eggers, Natalia Kalinnik, Stefan Kupferschmid, Tino Teige: Challenges in Constraint-Based Analysis of Hybrid Systems Recent Advances in Constraints, 2009; 5655: 51-65, Springer (Hrsg). : http://dx.doi.org/10.1007/978-3-642-03251-6_4
• Christoph Scholl, Stefan Disch, Florian Pigorsch, Stefan Kupferschmid: Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints Tools and Algorithms for the Construction and Analysis of Systems, 2009; 5505: 383-397, Springer (Hrsg).
• Natalia Kalinnik, Tobias Schubert, Erika Ábrahám, Ralf Wimmer, Bernd Becker: Picoso - A Parallel Interval Constraint Solver Int'l Conf. on Parallel and Distributed Processing Techniques and Applications, 2009: 473-479, CSREA Press (Hrsg).
• Stefan Kupferschmid, Tino Teige, Bernd Becker, Martin Fränzle: Proofs of Unsatisfiability for mixed Boolean and Non-linear Arithmetic Constraint Formulae GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, 2009: 27-36.
• Andreas Eggers, Natalia Kalinnik, Stefan Kupferschmid, Tino Teige: Challenges in Constraint-based Analysis of Hybrid Systems ERCIM Workshop on Constraint Solving and Constraint Logic Programming, 2008.
• Christoph Scholl, Stefan Disch, Florian Pigorsch, Stefan Kupferschmid: Using an SMT Solver and Craig Interpolation to Detect and Remove Redundant Linear Constraints in Representations of Non-Convex Polyhedra Int'l Workshop on Satisfiability Modulo Theories, 2008: 18-26.
• Jochen Eisinger: Upper Bounds on the Automata Size for Integer and Mixed Real and Integer Linear Arithmetic EACSL Annual Conf. on Computer Science Logic, 2008: 430-444, Springer-Verlag (Hrsg).
• Bernd Becker, Jochen Eisinger, Felix Klaedtke: Parallelization of Decision Procedures for Automatic Structures Workshop on Omega-Automata, 2007.