TRR 14:  Automatic Verification and Analysis of Complex Systems

• Subject Area: Computer Science, Systems and Electrical Engineering
• Term: from 2004 to 2015
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 5485999

• Final Report Year: 2017

Final Report Abstract

The Transregional Collaborative Research Center AVACS focused on rigorous, highly automated methods and algorithms for the analysis and verification of what would today be called complex Cyber-Physical Systems, in which software and hardware implement algorithms for highly automated control of physical systems such as aircrafts, cars, trains, or systems of these. Within the twelve years spanned by AVACS, we have seen the projected exponential take-up of embedded systems, creating seemingly intelligent systems, capable of autonomous decision-making, both in the transportation domain targeted by AVACS, but also in other industrial sectors such as enabling smartness in smart grids, smart homes, smart cities, smart crisis management etc. Common to all is the increasing degree of delegation of decision making from humans to technical systems. Thus the need identified by AVACS at its conception, to “verify compliance of embedded control to reliability, coordination, control and real-time requirements”, and hence the relevance of AVACS results has drastically increased during its 12 year funding period. Virtually all industrial domains will be dependent on (large scale networks of) such highly autonomous systems, and thus guaranteeing their correctness and availability is of extreme industrial and societal relevance. AVACS addressed in its three research areas of real-time systems, hybrid systems, and systems of systems fundamental challenges in the verification and analysis of such Systems of Cyber-Physical Systems. Through the solutions created in this creative research environment, • we understand the mathematical essence of Systems of Cyber-Physical Systems and have mathematical models allowing in principle a complete formalization of multi-layered design of such systems; • we understand the principles of the design of such Systems of Cyber-Physical Systems, in that we can provide guidelines for building such systems enabling the use of decomposition techniques, compositional reasoning, and abstraction for reducing the complexity of the verification problem; • we understand the expressivity of logics required to capture coordination, control, reliability and real-time requirements, as well as various other industrially relevant types of requirement, and have investigated the complexity of such logics and – if applicable – decision procedures; • we master a broad class of verification and formal synthesis approaches defining the state of the art for the verification of such complex systems. While research in the first funding phase focused in isolation on the analysis of real-time systems, hybrid systems, and systems of systems, the cross fertilizations of results across research areas achieved by AVACS manifests itself in verification techniques for highly complex models, such as in the analysis of probabilistic hybrid automata with non-linear dynamics, for the analysis of probabilistic hybrid topologylabeled game structures, the analysis of dynamically communicating ensembles of linear hybrid automata, and the analysis of parametrically generated real-time systems with complex types. Model classes proven to be undecidable were shown nonetheless to be amenable to complete verification methods by exploiting guidelines generally accepted in industry, such as those for robust system design. AVACS has played a leading role in systematically advancing the state of the art in arithmetic SMT solving, enhancing both its scalability and its coverage of unprecedentedly rich fragments of arithmetic and logic. Numerous transfer activities are taking the foundational results of AVACS closer to industrial application. This can and will continue to be successful, when principles of design for analyzability as developed by AVACS are adhered to. Only if such design principles are observed, can the results of AVACS contribute to building predictable and robust smart systems.

Publications

• Approximate symbolic model checking for incomplete designs. In Formal Methods in Computer-Aided Design, 2004, pp. 290–305
  T. Nopper and C. Scholl
  (See online at 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
  (See online at 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
  (See online at 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
  (See online at 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
  (See online at 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
  (See online at 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
  (See online at 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
  (See online at 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
  (See online at 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
  (See online at 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
  (See online at 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
  (See online at 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
  (See online at 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
  (See online at 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
  (See online at 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
  (See online at 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
  (See online at 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
  (See online at 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
  (See online at 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
  (See online at 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
  (See online at 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
  (See online at 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
  (See online at 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
  (See online at 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
  (See online at 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
  (See online at 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
  (See online at 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
  (See online at 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
  (See online at 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
  (See online at 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
  (See online at 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
  (See online at 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
  (See online at 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
  (See online at 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
  (See online at 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
  (See online at 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
  (See online at 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
  (See online at 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
  (See online at https://doi.org/10.1145/2834848.2834872)