AVACS

Automatic Verification and Analysis of Complex Systems


General Information

This project addresses the rigorous mathematical analysis of models of complex safety critical computerized systems, such as aircrafts, trains, cars, or other artifacts, whose failure can endanger human life. Our aim is to raise the state of the art in automatic verification and analysis techniques (v&a) from its current level, where it is applicable only to isolated facets (concurrency, time, continuous control, stability, dependability, mobility, data structures, hardware constraints, modularity, levels of refinement), to a level allowing a comprehensive and holistic verification of such systems.

  • We will investigate the mathematical models and their interrelationship as they arise at the various levels of design of safety critical computerized systems. These models range from classical non-deterministic transition systems to probabilistic, real-time, and hybrid system models.
  • We will, in particular, deal with the complete range of time-models needed to support the development of concrete systems, and the transition between them. This includes the determination of safe sampling rates in plant control as well as the transition between virtual time models and physical execution time.
  • We will also address a wide range of system structures in this application domain. These range from models of distributed target architectures (such as hierarchical bus-structures connecting multiple electronic control units) to task models (depicting hierarchical task structures with communication and timing requirements) to specification models of electronic control units (such as a controller enforcing a speed-profile) to system models (e.g. of the electronic on-board train systems) to inter-system specification models (e.g. for coordination of train movements).

Today's v&a technology at best addresses isolated points in this space of models. The proposed project sets out to develop automatic verification techniques covering the entire space. It is our firm belief that by improving and better automating base verification methods (such as abstract interpretation, SAT solvers, symbolic model checking, abstraction techniques, linear programming, constraint solving, Lyapunov functions, automatic decision procedures for relevant first-order theories, automata based verification, heuristic search) and by integrating them in a deep and focused manner we will be able to achieve a dramatic increase in the complexity of models amenable to automatic verification. (By complexity we mean both system size as well as logical complexity as induced by the interferences between the various facets of the system.) By identifying new, as well as by exploiting well-established design and modeling paradigms (mathematically reflected by decomposition theorems that break down complex systems into manageable sub-systems and facets), the combination of the individual, complementing automated verification techniques will deliver synergies that we do not see in present verification systems.

Project Area R - Real-Time Systems

Real-time systems are systems that interact with their environment in such a way that for certain inputs the corresponding outputs have to occur within given time bounds. Many embedded systems, in particular those in safety critical applications, are of this type. The practical importance of this class of systems has led to a large body of research on the specification, verification and analysis of real-time systems.
Analysis and verification of real-time systems is based on computational models of such systems. Models with continuous time are close to the physical world and are well suited for dealing with the requirement and specification level; their automatic verification is performed using tools based on timed automata with real-valued clocks. To gain in efficiency also models with discrete time are considered; their automatic verification is performed using classical approaches to temporal logic model checking. At the level of machine real-time systems are modeled as set of tasks that need to be scheduled to meet the required deadlines.
While these real-time models have led to powerful analysis and verifications techniques, they turn out to be too idealistic or too simplistic to deal with the challenges of high-level specification languages, highly concurrent systems, and the intricacies of distributed computer architectures.
The AVACS subprojects R1--3 strive to overcome these restrictions by exploiting the structure of the real-time systems at all levels of abstraction ranging from specification level down to implementation level:

  • subproject R1 will develop verification techniques for real-time requirements of high-level specifications based on constraint manipulation, predicate abstraction, and decision procedures for high-level data types;
  • subproject R2 will develop task distribution and scheduling techniques taking the constraints of distributed computer architectures into account, in particular the combination of caches and pipelines;
  • subproject R3 considers highly concurrent real-time systems and develops model checking techniques that combine heuristic search with abstraction.

Project Area S - Coarse Grain System Structure

Project Area S focuses on techniques to support the global analysis of the interplay between different systems, or between subsystems, thus addressing both inter-system and system-level design. Typical instances in the train system domain relate to the interaction between trains and track-side elements such as RBC, s, or between the different components of the on-board electronic subsystems of a train. The overall challenge for Project Area S is thus the need to address complete systems, or even systems of systems, demanding dedicated techniques to cater for the sheer complexity of resulting models. Subproject S1 addresses this by automating compositional verification; it uses learning strategies and combinations of abstraction techniques, game theory, and SAT and model checking based verification methods to automatically synthesize assumptions, allowing to reduce global verification of (potentially only partially specified) system level designs to local verification tasks. The particular challenges of inter-system coordination protocols, which typically require dynamically changing communication structures and must address systems entering and leaving surveillance regions, are attacked in S2 with a combination of static analysis techniques, abstraction techniques, and symmetry arguments to reduce the verification of such coordination protocols to finite state verification problems. Subproject S3 provides formal proofs of system dependability requirements through stochastic model checking of system models, taking into account failure models and component failure behaviors, while deriving safety requirements for subsequent design steps.
By addressing complete systems and their interplay, Project Area S provides methods for reducing global verification tasks to smaller problem instances (S1, S2) and dependability analysis, which inherently requires global system analysis. Subprojects S1 and S2 complement each other, in that verification instances resulting from the reduction methods of S2 can be further decomposed using techniques of S1. Models used will reflect the particular complexity dimension attacked in each subproject, providing sufficiently rich structuring methods to asynchronously compose transition systems, supporting their dynamic creation and destruction and dynamic communication structures for S2, and using extended Markov Processes in S3. Later project phases will enrich the class of models, allowing to deal with real-time and hybrid component models, and extend decomposition theorems to such richer classes of models, thus paving the way for realizing the AVACS vision, where an overall verification methodology invokes such decomposition theorems, unfolding a proof tree for global problems to a level where verification tasks can be discharged with the verification methods developed in Project Areas R and H.

Publications

  1. Influence of the Task Model on the Precision of Scheduling Analysis for Preemptive Systems – Status Report
    S. Altmeyer, and C. Maiza
    Proceedings of the 2nd International Real-Time Scheduling Open Problems Seminar, 2011. [bib]
  2. Cache Related Pre-emption Aware Response Time Analysis for Fixed Priority Pre-emptive Systems
    S. Altmeyer, R. I. Davis, and C. Maiza
    Proceedings of the 32nd IEEE Real-Time Systems Symposium (RTSS'11), 2011. [bib]
  3. Semi-Automatic Derivation of Timing Models for WCET Analysis
    M. Schlickling, and M. Pister
    LCTES '10: Proceedings of the ACM SIGPLAN/SIGBED 2010 conference on Languages, compilers, and tools for embedded systems, 2010. [doi]  [bib]
  4. Best Probabilistic Transformers
    B. Wachter, and L. Zhang
    VMCAI, 2010. [pdf]  [bib]
  5. A Graph Transformation Case Study for the Topology Analysis of Dynamic Communication System
    P. Backes, and J. Reineke
    Transformation Tool Contest 2010, 2010. [pdf]  [slides]  [bib]
  6. Abstract Topology Analysis of the Join Phase of the Merge Protocol
    P. Backes, and J. Reineke
    Transformation Tool Contest 2010, 2010. [pdf]  [slides]  [bib]
  7. Computing the Maximum Blocking Time for Scheduling with Deferred Preemption
    S. Altmeyer, C. Burguière, and R. Wilhelm
    Workshop on Software Technologies for Future Dependable Distributed Systems, 2009. [doi]  [bib]
  8. Abstract Interpretation of FIFO Replacement
    D. Grund, and J. Reineke
    Static Analysis, 16th International Symposium, SAS 2009, 2009. [doi]  [pdf]  [slides]  [bib]
  9. Branch Target Buffers: WCET Analysis Framework and Timing Predictability
    D. Grund, J. Reineke, and G. Gebhard
    15th International Conference on Embedded and Real-Time Computing Systems and Applications, RTCSA 2009, 2009. [doi]  [pdf]  [slides]  [bib]
  10. Memory Hierarchies, Pipelines, and Buses for Future Architectures in Time-critical Embedded Systems
    R. Wilhelm, D. Grund, J. Reineke, M. Schlickling, M. Pister, and C. Ferdinand
    IEEE Transactions on CAD of Integrated Circuits and Systems, 28 (7), 2009. [doi]  [bib]
  11. INFAMY: An Infinite-State Markov Model Checker
    E. M. Hahn, H. Hermanns, B. Wachter, and L. Zhang
    Computer Aided Verification, 2009. [doi]  [bib]
  12. Best Probabilistic Transformers and Beyond
    B. Wachter, and L. Zhang
    Technical Report, SFB/TR 14 AVACS, 2009. [pdf]  [bib]
  13. Sound and Efficient WCET Analysis in the Presence of Timing Anomalies
    J. Reineke, and R. Sen
    Proceedings of 9th International Workshop on Worst-Case Execution Time (WCET) Analysis, 2009. [pdf]  [slides]  [bib]
  14. Cache-Related Preemption Delay Computation for Set-Associative Caches—Pitfalls and Solutions
    C. Burguière, J. Reineke, and S. Altmeyer
    Proceedings of 9th International Workshop on Worst-Case Execution Time (WCET) Analysis, 2009. [pdf]  [slides]  [bib]
  15. Making Dynamic Memory Allocation Static To Support WCET Analyses
    J. Herter, and J. Reineke
    Proceedings of 9th International Workshop on Worst-Case Execution Time (WCET) Analysis, 2009. [pdf]  [slides]  [bib]
  16. A New Notion of Useful Cache Block to Improve the Bounds of Cache-Related Preemption Delay
    S. Altmeyer, and C. Burguière
    Proceedings of the 21st Euromicro Conference on Real-Time Systems (ECRTS '09), 2009. [doi]  [bib]
  17. An Abstraction-Aware Compiler for VHDL Models
    M. A. Maksoud, M. Pister, and M. Schlickling
    Proceedings of the International Conference on Computer Engineering and Systems (ICCES '09), 2009. [doi]  [bib]
  18. Improving Timing Analysis for Matlab Simulink/Stateflow
    L. Tan, B. Wachter, P. Lucas, and R. Wilhelm
    Proceedings of the 2nd International Workshop on Model Based Architecting and Construction of Embedded Systems (ACES-MB), 2009. [pdf]  [bib]
  19. Symbolic State Traversal for WCET Analysis
    S. Wilhelm, and B. Wachter
    International Conference on Embedded Software, 2009. [bib]
  20. Time-Bounded Model Checking of Infinite-State Continuous-Time Markov Chains
    E. M. Hahn, H. Hermanns, B. Wachter, and L. Zhang
    Fundamenta Informaticae, 95, 2009. [url]  [bib]
  21. The Worst-case Execution Time Problem—Overview of Methods and Survey of Tools
    R. Wilhelm, J. Engblom, A. Ermedahl, N. Holsti, S. Thesing, D. Whalley, G. Bernat, C. Ferdinand, R. Heckmann, T. Mitra, F. Mueller, I. Puaut, P. Puschner, J. Staschulat, and P. Stenström
    ACM Transactions on Embedded Computing Systems (TECS), 7 (3), 2008. [doi]  [bib]
  22. Probabilistic CEGAR
    H. Hermanns, B. Wachter, and L. Zhang
    CAV, 2008. [pdf]  [bib]
  23. Abstract Interpretation with Applications to Timing Validation
    R. Wilhelm, and B. Wachter
    CAV, 2008. [pdf]  [bib]
  24. Time-Bounded Model Checking of Infinite-State Continuous-Time Markov Chains
    L. Zhang, H. Hermanns, E. M. Hahn, and B. Wachter
    ACSD, 2008. [pdf]  [bib]
  25. Sensitivity of Cache Replacement Policies
    J. Reineke, and D. Grund
    Technical Report, SFB/TR 14 AVACS, 2008. [pdf]  [bib]
  26. Estimating the Performance of Cache Replacement Policies
    D. Grund, and J. Reineke
    MEMOCODE '08: Proceedings of the 6th IEEE/ACM International Conference on Formal Methods and Models for Codesign, 2008. [doi]  [pdf]  [slides]  [bib]
  27. Relative Competitiveness of Cache Replacement Policies
    J. Reineke, and D. Grund
    SIGMETRICS '08: Proceedings of the 2008 ACM SIGMETRICS international conference on Measurement and modeling of computer systems, 2008. [doi]  [pdf]  [bib]
  28. Relative Competitive Analysis of Cache Replacement Policies
    J. Reineke, and D. Grund
    LCTES '08: Proceedings of the 2008 ACM SIGPLAN-SIGBED conference on Languages, compilers, and tools for embedded systems, 2008. [doi]  [pdf]  [slides]  [bib]
  29. CAMA: Cache-Aware Memory Allocation for WCET Analysis
    J. Herter, J. Reineke, and R. Wilhelm
    Proceedings Work-In-Progress Session of the 20th Euromicro Conference on Real-Time Systems, 2008. [pdf]  [slides]  [bib]
  30. WCET Analysis for Preemptive Systems
    S. Altmeyer, and G. Gebhard
    Proceedings of the 8th International Workshop on Worst-Case Execution Time (WCET) Analysis, 2008. [bib]
  31. Parametric Timing Analysis for Complex Architectures
    S. Altmeyer, C. Hümbert, B. Lisper, and R. Wilhelm
    Procedeedings of the 14th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA'08), 2008. [bib]
  32. Caches in WCET Analysis
    J. Reineke
    Universität des Saarlandes, 2008. [pdf]  [slides]  [bib]
  33. Topology Analysis of Dynamic Communication Systems
    P. Backes
    Universität des Saarlandes, 2008. [bib]
  34. The Spotlight Principle: On Process-Summarizing State Abstractions
    B. Wachter, and B. Westphal
    Verification, Model Checking and Abstract Interpretation, 2007. [bib]
  35. New Developments in WCET Analysis
    C. Ferdinand, F. Martin, C. Cullmann, M. Schlickling, I. Stein, S. Thesing, and R. Heckmann
    Program Analysis and Compilation. Theory and Practice. Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday, Springer Verlag, 2007. [bib]
  36. A Framework for Static Analysis of VHDL Code
    M. Schlickling, and M. Pister
    Proceedings of 7th International Workshop on Worst-case Execution Time (WCET) Analysis, 2007. [ps]  [bib]
  37. Probabilistic Model Checking Modulo Theories
    B. Wachter, L. Zhang, and H. Hermanns
    Proceedings of the Fourth International Conference on the Quantitative Evaluation of Systems, 2007. [bib]
  38. Towards Symbolic State Traversal for Efficient WCET Analysis of Abstract Pipeline and Cache Models
    S. Wilhelm, and B. Wachter
    Proceedings of Seventh International Workshop on Worst-Case Execution Time Analysis, 2007. [pdf]  [bib]
  39. Timing Predictability of Cache Replacement Policies
    J. Reineke, D. Grund, C. Berg, and R. Wilhelm
    Real-Time Systems, 37 (2), 2007. [doi]  [pdf]  [slides]  [bib]
  40. On Probabilistic CEGAR
    H. Hermanns, B. Wachter, and L. Zhang
    Technical Report, SFB/TR 14 AVACS, 2007. [pdf]  [bib]
  41. Analysis of Dynamic Communicating Systems by Hierarchical Abstraction
    J. Bauer, and R. Wilhelm
    Technical Report, Dagstuhl, 2006. [pdf]  [bib]
  42. Specification and Verification of Dynamic Communication Systems
    J. Bauer, I. Schaefer, T. Toben, and B. Westphal
    Application of Concurrency to System Design, 2006. ACSD 2006. Sixth International Conference on, 2006. [pdf]  [bib]
  43. Automatic Identification of Timing Anomalies for Cycle-Accurate Worst-Case Execution Time Analysis
    J. Eisinger, I. Polian, B. Becker, A. Metzner, S. Thesing, and R. Wilhelm
    9th IEEE Workshop on Design \& Diagnostics of Electronic Circuits \& Systems (DDECS 2006), 2006. [bib]
  44. A Definition and Classification of Timing Anomalies
    J. Reineke, B. Wachter, S. Thesing, R. Wilhelm, I. Polian, J. Eisinger, and B. Becker
    Proceedings of 6th International Workshop on Worst-Case Execution Time (WCET) Analysis, 2006. [pdf]  [slides]  [bib]
  45. Determining Bounds on Execution Times
    R. Wilhelm
    Handbook on Embedded Systems, CRC Press, 2006. [bib]
  46. Explaining Data Type Reduction in the Shape Analysis Framework
    B. Wachter
    Workshop Trustworthy Software 2006, 2006. [bib]
  47. Analysis of Communication Topologies by Partner Abstraction
    J. Bauer
    Universität des Saarlandes, 2006. [bib]
  48. Predictability of Cache Replacement Policies
    J. Reineke, D. Grund, C. Berg, and R. Wilhelm
    Technical Report, SFB/TR 14 AVACS, 2006. [pdf]  [bib]
  49. Efficient Algorithms for Feasibility and Optimality
    W. Damm, A. Metzner, F. Eisenbrand, G. Shmonin, R. Wilhelm, and S. Winkel
    Proceedings of the 12th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA'06), 2006. [bib]
  50. Codegenerierung für CSP-OZ
    B. Franzen
    [bib]
  51. A Semantics for Procedure Local Heaps and its Abstractions
    N. Rinetzky, J. Bauer, T. Reps, M. Sagiv, and R. Wilhelm
    32nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'05), 2005. [pdf]  [bib]
  52. Timing Analysis and Timing Predictability
    R. Wilhelm
    FMCO 2004, 2005. [bib]
  53. Component-Wise Instruction-Cache Behavior Prediction
    A. Rakib, O. Parshin, S. Thesing, and R. Wilhelm
    ATVA 2004, 2004. [bib]
  54. Static Program Analysis via 3-Valued Logic
    T. Reps, S. Sagiv, and R. Wilhelm
    CAV 2004, 2004. [bib]
  55. A Semantics for Procedure Local Heaps and its Abstractions
    N. Rinetzky, J. Bauer, T. Reps, M. Sagiv, and R. Wilhelm
    Technical Report, AVACS, 2004. [pdf]  [bib]
  56. Design for Timing Predictability
    L. Thiele, and R. Wilhelm
    Real-Time Systems, 28, 2004. [bib]
  57. Why AI + ILP is Good for WCET, But MC Is Not, Nor ILP Alone
    R. Wilhelm
    VMCAI 2004, 2004. [url]  [bib]

More Information

If you are interested in more information on AVACS or the different subprojects, please visit www.avacs.org.