Thèse de Doctorat école doctorale sciences pour l’ingénieur et microtechniques U N I V E R S I T É D E F R A N C H E - C O M T É ◦ N 6 6 6 THE`SE pre´sente´e par VINCENT HUGOT pour obtenir le Grade de Docteur de l’Universite´ de Franche-Comte´ Spe´cialite´ : Informatique Tree Automata, Approximations, and Constraints for Verification Tree (Not-Quite) Regular Model-Checking Soutenue publiquement le 27 Septembre 2013 devant le Jury compose´ de : PHILIPPE SCHNOEBELEN Rapporteur Directeurderecherche,CNRS JEAN-MARC TALBOT Rapporteur Professeura` l’Universite´ d’Aix-Marseille PIERRE-CYRILLE HE´AM Co-Directeur Professeura` l’Universite´ deFranche-Comte´ OLGA KOUCHNARENKO Directeur de the`se Professeura` l’Universite´ deFranche-Comte´ FLORENT JACQUEMARD Examinateur Charge´ derechercheHDR,INRIA JEAN-FRANC¸OIS RASKIN Examinateur Professeura` l’Universite´ libredeBruxelles SOPHIE TISON Examinateur Professeura` l’Universite´ deLille 2 Version of the document: d361, dated 2013-12-30 05:08:42+01:00 , compiled on December 30, 2013. Table of Contents I Motivations and Preliminaries 8 1 Formal Tools for Verification 9 1.1 Model-Checking: Simple, Symbolic & Bounded . . . . . . . . . . . . 10 1.2 Regular Model-Checking. . . . . . . . . . . . . . . . . . . . . . . . . . 13 1.3 Tree Automata in Verification . . . . . . . . . . . . . . . . . . . . . . . 16 1.4 Outline and Contributions . . . . . . . . . . . . . . . . . . . . . . . . . 19 2 Some Technical Preliminaries 22 2.1 Pervasive Notions and Notations . . . . . . . . . . . . . . . . . . . . . 23 2.2 Ranked Alphabets, Terms, and Trees . . . . . . . . . . . . . . . . . . . 24 2.3 Term Rewriting Systems . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2.4 Bottom-Up Tree Automata . . . . . . . . . . . . . . . . . . . . . . . . . 30 2.5 Tree Automata With Global Constraints . . . . . . . . . . . . . . . . . 35 2.6 Decision Problems and Complexities . . . . . . . . . . . . . . . . . . . 37 II Approximating LTL over Rewrite Sequences 40 3 Term Rewriting for Model-Checking 41 3.1 On the Usefulness of Rewriting for Verification . . . . . . . . . . . . 42 3.2 Reachability Analysis for Term Rewriting . . . . . . . . . . . . . . . . 44 3.2.1 Preservation of Regularity Through Forward Closure . . . . . 45 3.2.2 Tree Automata Completion Algorithm . . . . . . . . . . . . . 46 3.2.3 Exact Behaviours of Completion . . . . . . . . . . . . . . . . . 47 3.2.4 One-Step Rewriting, and Completion . . . . . . . . . . . . . . 47 3.2.5 The Importance of Being Left-Linear . . . . . . . . . . . . . . 49 3.2.6 One-Step Rewriting, and Constraints . . . . . . . . . . . . . . 51 4 Approximating LTL on Rewrite Sequences 53 4.1 Preliminaries & Problem Statement . . . . . . . . . . . . . . . . . . . 56 4.1.1 Rewrite Words & Maximal Rewrite Words . . . . . . . . . . . 56 4.1.2 Defining Temporal Semantics on Rewrite Words. . . . . . . . 57 4.1.3 Rewrite Propositions & Problem Statement . . . . . . . . . . . 58 4.2 Technical Groundwork: Antecedent Signatures . . . . . . . . . . . . . 59 4.2.1 Overview & Intuitions . . . . . . . . . . . . . . . . . . . . . . . 59 4.2.2 Choosing a Suitable Fragment of LTL . . . . . . . . . . . . . . 61 4.2.3 Girdling the Future: Signatures. . . . . . . . . . . . . . . . . . 62 4.3 From Temporal Properties to Rewrite Propositions . . . . . . . . . . 73 4.4 Generating an Approximated Procedure . . . . . . . . . . . . . . . . 87 4.4.1 Juggling Assumptions and Expressive Power . . . . . . . . . 87 3 4 TABLE OF CONTENTS 4.4.2 Optimisation of Rewrite Propositions . . . . . . . . . . . . . . 95 4.5 Examples & Discussion of Applicability . . . . . . . . . . . . . . . . . 97 4.5.1 Examples: Three Derivations . . . . . . . . . . . . . . . . . . . 97 4.5.2 Coverage of Temporal Specification Patterns . . . . . . . . . . 101 4.5.3 Encodings: Java Byte-Code, Needham–Schroeder & CCS . . . 102 4.6 Conclusions & Perspectives . . . . . . . . . . . . . . . . . . . . . . . . 104 III Decision Problems for Tree Automata with Global Constraints 106 5 A Brief History of Constraints 107 5.1 Tree Automata With Positional Constraints . . . . . . . . . . . . . . . 107 5.1.1 The Original Proposal . . . . . . . . . . . . . . . . . . . . . . . 108 5.1.2 A Stable Superclass With Propositional Constraints . . . . . . 109 5.1.3 Constraints Between Brothers . . . . . . . . . . . . . . . . . . . 109 5.1.4 Reduction Automata . . . . . . . . . . . . . . . . . . . . . . . . 110 5.1.5 Reduction Automata Between Brothers . . . . . . . . . . . . . 111 5.2 Tree Automata With Global Constraints . . . . . . . . . . . . . . . . . 111 5.2.1 Generalisation to Propositional Constraints and More . . . . 112 5.2.2 Rigid Tree Automata . . . . . . . . . . . . . . . . . . . . . . . . 113 5.3 Synthetic Taxonomy of Automata With Constraints . . . . . . . . . . 114 5.4 Notations: Modification of an Automaton . . . . . . . . . . . . . . . . 115 6 Bounding the Number of Constraints 117 6.1 The Emptiness & Finiteness Problems . . . . . . . . . . . . . . . . . . 118 6.2 The Membership Problem . . . . . . . . . . . . . . . . . . . . . . . . . 121 6.3 A Strict Hierarchy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 126 6.4 Summary and Conclusions . . . . . . . . . . . . . . . . . . . . . . . . 128 7 SAT Encodings for TAGED Membership 129 7.1 Propositional Encoding. . . . . . . . . . . . . . . . . . . . . . . . . . . 130 7.2 Complexity and Optimisations . . . . . . . . . . . . . . . . . . . . . . 135 7.3 Implementation and Experiments . . . . . . . . . . . . . . . . . . . . 136 7.3.1 Experimental Results . . . . . . . . . . . . . . . . . . . . . . . . 137 7.3.2 The Tool: Inputs and Outputs . . . . . . . . . . . . . . . . . . 138 7.4 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 139 IV Decision Problems for Tree-Walking Automata 142 8 Tree Automata for XML 143 8.1 Tree-Walking Automata . . . . . . . . . . . . . . . . . . . . . . . . . . 144 8.2 Abstracting Away Unranked Trees . . . . . . . . . . . . . . . . . . . . 148 8.2.1 Unranked Trees and Their Automata . . . . . . . . . . . . . . 148 8.2.2 Document Type Definitions (DTD) . . . . . . . . . . . . . . . . 151 8.2.3 Binarisation of Trees and Automata . . . . . . . . . . . . . . . 152 8.3 Queries, Path Expressions, and Their Automata . . . . . . . . . . . . 155 8.3.1 Logic-based Queries . . . . . . . . . . . . . . . . . . . . . . . . 156 8.3.2 (Core) XPath: a Navigational Language . . . . . . . . . . . . . 157 8.3.3 Caterpillar Expressions . . . . . . . . . . . . . . . . . . . . . . 160 TABLE OF CONTENTS 5 8.4 The Families of Tree-Walking Automata . . . . . . . . . . . . . . . . . 162 8.4.1 Basic Tree-Walking Automata . . . . . . . . . . . . . . . . . . . 163 8.4.2 Nested Tree-Walking Automata . . . . . . . . . . . . . . . . . 164 9 Loops and Overloops: Effects on Complexity 165 9.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 166 9.2 Loops, Overloops and the Membership Problem . . . . . . . . . . . . 167 9.2.1 Defining, Classifying and Computing Loops . . . . . . . . . . 167 9.2.2 A Direct Application of Loops to Membership Testing . . . . 170 9.2.3 From Loops to Overloops . . . . . . . . . . . . . . . . . . . . . 172 9.3 Transforming TWA into equivalent BUTA . . . . . . . . . . . . . . . . 174 9.3.1 Two Variants: Loops and Overloops . . . . . . . . . . . . . . . 175 9.3.2 Overloops: Deterministic Size Upper-Bound . . . . . . . . . . 177 9.4 A Polynomial Over-Approximation for Emptiness . . . . . . . . . . . 179 9.5 Experimental Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . 181 9.5.1 Evaluating the Approximation’s Effectiveness . . . . . . . . . 181 9.5.2 Overloops Yield Smaller BUTA . . . . . . . . . . . . . . . . . . 182 9.5.3 Demonstration Software . . . . . . . . . . . . . . . . . . . . . . 183 9.6 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 184 V Summary and Perspectives 186 10 Summary and Future Works 187 10.1 Summary of Contributions . . . . . . . . . . . . . . . . . . . . . . . . 187 10.2 Future Works & Perspectives . . . . . . . . . . . . . . . . . . . . . . . 188 11 Appendix 191 11.1 More Relatives of Automata With Constraints . . . . . . . . . . . . . 191 11.1.1 Directed Acyclic Ordered Graph Automata . . . . . . . . . . . 191 11.1.2 Tree Automata With One Memory . . . . . . . . . . . . . . . . 193 11.2 More Relatives of Tree-Walking Automata. . . . . . . . . . . . . . . . 196 11.2.1 Tree-Walking Pebble Automata . . . . . . . . . . . . . . . . . . 196 11.2.2 Tree-Walking Invisible Pebble Automata . . . . . . . . . . . . 197 11.2.3 Tree-Walking Marbles Automata . . . . . . . . . . . . . . . . . 198 11.2.4 Tree-Walking Set-Pebble Automata . . . . . . . . . . . . . . . 199 11.2.5 Alternating Tree-Walking Automata . . . . . . . . . . . . . . . 199 12 [FR] Résumé en français 200 12.1 Approximation de LTL sur réécriture . . . . . . . . . . . . . . . . . . 202 12.2 Problèmes de décisions pour automates à contraintes . . . . . . . . . 206 12.3 Problèmes de décision pour les automates cheminants . . . . . . . . 208 List of Figures 1.1 Tree representation of “Star Trek” XML document. . . . . . . . . . . 18 2.1 Reading dependencies between chapters. . . . . . . . . . . . . . . . . 23 2.2 Automata, their closure properties and decision complexities. . . . . 38 2.3 Decision problems: inputs and outputs. . . . . . . . . . . . . . . . . . 39 3.1 Executions of a rewrite system satisfying (cid:3)(X ⇒ •Y). . . . . . . . . . 42 3.2 Forward-closure regularity-preserving classes of TRS. . . . . . . . . . 46 4.1 LTL semantics on maximal rewrite words. . . . . . . . . . . . . . . . 58 4.2 Building signatures on A-LTL. . . . . . . . . . . . . . . . . . . . . . . 73 4.3 Partially supported patterns from [Dwyer, Avrunin & Corbett, 1999]. 101 5.1 A taxonomy of automata, with or without constraints. . . . . . . . . 116 6.1 Reduction of intersection-emptiness: the language. . . . . . . . . . . 120 6.2 Housings: affecting a similarity classes to each group. . . . . . . . . 123 7.1 CNF solving time, laboratory example. . . . . . . . . . . . . . . . . . 137 7.2 CNF solving time, L=, for accepted and rejected terms. . . . . . . . . 138 7.3 Input syntax of the membership tool: automaton and term. . . . . . 139 7.4 Example LATEX output of the tool – cf. Fig. 7.3[p139]. . . . . . . . . . . 140 9.1 Uniform random TWA: emptiness tests. . . . . . . . . . . . . . . . . . 182 9.2 Uniform random TWA: size results. . . . . . . . . . . . . . . . . . . . 183 11.1 TA1M: capabilities of transitions in the literature. . . . . . . . . . . . 194 12.1 [3.1 ] Exécutions d’un système de réécriture satisfaisant (cid:3)(X ⇒ •Y).203 [p42] 6 LIST OF FIGURES 7 — Part I — Motivations and Preliminaries 8 Chapter 1 Formal Tools for Verification Contents 1.1 Model-Checking: Simple,Symbolic&Bounded . . . . . . . . . 10 1.2 RegularModel-Checking . . . . . . . . . . . . . . . . . . . . . . . 13 1.3 TreeAutomatainVerification . . . . . . . . . . . . . . . . . . . . 16 1.4 OutlineandContributions . . . . . . . . . . . . . . . . . . . . . . 19 —Where we are reminded that bugs are bad, and that formal methods are good. Ariane 5’s 1996 maiden flight “501”enjoysthedubiousdistinctionofbeing remembered as one of the most expensive fireworks displays in the history of mankind. Yet its most striking feature lies not in the spectacular character of the failure, but in how it came to pass. The cause was not a structural flaw of the rocket, but a software bug. The ruinous error lay in a single line of Ada code in the inertial navigation system, a fairly simple conversion from 64-bit to 16-bit that should have checked for overflows but did not. Misled by erroneous navigation data, the rocket veered hopelessly off course, and self-destructed. There may be imponderables in rocket design, but that was not one of them. The range check had actually been deliberately deactivated for this conversion, as a performance optimisation made under the belief that there was an ample margin of error. This may have been true for Ariane 4, from which the navigation system was copied directly, but the greater acceleration of Ariane 5 turned out to be beyond the scope of the 16-bit variable. Not all individual software bugs cost a few hundred million to one billion dollars – as did flight 501 – but they are pervasive and the costs accrue over time. However, there is no intrinsic difference between (mostly) harmless, everyday bugs and catastrophic ones, as a quick look at some of the most publicised incidents shows. Similar to the Ariane 5 incident is the loss of the Mariner I space probe in 1962: TheCostofSoftwareBugs an error in some rarely-used part of the navigation software of the Atlas-Agena A study conducted by the rocket resulted in the unrecoverable failure of its guidance system. The Phobos NIST in 2002 concluded I probe on the other hand was launched successfully in 1988, but a malformed that software bugs cost command sent from earth forced the unexpected execution of a test routine that the US economy about $59 billion each year, or wassupposedtobedeadcode. Theyear1999sawthelossoftwoprobestosoftware about 0.6% of the GDP. A errors: the Mars Climate Orbiter likely disintegrated in Mars’s atmosphere because 2013 Cambridge University study estimated a global the ground-control computer was using imperial units while the probe itself used annual cost of $312 bil- metric units; the Mars Polar Lander nearly made it to the ground, but invalid lion...for the constant de- buggingactivityalone. touchdowndetectionlogicpromptedittocutthrusters40metersabovetheground. After a decade of loyal services, the Mars Global Surveyor was lost in 2006 because of an error causing data to be written in the wrong memory address. 9 10 Part I. Chapter 1. Formal Tools for Verification In the medical domain, the Therac-25 radiation therapy machine is infamous for having killed three patients and balefully irradiated at least three others between 1985 and 1987. Its predecessor, the Therac-20, used a mechanical safety interlock that prevented the high-powered electron beam from being used directly. The Therac-25 used a software interlock instead, which a race condition could disable if the machine’s operator was fast enough. Another race condition, this time in the alarm routines of a XA/21 energy management system, escalated what was a minor power failure into the USA & Canada Northeast blackout of 2003, depriving 55 million people of electricity for up to two days. In 1991, a MIM-104 Patriot anti-ballistic battery correctly detected an incoming Al-Hussein missile, but after 100hoursinoperation,cumulativeroundingerrorshadcauseditsinternalsoftware clock to drift by one third of a second; using this erroneous time to predict the missile’s trajectory yielded an error of about 600 meters. Unopposed, the missile hit its mark, killing 28 soldiers. Range checks, race conditions, access to dead code, dimensional clashes, clock TotalRecall synchronisation problems... Despite their dramatic consequences, those are all In 2010, Toyota recalled 133000 Prius hybrids and perfectly mundane bugs of the same kinds that plague desktop computers on a 14500 Lexus hybrids. In daily basis, from word processors to card games. But when software controls 2004–05, Mercedes recalled almost two million SL500 rockets, missiles, or any sort of critical equipment, bugs are more than mere and E-Class vehicles. Both annoyances. Increasingly, sophisticated software replaces simpler mechanical cases were warranted by faults in the braking soft- systems and specialised circuits. Embedded systems are everywhere, from pocket ware. watches to microwave ovens to phones to cars to planes to rockets. But regardless of what it is that the software controls, preventing, handling and fixing bugs is not rocket science, but computer science. There are many approaches dedicated to the end-goal of reliable software; this verification thesis only concerns itself with the field of verification (or formal methods), whose formalmethods aims can be broadly defined as proving that a given piece of software or hardware is correct with respect to a given specification. The rise of embedded systems not only makes such methods more necessary than ever, but also contributes to create a “target-rich” environment for the field. The high cost of formal methods is indeed offset by the much higher cost of bugs in embedded systems: even if a bug is caught in time and causes no damage, recalling and fixing entire lines of products is prohibitively expensive. Furthermore, embedded systems are often smaller and more specialised than modern desktop software, which makes them easier to specify and to check. Thus the current technological advances provide a strong impetus for software verification. That field is quite vast, however; this chapter provides a very succinct and mostly informal overview of the techniques and traditions within which our work is inscribed. 1.1 Model-Checking: Simple, Symbolic & Bounded Hoarelogic One of the first approaches to program verification is Hoare logic, introduced in [Hoare, 1969] and further refined by many other researchers, notably Floyd and Dijkstra. The basic idea is to enclose a program code C between two assertions p