TRR 14:  AVACS - Automatische Verifikation und Analyse komplexer Systeme

• Fachliche Zuordnung: Informatik, System- und Elektrotechnik
• Förderung: Förderung von 2004 bis 2015
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 5485999

• Erstellungsjahr: 2017

Zusammenfassung der Projektergebnisse

Der SFB-Transregio AVACS hat Algorithmen zur automatischen Analyse und formalen Verifikation von komplexen Cyber-Physischen Systemen entwickelt. Derartige Systeme verwenden Software und Hardware zur automatisierten Steuerung, Regelung und Optimierung physischer Systeme wie Fahrzeuge, Flugzeuge, Züge oder kooperierender vernetzter Transportsysteme. Während der 12-jährigen Laufzeit von AVACS ist erwartungsgemäß die Komplexität dieser Systeme bezüglich Anzahl der verwendeten Hardwarebausteine wie Softwareumfang exponentiell gewachsen. Zu Projektbeginn nicht vorhersehbar war die damit einhergehende drastische Zunahme der Autonomie der Entscheidungsfindung, in der bisher von Menschen vorgenommene Abwägungen nunmehr durch in Software realisierte Entscheidungsfindung ersetzt wird. Dies ist prominent aktuell im Bereich des Hochautomatisierten Fahrens beobachtbar, betrifft aber alle "Smart Systems", wie etwa Smart Production, Smart Health, Smart Energy und eben auch Smart Mobility. Die domänenübergreifend zu beobachtenden Delegation von Entscheidungskompetenzen an technische Systeme stellt eine besondere Herausforderung in sicherheitsrelevanten Anwendungen dar. Die durch AVACS adressierte zentrale wissenschaftliche Herausforderung der Bereitstellung von formalen Methoden zum Nachweis von Sicherheits-, Stabilitäts-, Verfügbarkeits- und Echtzeitanforderungen könnte somit nicht besser gewählt worden sein, ist sie damit doch in ihrer Relevanz drastisch gestiegen: Nahezu jede industrielle Anwendungsdomäne wird durch solche hochautomatisierten Systeme kontrolliert werden, der Nachweis ihrer funktionalen Korrektheit, ihrer Sicherheit, und ihrer Verfügbarkeit ist somit von zentraler gesellschaftlicher Bedeutung. AVACS ist es gelungen, durch die standortübergreifende Vernetzung von fachlichen Kompetenzen eine Forschungsumgebung aufzubauen, deren Forschungsresultate dazu führen, dass wir heute • die mathematische Essenz von vernetzten Cyber-Physikalischen Systemen durch kompakte mathematischen Modellbildungen derart präzise gefasst haben, das diese im Prinzip eine vollständige Formalisierung hierarchischer ebenen-übergreifender Entwurfsprozesse solcher Systeme unterstützen, • die Ausdrucksstärke und Komplexität von Logiken charakterisieren können, die zur Formalisierung der Anforderungen der Verfügbarkeit, Sicherheit und Echzeitfähigkeit solcher Systeme auch in kooperativen Anwendungen erforderlich ist, • den Stand der Technik in vielen Klassen formaler Verifikationsalgorithmen und Syntheseverfahren definieren, • die Prinzipien des Entwurfs solcher vernetzter Cyber-Physischer Systeme so tief durchdrungen haben, dass wir Entwurfsregeln aufstellen können, deren Einhaltung die vollständige Analysierbarkeit solcher komplexen Systeme durch eine Kombination systematischer Dekompositionstechniken, kompositioneller Analysetechniken, Abstraktionstechniken und dedizierter in AVACS entwickelter Verifikationsalgorithmen gewährleistet. Während in der ersten Förderphase eine Fokussierung auf jeweils einzelne bekannter Systemaspekte erfolgte, wurde anschließend für solche Modelle von CPS Verifikationsverfahren entwickelt, die eine Vielzahl von Merkmalen solcher Systemklassen gleichzeitig aufweisen, wie etwa probabilistische hybride Automaten mit nicht-linearer Zustandsdynamik, Spiele über sich dynamisch rekonfigurierenden Arenen, dynamisch vernetzte Systeme linearer hybrider Automaten, oder parametrisierte Familien zeitbehafteter Automaten über komplexen Zustandsräumen. Modellklassen mit formal nicht entscheidbaren Verifikationsproblemen erwiesen sich als entscheidbar für Teilklassen, welche die aus industrieller Sicht ohnehin notwendigen Robustheitseigenschaften berücksichtigen. AVACS hat systematisch und nachhaltig den Stand der Forschung bei SMT-Entscheidungsverfahren durch Beiträge zu ihrer Skalierbarkeit und Übertragung auf zuvor unerreicht reichhaltige Fragmente von Arithmetik und Logik geprägt. Zahlreiche Transferaktivitäten greifen Ergebnisse von AVACS auf und führen sie näher an industrielle Anwendungen. Dies kann und wird erfolgreich sein, wenn die von AVACS aufgestellten Entwurfsrichtlinien industriell durchgesetz werden. Unter diesen Umständen werden unsere Resultate dazu beitragen, dass hoch automatisierte vernetzte Cyber-Physikalische Systeme robust und sicher sind.

Projektbezogene Publikationen (Auswahl)

• Approximate symbolic model checking for incomplete designs. In Formal Methods in Computer-Aided Design, 2004, pp. 290–305
  T. Nopper and C. Scholl
  (Siehe online unter https://doi.org/10.1007/978-3-540-30494-4_21)
• Uniform distributed synthesis. In 20th Annual IEEE Symposium on Logic in Computer Science (LICS 2005), 2005, pp. 321–330. IEEE Computer Society Press
  B. Finkbeiner and S. Schewe
  (Siehe online unter https://doi.org/10.1109/LICS.2005.53)
• Directed model checking with distance-preserving abstractions. In A. Valmari, ed., Model Checking Software, 13th International SPIN Workshop, 2006, LNCS 3925, pp. 19–34. Springer
  K. Dräger, B. Finkbeiner, and A. Podelski
  (Siehe online unter https://doi.org/10.1007/11691617_2)
• Model checking of hybrid systems: From reachability towards stability. In Hybrid Systems: Computation and Control, HSCC’06, 2006, LNCS 3927, pp. 507 – 521
  A. Podelski and S. Wagner
  (Siehe online unter https://doi.org/10.1007/11730637_38)
• Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. Journal on Satisfiability, Boolean Modeling and Computation – Special Issue on SAT/CP Integration, 1:209–236, 2007
  M. Fränzle, C. Herde, S. Ratschan, T. Schubert, and T. Teige
  (Siehe online unter https://doi.org/10.3233/SAT190012)
• Guaranteed termination in the verification of LTL properties of non-linear robust discrete time hybrid systems. International Journal of Foundations of Computer Science, 18(1):63–88, 2007
  W. Damm, G. Pinto, and S. Ratschan
  (Siehe online unter https://doi.org/10.1142/S0129054107004577)
• Slicing abstractions. Fundamenta Informaticae, 89(4):369–392, 2008
  I. Brückner, K. Dräger, B. Finkbeiner, and H. Wehrheim
  (Siehe online unter https://dl.acm.org/doi/10.5555/2366366.2366368)
• Stochastic satisfiability modulo theory: A novel technique for the analysis of probabilistic hybrid systems. In M. Egerstedt and B. Mishra, eds., Proceedings of the 11th International Conference on Hybrid Systems: Computation and Control (HSCC’08), 2008, LNCS 4981, pp. 172–186. Springer
  M. Fränzle, H. Hermanns, and T. Teige
  (Siehe online unter https://doi.org/10.1007/978-3-540-78929-1_13)
• The surprising robustness of (closed) timed automata against clock-drift. In G. Ausiello, J. Karhumäki, G. Mauri, and L. Ong, eds., IFIP International Conference on Theoretical Computer Science (IFIP TCS), 2008, vol. 273, pp. 537–553. Springer
  M. Swaminathan, M. Fränzle, and J.-P. Katoen
  (Siehe online unter https://doi.org/10.1007/978-0-387-09680-3_36)
• Compositional dependability evaluation for statemate. Institute of Electrical and Electronics Engineers (IEEE) Transactions on Software Engineering, 35(2):274–292, 2009
  E. Böde, M. Herbstritt, H. Hermanns, S. Johr, T. Peikenkamp, R. Pulungan, J. Rakow, R. Wimmer, and B. Becker
  (Siehe online unter https://doi.org/10.1109/TSE.2008.102)
• Decompositional construction of lyapunov functions for hybrid systems. In R. Majumdar and P. Tabuada, eds., 12th International Conference on Hybrid Systems: Computations and Control, 2009, LNCS 5469, pp. 276–290. Springer
  J. Oehlerking and O. Theel
  (Siehe online unter https://doi.org/10.1007/978-3-642-00602-9_20)
• Refinement of trace abstraction. In J. Palsberg and Z. Su, eds., Static Analysis Symposium (SAS), 2009, LNCS 5673, pp. 69–85. Springer
  M. Heizmann, J. Hoenicke, and A. Podelski
  (Siehe online unter https://doi.org/10.1007/978-3-642-03237-0_7)
• Automatic verification of parametric specifications with complex topologies. In D. Mery and S. Merz, eds., Integrated Formal Methods (IFM), 2010, LNCS 6396, pp. 152–167. Springer
  J. Faber, C. Ihlemann, S. Jacobs, and V. Sofronie-Stokkermans
  (Siehe online unter https://doi.org/10.1007/978-3-642-16265-7_12)
• Coordination logic. In A. Dawar and H. Veith, eds., Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the European Association for Computer Science Logic (EACSL), Brno, Czech Republic, August 23-27, 2010. Proceedings, 2010, LNCS 6247, pp. 305–319. Springer-Verlag
  B. Finkbeiner and S. Schewe
  (Siehe online unter https://doi.org/10.1007/978-3-642-15205-4_25)
• Counterexample-guided focus. In M. V. Hermenegildo and J. Palsberg, eds., 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 20-22, 2010, 2010, pp. 249–260. Association for Computing Machinery (ACM)
  A. Podelski and T. Wies
  (Siehe online unter https://doi.org/10.1145/1706299.1706330)
• Resilience analysis: Tightening the crpd bound for setassociative caches. In LCTES ’10: Proceedings of the ACM SIGPLAN/SIGBED 2010 conference on Languages, compilers, and tools for embedded systems, New York, NY, USA, 2010, pp. 153–162. ACM
  S. Altmeyer, C. Maiza, and J. Reineke
  (Siehe online unter https://doi.org/10.1145/1755951.1755911)
• Symblicit calculation of long-run averages for concurrent probabilistic systems. In G. Ciardo and R. Segala, eds., Proceedings of the 7th International Conference on Quantitative Evaluation of Systems (QEST), Williamsburg, Virginia, USA, 2010, pp. 27–36. IEEE Computer Society
  R. Wimmer, B. Braitling, B. Becker, E. M. Hahn, P. Crouzen, H. Hermanns, A. Dhama, and O. Theel
  (Siehe online unter https://doi.org/10.1109/QEST.2010.12)
• An abstract model for proving safety of multi-lane traffic manoeuvres. In S. Qin and Z. Qiu, eds., International Conference on Formal Engineering Methods (ICFEM), 2011, LNCS 6991. Springer
  M. Hilscher, S. Linker, E.-R. Olderog, and A. Ravn
  (Siehe online unter https://doi.org/10.1007/978-3-642-24559-6_28)
• Automating the design flow for distributed embedded automotive applications: Keeping your time promises, and optimizing costs, too. In I. Bate and R. Passerone, eds., Proc. International Symposium on Industrial Embedded Systems (SIES’11), 2011. IEEE Computer Society
  M. Büker, W. Damm, G. Ehmen, A. Metzner, I. Stierand, and E. Thaden
  (Siehe online unter https://doi.org/10.1109/SIES.2011.5953658)
• Bounding the equilibrium distribution of markov population models. Numerical Linear Algebra with Applications, 6(18):931–946, 2011
  T. Dayar, H. Hermanns, D. Spieler, and V. Wolf
  (Siehe online unter https://doi.org/10.1002/nla.795)
• Constraint-based analysis of concurrent probabilistic hybrid systems: An application to networked automation systems. Nonlinear Analysis: Hybrid Systems, 5(2):343–366, 2011
  T. Teige, A. Eggers, and M. Fränzle
  (Siehe online unter https://doi.org/10.1016/j.nahs.2010.04.009)
• Craig interpolation in the presence of non-linear constraints. In Formal Modeling and Analysis of Timed Systems, 9th International Conference, FORMATS 2011, Aaalborg, Denmark, September 21-23, 2011, Proceedings, Berlin Heidelberg, 2011, LNCS 6916. Springer
  S. Kupferschmid and B. Becker
  (Siehe online unter https://doi.org/10.1007/978-3-642-24310-3_17)
• Decomposition of Stability Proofs for Hybrid Systems. Doctoral dissertation, Carl von Ossietzky Universität Oldenburg, Department of Computing Science, Germany, 2011. Supervisors: Prof. Dr. Oliver Theel and Prof. Dr. Martin Fränzle
  J. Oehlerking
  
• Does it pay to extend the perimeter of a world model? In M. Butler and W. Schulte, eds., Proceedings of the 17th International Symposium on Formal Methods, 2011, LNCS 6664, pp. 12–26. Springer-Verlag
  W. Damm and B. Finkbeiner
  (Siehe online unter https://doi.org/10.1007/978-3-642-21437-0_4)
• PTIME parametric verification of safety properties for reasonable linear hybrid automata. Mathematics in Computer Science, Special Issue on Numerical Software Verification, 5(469), 2011
  W. Damm, C. Ihlemann, and V. Sofronie-Stokkermans
  (Siehe online unter https://doi.org/10.1007/s11786-011-0098-x)
• Superposition modulo non-linear arithmetic. In C. Tinelli and V. Sofronie-Stokkermans, eds., 8th international Symposium on Frontiers of Combining Systems (FroCos 2011), 2011, LNAI 6989, pp. 119–134. Springer
  A. Eggers, E. Kruglov, S. Kupferschmid, K. Scheibler, T. Teige, and C. Weidenbach
  (Siehe online unter https://doi.org/10.1007/978-3-642-24364-6_9)
• A box-based distance between regions for guiding the reachability analysis of spaceex. In P. Madhusudan and S. A. Seshia, eds., Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, 2012, LNCS 7358, pp. 479–494. Springer
  S. Bogomolov, G. Frehse, R. Grosu, H. Ladan, A. Podelski, and M. Wehrle
  (Siehe online unter https://doi.org/10.1007/978-3-642-31424-7_35)
• Counterexample-guided synthesis of observation predicates. In M. Jurdzinski and D. Nickovic, eds., Formal Modeling and Analysis of Timed Systems - 10th International Conference, FORMATS 2012, London, UK, September 18-20, 2012. Proceedings, 2012, LNCS 7595, pp. 107–122. Springer
  R. Dimitrova and B. Finkbeiner
  (Siehe online unter https://doi.org/10.1007/978-3-642-33365-1_9)
• Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces. Science of Computer Programming, Special Issue on Automated Verification of Critical Systems, 77(10-11):1122–1150, 2012
  W. Damm, H. Dierks, S. Disch, W. Hagemann, F. Pigorsch, C. Scholl, U. Waldmann, and B. Wirtz
  (Siehe online unter https://doi.org/10.1016/j.scico.2011.07.006)
• Generalized Craig interpolation for stochastic Boolean satisfiability problems with applications to probabilistic state reachability and region stability. Logical Methods in Computer Science, 8(2):1–32, 2012
  T. Teige and M. Fränzle
  (Siehe online unter https://doi.org/10.2168/LMCS-8(2:16)2012)
• Safety verification for probabilistic hybrid systems. European Journal of Control, 18(6):588–590, 2012
  L. Zhang, Z. She, S. Ratschan, H. Hermanns, and E. M. Hahn
  (Siehe online unter https://doi.org/10.1016/S0947-3580(12)71160-3)
• Bounded synthesis. International Journal on Software Tools for Technology Transfer (STTT), 15(5-6):519–539, 2013
  B. Finkbeiner and S. Schewe
  (Siehe online unter https://doi.org/10.1007/s10009-012-0228-z)
• Can we build it: Formal synthesis of control strategies for cooperative driver assistance systems. Mathematical Structures in Computer Science, Special Issue on Practical and Lightweight Formal Methods for the Design, Modeling and Analysis of Software Systems, 23(4):676–725, 2013
  W. Damm, H.-J. Peter, J. Rakow, and B. Westphal
  (Siehe online unter https://doi.org/10.1017/S0960129512000230)
• Equivalence checking of partial designs using dependency quantified boolean formulae. In Proceedings of the 31st IEEE International Conference on Computer Design, Asheville, NC, USA, 2013, pp. 396–403. IEEE Computer Society Press
  K. Gitina, S. Reimer, M. Sauer, R. Wimmer, C. Scholl, and B. Becker
  (Siehe online unter https://doi.org/10.1109/ICCD.2013.6657071)
• The relative pruning power of strong stubborn sets and expansion core. In Proceedings of the 23rd International Conference on Automated Planning and Scheduling (ICAPS 2013), 2013, pp. 251–259
  M. Wehrle, M. Helmert, Y. Alkhazraji, and R. Mattmüller
  (Siehe online unter https://doi.org/10.1609/icaps.v23i1.13565)
• Decidability of verification of safety properties of spatial families of linear hybrid automata. In C. Lutz and S. Ranise, eds., Frontiers of Combining Systems (FroCoS), 2015, pp. 186–202. Springer
  W. Damm, M. Horbach, and V. Sofronie-Stokkermans
  (Siehe online unter https://doi.org/10.1007/978-3-319-24246-0_12)
• Proof theory of a multi-lane spatial logic. Logical Methods in Comp. Sci., 11(3), 2015. Regular Issue, 27 pp.
  S. Linker and M. Hilscher
  (Siehe online unter https://doi.org/10.2168/LMCS-11(3:4)2015)
• Solving DQBF through quantifier elimination. In Proceedings of the International Conference on Design, Automation & Test in Europe (DATE), Grenoble, France, 2015, pp. 1617–1622. IEEE
  K. Gitina, R. Wimmer, S. Reimer, M. Sauer, C. Scholl, and B. Becker
  (Siehe online unter https://doi.org/10.7873/DATE.2015.0098)
• Towards compact abstract domains for pipelines. In R. Meyer, A. Platzer, and H. Wehrheim, eds., Correct System Design, Essays Dedicated to Ernst-Rüdiger Olderog on the Occasion of his 60th Birthday, LNCS. Springer, 2015
  S. Hahn, J. Reineke, and R. Wilhelm
  (Siehe online unter https://doi.org/10.1007/978-3-319-23506-6_14)
• WCET analysis for multi-core processors with shared buses and event-driven bus arbitration. In Proceedings of the 23rd International Conference on Real Time Networks and Systems, RTNS 2015, Lille, France, November 4-6, 2015, 2015, pp. 193–202
  M. Jacobs, S. Hahn, and S. Hack
  (Siehe online unter https://doi.org/10.1145/2834848.2834872)