Stephan Merz

Formal specification and verification

Introduction

Beyond his seminal contributions to the theory and the design of concurrent and distributed algorithms, Leslie Lamport has throughout his career worked on methods and formalisms for rigorously establishing the correctness of algorithms. Commenting on his first article about a method for proving the correctness of multi-process programs [START_REF] Lamport | Proving the correctness of multiprocess programs[END_REF] on the website providing access to his collected writings [START_REF] Lamport | My writings[END_REF], Lamport recalls that this interest originated in his submitting a flawed mutual-exclusion algorithm in the early 1970s. As a trained mathematician, Lamport is perfectly familiar with mathematical set theory, the standard formal foundation of classical mathematics. His career in industrial research environments and the fact that his main interest has been in algorithms, not formalisms, has certainly contributed to his designing reasoning methods that combine pragmatism and mathematical elegance. The methods that he designed have always been grounded in the semantics of programs and their executions rather than being driven by the syntax in which these programs are expressed, in contrast to many methods advocated by "pure" computer scientists.

The famous "Time/Clocks" paper [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] describes executions of distributed state machines and introduces the happened-before or causality relation, a partial order on the events occurring in runs. The "philosophically correct" way for reasoning about distributed executions would thus appear to be based on a partial ordering between operations. Indeed, Lamport explored this idea and proposed a method based on two relations called precedes and may affect [START_REF] Lamport | A new approach to proving the correctness of multiprocess programs[END_REF]. This method can notably be applied to algorithms that involve non-atomic operations, such as the Bakery algorithm. However, Lamport felt that the method did not scale well, unlike assertional reasoning about global states of systems as viewed by an idealized external observer, even if no single process can observe them. This style of reasoning considers linearizations of distributed executions, and it generally requires algorithms to be described in terms of their atomic operations (an exception being [START_REF] Lamport | win and sin: Predicate transformers for concurrency[END_REF]). The notion of an overall system invariant that is preserved by every operation plays a central role in this approach: such an invariant explains why the algorithm is correct. Assertional proofs have since been demonstrated to be completely rigorous, to be amenable to mechanized checking, and to scale well. [START_REF] Abadi | The existence of refinement mappings[END_REF] Lamport realized that there are two fundamental classes of correctness properties that arise in the verification of concurrent algorithms, for which he coined the terms safety and liveness properties [START_REF] Lamport | Proving the correctness of multiprocess programs[END_REF]. Generalizing, respectively, partial correctness and termination of sequential programs, safety properties assert that "nothing bad ever happens", and liveness properties require that "something good happens eventually." These intuitive concepts were later formalized by Alpern and Schneider [START_REF] Alpern | Defining liveness[END_REF] who showed that any property of runs can be expressed as the intersection of a safety property and a liveness property. Although proofs of liveness properties generally rely on auxiliary invariants, the basic principles for proving safety and liveness properties are different, and the two are therefore best considered separately.

Lamport advocates describing algorithms in terms of state machines whose operations are atomic. Invariants, and more generally safety properties, are then established by induction: the invariant holds in all possible initial states and is preserved by every operation of the state machine. The proof of liveness properties usually relies on associating a measure with the states of the algorithm and showing that the measure decreases with every step as long as the "good state" has not been reached. This argument is made formal through the use of well-founded orderings, which do not admit infinite decreasing chains. A direct application of that proof principle would require fixing a scheduler that governs the execution of different processes-an undesirable requirement since one wants to establish the correctness of the algorithm for any "reasonable" scheduler. A useful generalization requires that as long as the target state has not been reached, no step of the algorithm increases the measure, "helpful" steps decrease the measure, and some helpful step will eventually be executed. In order to justify the latter (which in itself is a liveness property!), one invokes fairness assumptions [START_REF] Attie | Fairness and hyperfairness in multi-party interactions[END_REF][START_REF] Lamport | Fairness and hyperfairness[END_REF] that assert that executable operations will not be neglected forever, fixing the precise understanding of a "reasonable" scheduler for the particular application.

Another fundamental concept underlying the rigorous development and proof of concurrent algorithms advocated by Lamport is that of refinement. It allows a designer to describe the fundamental correctness properties using a high-level (possibly centralized) state machine and then prove that another state machine whose description is given at a lower level of abstraction faithfully implements the high-level description. For example, a high-level state machine describing a consensus algorithm [START_REF] Lamport | The byzantine generals problem[END_REF] could have a variable chosen holding a set of values, initialized to the empty set, a Choose operation that assigns chosen to the singleton set {v } for some value v among the proposed values, and Decide operations that set the decision values of each process to that chosen value. A lower-level refinement would then describe the actual algorithm in terms of exchanged messages and votes. A technical complication in that approach is that the lower-level state machine will have operations that modify only low-level variables, i.e., variables that do not exist at the higher level of abstraction. These operations cannot be mapped to operations of the high-level state machine. For example, operations that send messages in the putative Consensus algorithm have no meaning in the high-level specifi-cation. Lamport advocates that formalisms for describing executions of state machines should be insensitive to stuttering steps that leave unchanged the state visible to the specification.

The remainder of this chapter will focus on the Temporal Logic of Actions TLA and the specification language TLA + . These are Lamport's contributions to the formal specification and verification of algorithms that have had the greatest impact in the academic community and in industry, and their design was guided by the principles outlined above.

The Temporal Logic of Actions

Temporal logic [START_REF] Prior | Past, Present and Future[END_REF] is a branch of modal logic in which the accessibility relation corresponds to temporal succession. During the 1970s, several authors [START_REF] Burstall | Program proving as hand simulation with a little induction[END_REF][START_REF] Kröger | LAR: A logic of algorithmic reasoning[END_REF] suggested adopting temporal logic as a basis for proving programs correct. Pnueli's influential paper [START_REF] Pnueli | The temporal logic of programs[END_REF] provided the insight that temporal logic is particularly useful for specifying and reasoning about reactive systems, which include concurrent and distributed systems. A generalization of Pnueli's logic that is based on the "next" and "until" connectives remains the standard variant of linear-time temporal logic used in computer science to this day.

The Genesis of TLA

In 1977, Lamport proposed a method for proving the correctness of concurrent programs [START_REF] Lamport | Proving the correctness of multiprocess programs[END_REF]. It used invariant reasoning (based on Floyd's method [START_REF] Floyd | Assigning meanings to programs[END_REF]) for establishing safety properties and lattices of leads-to properties for proving liveness. The method relied on a fixed progress assumption for each process in order to establish elementary leads-to properties. Lamport was introduced to temporal logic in the late 1970s during a seminar organized by Susan Owicki at Stanford University. At that time, the distinction between linear-time and branching-time temporal logics was not yet clearly established in computer science. Lamport clarified this difference [START_REF] Lamport | Sometime" is sometimes "not never" -on the temporal logic of programs[END_REF] and showed that the expressive powers of LTL and CTL are incomparable. He quickly realized that temporal logic was a convenient language for expressing and reasoning about fairness and liveness properties. For example, weak and strong fairness of executions with respect to an action α, representing an operation of a process in a concurrent system, can be written as

2(2en(α) ⇒ 3exec(α)) and 2(23en(α) ⇒ 3exec(α)).
In these formulas, the predicate en(α) characterizes those states in which α is enabled (may be executed), exec(α) is true when action α has been executed, and 2 and 3 are the "always" and "eventually" operators of LTL. Weak fairness requires that an action cannot remain perpetually enabled without eventually being executed. Strong fairness requires that even an action that is infinitely often (but perhaps not perpetually) enabled must eventually be executed. Using such formulas, more general fairness hypotheses than uniform progress of processes considered in [START_REF] Lamport | Proving the correctness of multiprocess programs[END_REF] can be expressed unambiguously. Moreover, the principles of reasoning about leads-to lattices could be derived from the general proof rules of temporal logic. A joint paper with Owicki [START_REF] Owicki | Proving liveness properties of concurrent programs[END_REF] develops these ideas into a full-fledged method for proving the correctness of concurrent programs. In the introduction to this paper, the authors write:

While we hope that logicians will find this work interesting, our goal is to define a method that programmers will find useful.

This motto describes well Lamport's approach to formalisms for specification and verification. Whereas standard LTL was clearly useful for expressing fairness and liveness properties, Lamport felt that it was not convenient for writing complete specifications of actual systems. His intuition was confirmed when he observed colleagues at SRI struggling with specifying a FIFO queue in Pnueli's temporal logic. (It was later proved that this is actually impossible unless one assumes that the input values presented to the queue were unique.) This observation led his colleagues to introduce a more expressive temporal logic based on intervals [START_REF] Schwartz | An interval-based temporal logic[END_REF]. In contrast, Lamport concluded that the fundamental problem was the "property-oriented" style of specifications as a list (conjunction) of properties observed at the interface of a system, such as the inputs and outputs of the queue, but excluding any reference to internal system states. He designed TLA as a logic geared towards specifying and reasoning about state machines, based on a few orthogonal and simple concepts that provide a higher level of abstraction (and elegance!) than the use of a pseudo-programming language, as in the earlier paper with Owicki [START_REF] Owicki | Proving liveness properties of concurrent programs[END_REF].

The Logic TLA

Lamport designed TLA around 1990 [START_REF] Lamport | The Temporal Logic of Actions[END_REF][START_REF] Lamport | The temporal logic of actions[END_REF]. TLA formulas are built from constants, whose values are fixed throughout an execution, and (state) variables. We use x , y, z to denote constants and u, v , w to denote variables. A state is a mapping from variables to values. TLA distinguishes three levels of expressions:

• The syntax of state functions and state predicates is that of standard terms and formulas of first-order logic. Concrete examples of state predicates are v ≥ 0 or ∃x : x ∈ u ∧ x / ∈ v . Semantically, they are interpreted over individual states. 1• Transition functions and transition predicates, also called actions, are first-order terms and formulas that may contain both standard (unprimed) variables u, v , w and primed variables u , v , w . Examples are u ∈ v or ∃x : u + x = v . Semantically, transition formulas are interpreted over pairs s, t of states, with unprimed variables being interpreted in state s and primed variables in t.

• Temporal formulas are built from state and transition formulas by applying operators of temporal logic according to the rules given below. They are interpreted over behaviors, i.e., sequences σ = s 0 , s 1 , . . . of states.

Whereas standard LTL builds temporal formulas solely from state formulas, the introduction of transition formulas as a primitive building block is fundamental to specifying state machines. For example, the LTL equivalent to the TLA action u ∈ v would be

∃x : x ∈ v ∧ c (u = x )
where c denotes LTL's next-time operator. Rather than using a pseudo-programming notation as in [START_REF] Owicki | Proving liveness properties of concurrent programs[END_REF], actions are just first-order formulas over primed and unprimed variables. One reasons about them using ordinary mathematical logic, rather than special principles for reasoning about programs. At the temporal level, any formula can be considered as a system specification or as a property. There is no formal distinction between the two, and reasoning about them relies on the same fundamental principles of temporal logic.

TLA introduces several notations at the levels of state and transition formulas. Given a state formula e, the transition formula e is obtained by replacing all (free) occurrences of state variables by their primed counterparts. Semantically, e denotes the value of e at the second state of the pair of states at which e is evaluated. The action UNCHANGED e is shorthand for e = e. For an action A and a state formula e, the actions [A] e and A e stand for A ∨ e = e and A ∧ e = e, respectively. The action formula [A] e represents closure of A under stuttering (with respect to e), in particular it is true of a pair of states s, t if A is true or if s = t. Dually, A e requires A to be true and the step from state s to state t to be observable through a change of e. Finally, the state predicate ENABLED A is obtained by existential quantification over all primed state variables that occur in the action A. For example, 2 if

A ∆ = v > 0 ∧ v = v -1 ∧ w = w then ENABLED A ∆ = ∃v , w : v > 0 ∧ v = v -1 ∧ w = w
It is easy to see that for this example, ENABLED A is logically equivalent to the predicate v > 0. In general, ENABLED A is true at state s if there exists some state t such that A holds for the pair s, t .

Formulas at all three levels are closed under Boolean operators (¬, ∧, ∨, ⇒, ≡) and firstorder quantifiers (∀, ∃). The rules for forming temporal formulas are as follows:

• Every state predicate is a temporal formula.

• If A is an action and e is a state formula then 2[A] e is a temporal formula.

• If ϕ is a temporal formula then so is 2ϕ. 2 The symbol ∆ = denotes "is defined as".

STL1

.

ϕ 2ϕ STL4. ϕ ⇒ ψ 2ϕ ⇒ 2ψ STL2. 2ϕ ⇒ ϕ STL5. 2(ϕ ∧ ψ) ≡ 2ϕ ∧ 2ψ STL3. 22ϕ ≡ 2ϕ STL6. 32(ϕ ∧ ψ) ≡ 32ϕ ∧ 32ψ
TLA1.

P ∧ e = e ⇒ P 2P ≡ P ∧ 2[P ⇒ P ] e TLA2.

P ∧

[A] e ⇒ Q ∧ [B ] f 2P ∧ 2[A] e ⇒ 2Q ∧ 2[B ] f Lattice.
(S , ≺) is a well-founded ordering ∀x ∈ S : ϕ(x ) ; (ψ ∨ ∃y ∈ S : y ≺ x ∧ ϕ(y))

(∃x ∈ S : ϕ(x )) ; ψ • If ϕ is a temporal formula, x is a constant, and v is a variable, then ∃x : ϕ and ∃ ∃ ∃ ∃ ∃ ∃ v : ϕ are temporal formulas.

The formulas 3ϕ and 3 A e are shorthand for ¬2¬ϕ and ¬2[¬A] e , respectively. Also, ϕ ; ψ ("ϕ leadsto ψ") abbreviates 2(ϕ ⇒ 3ψ). Observe in particular that if A is an action formula, 2A is in general not well-formed: actions need to be "protected" by square or angle brackets inside temporal formulas.

The operators 2 and 3 are the familar "always" and "eventually" operators of LTL: 2ϕ is true of σ if ϕ is true of every suffix of σ. The formula 2[A] e is true of σ = s 0 , s 1 , . . . if, for all n ∈ N, the action A holds of the state pair s n , s n+1 or the state formula e evaluates to the same value in s n and s n+1 , and the interpretation of 3 A e is dual. The syntactic restriction of allowing action formulas to appear only inside brackets ensures that all temporal formulas ϕ of TLA are insensitive to finite stuttering: if two state sequences σ and τ agree up to insertions or removals of finite repetitions of states then ϕ is true of σ if and only if

ϕ is true of τ. The formula ∃ ∃ ∃ ∃ ∃ ∃ v : ϕ is true of σ = s 0 , s 1 , . . . if ϕ is true of a sequence τ = t 0 , t 1 , .
. . such that for all n, s n and t n agree on the values of all variables except possible v . The formal definition is somewhat more complicated in order to preserve invariance under stuttering [START_REF] Lamport | The temporal logic of actions[END_REF].

The notion of validity of TLA formulas is standard. In particular, a temporal formula ϕ is valid if it is true of all behaviors. Lamport also provides a set of proof rules for TLA. In particular, he states that the proof rules reproduced in Figure 1, plus ordinary first-order reasoning, are sufficient (in the sense of relative completeness [START_REF] Apt | Ten years of Hoare's logic: A survey -part 1[END_REF]) for reasoning about algorithms specified in TLA without quantification over state variables. These rules should be read as asserting that if the hypotheses are valid, then so is the conclusion. For example, rule (STL1) is the well-known necessitation rule of modal logic, and it is justified because any suffix of a behavior is again a behavior, of which ϕ is true by the hypothesis of the rule. Of course, the implication ϕ ⇒ 2ϕ is not valid in general. From the elementary rules of Figure 1, further useful verification rules can be derived such as the following rule for proving that a state predicate P is an invariant of a system specification

INV1. P ∧ [A] e ⇒ P P ∧ 2[A] e ⇒ 2P
This rule, like most other rules for system verification in TLA, establishes a conclusion expressed in temporal logic from non-temporal (action-level) hypotheses. In this way, reasoning at the temporal level is confined to the top levels of a TLA proof and typically represents less than 5% of the proof steps. In particular, reasoning about safety properties does not involve temporal logic.

Lamport's rules are intended for the verification of algorithms. In contrast, providing a proof system for-even propositional-TLA that is complete in the standard sense of formal logic (i.e., that allows all valid formulas to be derived as theorems) is more delicate. In particular, whereas (INV1) is sufficient for proving invariants of systems, the general induction axiom of LTL

2(ϕ ⇒ c ϕ) ⇒ (ϕ ⇒ 2ϕ)
cannot be expressed in TLA because there is no next-time operator that could be applied to temporal formulas. A generalization of TLA, together with a system of rules that is complete for the propositional fragment of that logic, appears in [START_REF] Merz | A more complete TLA[END_REF].

Refinement, Hiding, and Composition

We mentioned above that TLA does not formally distinguish between system specifications and their properties: both are represented as temporal formulas. In practice, specifications of state machines are usually written in the form

Init ∧ 2[ Next ] v ∧ L (1)
where the state predicate Init specifies the possible initial states of the system, the action Next its next-state relation, v is the tuple of all state variables used in the specification, and L expresses fairness conditions. Typically, Next is a disjunction of actions A i that describe atomic transitions of the system or of its environment, and L is a conjunction of strong or weak fairness conditions on (some of) the actions A i .

Refinement of specifications. Perhaps influenced by ideas on program refinement developed by Back and Morgan [START_REF] Back | On correct refinement of programs[END_REF][START_REF] Morgan | Programming from specifications[END_REF], ultimately inspired by Dijkstra [START_REF] Dijkstra | A Discipline of Programming[END_REF], Lamport [START_REF] Lamport | What good is temporal logic?[END_REF] already observes that "temporal logic supports hierarchical specification and reasoning in a simple, natural way". He also notes that the essential ingredient for this to be possible is the invariance of temporal logic formulas under stuttering, ensured by the absence of a next-time operator. The idea is that a refinement R of a high-level specification S introduces implementation detail, represented by additional state variables. Newly introduced actions that modify solely these new variables correspond to stuttering steps at the level of S and, by stuttering invariance, cannot invalidate S . Actions that modify the variables present in S must do so in ways that are allowed by (the next-state relation of) S . Whereas R may have fewer behaviors (when projected to the state space of S ), the fairness conditions in S must be preserved: if a high-level action A i for which S states a fairness condition is sufficiently often enabled in a run, R must ensure that some action whose effect corresponds to the occurrence of A i will eventually occur in that run. Summing up, R refines S if and only if the implication R ⇒ S is valid. Assuming that R and S are specified using formulas of shape (1) (with superscripts R and S ), refinement is proved by finding a state predicate I such that all of the following implications hold:

Init R ⇒ I ∧ Init S I ∧ [ Next R ] v R ⇒ I ∧ [ Next S ] v S 2I ∧ 2[ Next R ] v R ∧ L R ⇒ L S
In words, I is an invariant of the low-level specification R that is strong enough to prove that every transition according to R's next-state relation is also a possible transition for S , possibly stuttering, and to show that R implies the liveness hypotheses asserted by S . The first two proof obligations establish the safety part of the refinement and do not involve temporal logic; the third one concerns liveness and requires temporal reasoning.

Hiding of internal state. The standard form (1) of specifications is useful for describing a system as a state machine, but it does not distinguish between variables that are visible at the interface and those that represent the internal state of the machine. This distinction is, however, important in the sense that the "contract" between the implementation of a system and its users should only constrain the interface, not the internal state. For example, a highlevel specification S set of a key-value store may represent the current content of the store in a variable store holding a set of pairs (k , v ), but the implementer should be free to choose another suitable data structure, such as a hashtable. Because the operations of the lowerlevel specification S tbl update a hashtable instead of a set of pairs, the implication S tbl ⇒ S set cannot be proved. Indeed, the internal variable store (and the set of values that it holds) is not part of the interface of the system, which solely consists of the input and output channels through which the system corresponds with its environment. Lamport realized that this form of information hiding corresponds to existential quantification: the actual high-level specification of our system is not S set , but rather ∃ ∃ ∃ ∃ ∃ ∃ store : S set , which asserts that the system behaves as if it contained a store represented as a set of key-value pairs. Similarly, the lowerlevel specification is ∃ ∃ ∃ ∃ ∃ ∃ store : S tbl , 3 and in order to establish refinement, we have to prove the implication

∃ ∃ ∃ ∃ ∃ ∃ store : S tbl ⇒ ∃ ∃ ∃ ∃ ∃ ∃ store : S set . (2)
Applying standard quantifier rules, that proof can be reduced to proving the implication

S tbl ⇒ ∃ ∃ ∃ ∃ ∃ ∃ store : S set
where the internal state of the lower-level specification has been exposed. It now suffices to find a suitable state function s that provides a witness term for the internal state of the higherlevel specification, i.e., such that the implication

S tbl ⇒ (S set WITH store ← s) (3)
is provable. (The notation used here for substituting the variable store by the expression s is not part of TLA.) In our example, a suitable witness s is provided by the contents of the hashtable.

State functions that serve as witness terms for refinement proofs are known as refinement mappings. They serve to reconstruct the value of an internal state variable used in the high-level specification from the corresponding lower-level state. Semantically, showing an implication of the form (2) requires exhibiting an infinite sequence of values for the quantified variable on the right-hand side, given a sequence of values for the variable on the left. In contrast, a refinement mapping as in (3) computes values state by state, which is clearly weaker: one cannot refer to previous or future values in the sequence of values satisfying the left-hand specification. Indeed, in general a suitable refinement mapping need not exist even if (2) holds. Abadi and Lamport [START_REF] Abadi | The existence of refinement mappings[END_REF] suggested that for the proof of refinement, the lowlevel specification may be augmented by auxiliary variables. The augmented specification is semantically equivalent to the original one, but the additional variables help in defining a refinement mapping. In particular, Abadi and Lamport defined principles for augmenting specifications by history and prophecy variables, and they provided sufficient conditions for these principles to be complete for proving refinement. The constructions were presented in a semantic framework independent of TLA. Proof rules for introducing auxiliary variables in TLA appear in [START_REF] Lamport | Auxiliary variables in TLA +[END_REF].

Representing parallel composition. The above discussion has shown that refinement and hiding can be represented in TLA using implication and quantification, and therefore standard principles of logical deduction can be applied to reason about these concepts. Now consider two components, specified by TLA formulas Φ and Ψ, that are intended to operate in parallel. In order for both parallel components to adhere to their specifications, the variables of the first component must evolve as prescribed by Φ, and similarly for the second component. In particular, any steps that change a variable shared by both components must be permitted by both Φ and Ψ. Transitions that exclusively modify variables from one specification appear as stuttering steps to the other one and are trivially allowed by that specification, whereas variables shared between Φ and Ψ synchronize transitions of the two specifications. It follows that the formula Φ ∧ Ψ characterizes the parallel composition of the two specifications. (We see in Section 3.3 that for some computational models, it may be useful to adopt a stronger specification Φ ∧ Ψ ∧ Ξ where Ξ expresses extra synchronization hypotheses embodied in the computational model.)

Expressing composition as conjunction corresponds to the overall philosophy of TLA that structural concepts are expressed by logical operators. Although the conjunction of two specifications Φ and Ψ written in the standard form of ( 1) is not itself in standard form, it can easily be transformed into standard form by applying the equivalence

2[A] u ∧ 2[B ] v ≡ 2 [A] u ∧ [B ] v u,v
Specifying open or closed systems. When specifying a component, one invariably has to describe not just the component itself, but also the environment that the component is going to operate in. A closed-system specification of a component describes the most general environment that is acceptable, together with the component itself. In particular, the specification's next-state relation will be a disjunction of actions that describe the component's transitions and of actions that describe steps of the environment. Although this style works well in practice, it does not yield the most general specification of the overall system. Instead of constraining the environment, we may want to write a specification that allows the environment to behave arbitrarily, but that leaves the behavior of the component unconstrained after a step occurred that is disallowed by the assumptions on the environment. Abadi and Lamport considered ways of writing specifications that separate the environment assumptions E and the component guarantees C . The implication E ⇒ C is a natural way for expressing such an assumption-guarantee specification, and this form is explored in [START_REF] Abadi | Composing specifications[END_REF]. However, the implication holds of behaviors in which first the component violates C , and later the environment violates E . In later work, Abadi and Lamport [START_REF] Abadi | Open systems in TLA[END_REF][START_REF] Abadi | Conjoining specifications[END_REF] introduced the stronger operator +

such that E + -C requires that (the safety part of) C may be violated only if (the safety part of) E was violated strictly earlier. 4 Given two components described through assume-guarantee specifications, one may wish to prove that their composition refines a higher-level specification of the composed system. This is expressed in TLA as a proof obligation of the form

(E 1 + -C 1 ) ∧ (E 2 + -C 2 ) ⇒ (E + -C )
In order to establish the overall system guarantee C from the component guarantees C 1 and C 2 , one will need to show that the environment assumptions E 1 and E 2 hold true. Now, the environment of each component consists of the overall environment (assumptions on which are expressed by E ) and the other component, so one will want to use both E and C 2 for establishing E 1 , and similarly for the other component. Despite the apparent circularity of this reasoning chain, Abadi and Lamport [START_REF] Abadi | Conjoining specifications[END_REF] give rules that support this approach in a sound way, based on a form of computational induction that is embodied in the definition of the + operator.

The Specification Language TLA +

Lamport designed TLA as a variant of linear-time temporal logic that is particularly appropriate for specifying executions of fair state machines. Stuttering invariance is key for representing composition as conjunction of specifications, and refinement as validity of implication. Quantification over state variables adds significant expressive power and is useful notably for distinguishing the state visible at the interface of a component from the internal state used for its implementation.

However, TLA is not a full specification language: it does not fix the interpretation of elementary function and predicate symbols such as + and ∈. These symbols are provided by an underlying mathematical language based on first-order or higher-order logic. In particular, non-temporal proof obligations that arise during the verification of a system property or during a refinement proof should then be discharged using a (possibly mechanized) proof system associated with that host language.

Overall Design of TLA +

Starting in the early 1990s and encouraged by successful experiments with TLP [START_REF] Engberg | Mechanical verification of concurrent systems with TLA[END_REF], a prototype proof system for TLA based on the Larch Prover, Lamport developed the specification language TLA + . The language is described in the book Specifying Systems [START_REF] Lamport | Specifying Systems: The TLA + Language and Tools for Hardware and Software Engineers[END_REF]; the Hyperbook and Lamport's video series [START_REF] Lamport | The TLA + hyperbook[END_REF][START_REF] Lamport | The TLA + video course[END_REF] provide excellent tutorial introductions, whereas the description of TLA + in [START_REF] Merz | The specification language TLA +[END_REF] focuses on the semantics of the language. TLA + is based on a variant of Zermelo-Fraenkel set theory with choice (ZFC) for describing the data manipulated by an algorithm. ZFC is widely accepted by mathematicians as the basis for formalizing mathematical theories. In order to emphasize the expressiveness of ZFC, Lamport shows that a formal definition of the Riemann integral can be given in just 15 lines starting from a standard module defining the real numbers with ordinary arithmetical operators [START_REF] Lamport | Hybrid systems in TLA +[END_REF]. When writing high-level specifications of algorithms, it is useful to model data in terms of concepts such as sets and functions rather than using low-level data types provided by programming languages and their libraries. In this respect, TLA + adopts a similar approach as the specification languages Z and (Event-)B [START_REF]The B-Book: Assigning Programs to Meanings[END_REF][START_REF]Modeling in Event-B[END_REF][START_REF] Spivey | The Z Notation: A reference manual[END_REF]. However, the latter languages impose a typing discipline on set theory, whereas TLA + is untyped. Again, Lamport follows classical mathematical practice and, for example, considers that the set {2, 4, 6, . . .} of positive even numbers can be viewed as a type just like the set of all integers. He maintains that imposing a decidable type system on a specification language leads to unacceptable restrictions of the expressiveness of that language. Also, embedding partial operations in a typed language often leads to objectionable choices. For example, declaring integer division as a binary operation with integer arguments and result asserts that division by 0 returns an in-teger, whereas implementations naturally raise an exception. 5 Although TLA + is untyped and handles partial operators by underspecification [START_REF] Gries | Avoiding the undefined by underspecification[END_REF], this does not preclude tools for TLA + to reconstruct types when this is convenient for their analyses. An article by Lamport and Paulson [START_REF] Lamport | Should your specification language be typed[END_REF] contains an interesting discussion of these questions.

A Glimpse of TLA +

TLA + specifications are organized in modules. A module can extend other modules; semantically, this is equivalent to copying the content of the extended modules (with duplicates removed) into the extending module.

A module may declare constant and variable parameters. Any symbol that occurs in an expression in the module must be either a built-in symbol of TLA + , a parameter in the context in which the expression appears, or a symbol that was previously defined or declared.

Modules may assert properties of constant parameters in the form of assumptions or axioms, both of which express hypotheses of the module. 6 Modules may also state theorems that can be proved using TLAPS, the TLA + Proof System.

The bulk of the contents of a typical TLA + module consists of definitions of operators, used to build up more complex expressions. An operator may take zero or more arguments, including operator arguments (whose arity must be specified). For example, the definition Symmetric(R( , ), S ) ∆ = ∀x , y ∈ S : R(x , y) ≡ R(y, x ) introduces an operator characterizing a symmetric binary relation R over a set S . Besides the ordinary operators of first-order set theory, TLA + also borrows a few constructions from programming languages, such as conditional expressions (including n-ary case distinctions) and local definitions introduced through LET-bindings.

A module containing a system specification will usually define operators corresponding to the initial condition, the next-state relation, the overall specification, and properties to be verified. As a concrete example, Figure 2 contains a TLA + specification of a FIFO queue. It extends the library module Sequences, which defines the set Seq(S ) of finite sequences that contain elements of S , as well as operations such as Head and Tail to access the first element and the remaining elements of a sequence. Module FIFO then declares two constants Data and null that correspond to the data to be stored in the queue and a "null" element representing the absence of data. The module also declares the variables in, out, and q that are used for specifying the state machine describing the behavior of the FIFO queue. Concretely, in and out represent the channels for data input and output, whereas q contains the current contents of the queue. Again, TLA + is untyped, and consequently one does not declare types for constant or variable parameters. Because TLA + is based on set theory, there is no need to assert that Data is a set. In fact, semantically all values are sets, although it is more useful to think of the elements of set Data ∪ {null}, as well as of numbers or strings, as atomic values.

MODULE FIFO EXTENDS Sequences CONSTANTS Data, null ASSUME null / ∈ Data VARIABLES in, q, out TypeOK ∆ = in ∈ (Data ∪ {null}) ∧ out ∈ (Data ∪ {null}) ∧ q ∈ Seq(Data) Init ∆ = in = null ∧ out = null ∧ q = Enq ∆ = ∧ in ∈ (Data ∪ {null}) \ {in} ∧ q = IF in ∈ Data THEN Append(q, in ) ELSE q ∧ out = out Deq ∆ = ∧ ∨ q = ∧ out = null ∧ q = q ∨ q = ∧ out = Head(q) ∧ q = Tail(q) ∧ in = in vars ∆ = in, q, out FIFO ∆ = Init ∧ 2[ Enq ∨ Deq ] vars ∧ WF vars (Deq) THEOREM FIFOType ∆ = FIFO ⇒ 2TypeOK THEOREM InOut ∆ = FIFO ⇒ 2[ in = in ∨ out = out ] vars THEOREM Liveness ∆ = FIFO ⇒ ∀x ∈ Data : (in = x ) ; (out = x )
The second block of the module contains operator definitions. 7 The first operator corresponds to the (intended) type invariant of the specification. The definitions of the operators Init, Enq, and Deq introduce the initial condition and the enqueue and dequeue actions of the queue. The initial predicate simply requires that the input and output channels contain the null value and that the queue is empty. The enqueue action models a change of value at the input channel. If a data value is sent over the channel, it is appended to the current contents of the queue. Otherwise (i.e., if a null value appears on the channel), the queue remains unchanged. The output value of the queue remains unchanged during an enqueue operation. Symmetrically, a dequeue operation does not modify the input channel. It puts null on the output channel and leaves the queue unchanged if the queue is empty and otherwise sends Head(q) on the output channel and removes that element from the queue. Formula FIFO represents the overall queue specification. Its next-state relation is the disjunction of the enqueue and dequeue actions. The fairness conjunct requires dequeue actions to happen eventually so that the queue must eventually output the values that it stores.

MODULE TwoFIFO EXTENDS Sequences CONSTANTS Data, null ASSUME null / ∈ Data VARIABLES in, q1, mid, q2, out Left ∆ = INSTANCE FIFO WITH q ← q1, out ← mid Right ∆ = INSTANCE FIFO WITH in ← mid, q ← q2 Conc ∆ = INSTANCE FIFO WITH q ← q2 • q1 Interleave ∆ = in = in ∨ out = out TwoFIFO ∆ = Left!FIFO ∧ Right!FIFO ∧ 2[Interleave] in,out THEOREM Implementation ∆ = TwoFIFO ⇒ Conc!FIFO
The third block of the module asserts three theorems. The first theorem states that the type correctness predicate holds throughout any execution. The second theorem states that the values of the input and output channels never change simultaneously, and the third theorem asserts that every data value that appears on the input channel will eventually be output by the queue. We will see in Section 5 how these properties can be verified using the TLA + tools.

Composing Modules

Beyond module extension, TLA + offers instantiation as a second way for composing modules.

An instance conceptually creates a copy of the original module in which the constant and variable parameters can be instantiated by (constant and state) expressions. This construction is useful for composing specifications. For example, module TwoFIFO of Figure 3 declares the composition of two FIFO queues by creating two instances Left and Right of the FIFO module of Figure 2. Instance Left uses variables q1 and mid for the internal queue and the output channel; all other parameters are instantiated by the parameters of the same name declared in module TwoFIFO. Similarly, instance Right uses mid and q2 for in and q. The conjunction of the two instantiated specifications Left!FIFO and Right!FIFO describes the composition of two FIFO queues that communicate through the shared communication channel mid. We would like to assert that the conjunction of these specifications behaves like a FIFO whose internal queue is given by the concatenation of the internal queues of the two components. The instance Conc represents this "longer" FIFO queue with input channel in and output channel out, and we would therefore like to assert the theorem

Left!FIFO ∧ Right!FIFO ⇒ Conc!FIFO.
However, this implication is not valid: the conjunction on the left-hand side allows an enqueue action of the left FIFO queue and a dequeue action of the right FIFO queue to happen simultaneously (observe that both actions leave the shared variable mid unchanged). In this case, the values of the channels in and out change simultaneously, and this is not allowed by specification Conc!FIFO. Indeed, we wrote our specification according to an interleaving model, where enqueue and dequeue actions do not happen simultaneously. We have to explicitly enforce this interleaving assumption for the composition of the two FIFO queues, as expressed in the specification TwoFIFO, in order to obtain the theorem Implementation stated at the end of the module.

PlusCal: an Algorithm Language

Due to its expressiveness and high level of abstraction, TLA + is a very powerful language for specifying high-level designs of concurrent algorithms and systems. However, it may feel unfamiliar to programmers, in particular due to the syntax based on mathematical logic and to the absence of explicit control flow in the specification of systems and algorithms. Lamport designed PlusCal [START_REF] Lamport | The PlusCal algorithm language[END_REF] as a language for describing algorithms that combines the look and feel of pseudo-code and the precision of TLA + . It uses primitives that are familiar from imperative programming languages for describing the control flow of an algorithm. In contrast, the data manipulated by the algorithm is represented by TLA + expressions, letting the algorithm designer benefit from the abstraction afforded by set theory without being constrained by concerns of how to concretely implement data structures. A PlusCal algorithm is embedded as a comment within a TLA + module and has access to all operators available at that point of the module (whether defined in extended modules or locally). The PlusCal translator converts the algorithm into a TLA + specification that is inserted into the module. The user then states properties in terms of the TLA + translation and verifies them just as for any other TLA + specification, using the tools described in Section 5.

A PlusCal algorithm may declare several process templates for parallel execution, and each template can have a fixed number of instances. 8 Variables can be declared globally, representing shared state (including the communication network of a distributed system), or locally for each process. The control flow of each process is described using standard primitives of imperative languages (sequencing, conditional statements, loops, procedure calls etc.). In addition, the two primitives either { . . . } or { . . . } and with (x ∈ S ) { . . . } are available for modeling non-determinism. The first construct can be used to introduce a fixed number of alternatives, the second one executes a block of code for some value that is chosen non-deterministically from the set S . Synchronization among processes is modeled using the instruction await P that blocks until the predicate P becomes true. An important aspect for the specification of concurrent algorithms is to identify the "grain of atomicity", i.e., which blocks of statements are intended to be executed without interference from other processes. Rather than imposing an arbitrary fixed level of atomicity, PlusCal uses labels to identify yield points at which processes may be interrupted. A group of statements between two labels is assumed to be executed atomically. This allows the designer to choose the degree of atomicity appropriate for the specification and to compare algorithms described at different degrees of atomicity. 9 In order to ensure liveness of PlusCal algorithms, fairness conditions may be attached to labels or to entire processes. These ensure that the group of statements following the label (respectively, the entire process) will eventually execute if it is sufficiently often enabled.

As an example, a PlusCal algorithm modeling a simple producer-consumer system appears in Figure 4. It declares two process templates for the producer and the consumer, each of which is instantiated once for process identities "p" and "c". The two processes communicate using a shared FIFO queue of bounded capacity maxCapacity. Each process has an infinite loop: the producer repeatedly adds new data to the queue, while the consumer retrieves the data from the queue. By declaring a (weak) fairness condition for the consumer process, we ensure that every data item that is present in the queue will eventually be consumed. In this specification of the algorithm, the bodies of the while loops execute atomically; non-atomic execution would be modeled by inserting additional labels. The operations Len, Append, Head, and Tail that appear in the presentation of the algorithm are defined in the standard module Sequences that is extended by module ProducerConsumer.

Invoking the PlusCal translator on module ProducerConsumer generates a TLA + specification corresponding to the algorithm. In particular, the translator generates declarations of TLA + variables corresponding to the global and local variables of the PlusCal algorithm, and it derives the initial condition from the initializations of the PlusCal variables. 10 The essential step of the translation is to generate a TLA + action for each group of statements between Because the translation from PlusCal to TLA + is fairly direct, the generated TLA + specification is usually quite readable. This is important because correctness properties of the algorithm are written in TLA + rather than in PlusCal. For our producer-consumer example, we may want to verify the invariant BoundedQueue and the temporal property Liveness defined as

BoundedQueue ∆ = q ∈ Seq(Data) ∧ Len(q) ≤ maxCapacity Liveness ∆ = ∀d ∈ Data : (∃i ∈ 1 .. Len(q) : q[i ] = d ) ; rcvd = d
that express type correctness and eventual reception of every data item contained in the queue.

Tool Support

The model checker TLC

Lamport originally designed TLA + as a precise and expressive language for specifying algorithms and for (deductively) reasoning about their properties. It was used in the second half of the 1990s by hardware designers at Digital Equipment Corporation, in particular for describing cache coherence protocols of multiprocessors [START_REF] Joshi | Checking cache-coherence protocols with TLA +[END_REF]. They wrote rigorous, informal proofs for key invariants maintained by these protocols. Yuan Yu then recognized that it was possible to support this type of reasoning using model checking. Lamport reports that originally he was very skeptical of this idea. Input languages for model checkers such as Spin [START_REF] Holzmann | The SPIN Model Checker[END_REF], SMV [START_REF] Mcmillan | Symbolic Model Checking[END_REF] or Murphi [START_REF] Dill | Protocol verification as a hardware design aid[END_REF] are based on low-level primitives carefully chosen to support efficient verification of finite-state systems, whereas TLA + uses the full power of ZFC set theory and is intended for modeling systems of arbitrary size. It is not possible in general to systematically enumerate all behaviors that satisfy a given TLA + formula.

TLC, the TLA + model checker, accepts a subset of TLA + specifications written in standard form [START_REF] Abadi | The existence of refinement mappings[END_REF]. It is an explicit-state model checker, intended for verifying finite instances of specifications. In addition to the specification, the user has to provide the model checker with a model that describes a finite instance by fixing specific values for constant parameters. For the queue specification of Figure 2, one could for example fix parameter values Data = {1, 2, 3} and null = 0. TLC then interprets the specification, restricted to this model, by decomposing the next-state relation into disjuncts (bounded existential quantification over finite sets is expanded into an explicit disjunction) and evaluating each disjunct from left to right. The first occurrence of a primed variable v is expected to be of the form v = e or v ∈ e for an expression e that TLC can evaluate; in the second form, e must evaluate to a finite set. The first form is interpreted as an assignment of (the value denoted by) e to v in the successor state. The second form leads to the generation of one successor state per element of e, with v assigned to that element. Subsequent occurrences of v are interpreted by the value assigned to v in the successor state in this way. For example, the conjunct in ∈ (Data ∪ {null}) \ {in} of the action Enq of Figure 2 generates one successor state for each element of Data ∪ {null}, except for the current value of in. The occurrences of in in the second conjunct of Enq then refer to the value chosen for that successor state. The initial predicate is evaluated in a similar way. TLC will abort with an error message if the initial predicate or some subaction of the next-state relation does not assign a value to some of the variables declared in the module.

When evaluating set-theoretic expressions, TLC will generally enumerate the elements, but it will apply some optimizations. For example, in evaluating the predicate e ∈ Nat that may occur in a typing invariant, TLC will simply check if (the value denoted by) e is a natural number. TLC disallows unbounded quantification, and it signals an error when it would have to enumerate an infinite set.

Using the strategy outlined above, TLC enumerates all reachable states in a breadth-first manner, and it checks the invariant predicates provided by the user during this state enumeration. When an invariant evaluates to false, the run is aborted and a counter-example is displayed. (Due to breadth-first search, that counter-example will be of minimal length.) Liveness properties are evaluated over the state graph computed during state enumeration, based on the tableau algorithm of [START_REF] Lichtenstein | Checking that finite state concurrent programs satisfy their linear specification[END_REF]. TLC parallelizes state enumeration on multi-core machines and provides a distributed implementation for running in a cluster or cloud environment. States may be stored to disk so that state exploration is not memory bound, and TLC regularly performs checkpoints so that model checking can be resumed in case of a crash. In order to limit the explored state space, the user can impose state constraints. For example, the FIFO queue of Figure 2 generates an unbounded state space even for a fixed finite set Data because the length of the queue can grow without bound, and the user can choose not to explore successors of states in which Len(q) exceeds some fixed value. TLC also implements symmetry reduction in order to explore only a quotient of the state space with respect to an equivalence relation. In the queue example, the user may choose to declare Data (or more precisely, the set that the parameter Data is instantiated with in the concrete model) as a symmetry set because all operations are insensitive to particular values in that set.

Although TLC imposes certain restrictions on the specifications that it can check, most specifications that are written in practice adhere to those restrictions or can easily be rewritten so that they do. (The fact that TLC has been the main analysis tool for TLA + specifications has also contributed to disciplining users so that they respect those restrictions.) In particular, TLA + specifications obtained from translating PlusCal algorithms can be checked using TLC. The different properties asserted in the modules of the previous sections can be verified by TLC for concrete instances of parameters, including the theorems of Figures 2 and3, as well as the properties of the producer-consumer system given at the end of Section 4. 11Like most model checkers, TLC is most useful when a counter-example to a putative property is discovered. A positive verdict only means that the checked properties hold for the particular model that TLC checked, and it requires sound engineering judgement to determine if this gives enough confidence in the correctness of the properties for arbitrary instances of the specification.

The TLA + Proof System

TLAPS, the TLA + Proof System [START_REF] Cousineau | TLA + proofs[END_REF], is a proof assistant for checking proofs written in TLA + . For this purpose, TLA + was extended to include a language for writing hierarchical proofs based on a format that Lamport had proposed earlier [START_REF] Lamport | How to write a proof[END_REF] for writing rigorous pencil-andpaper proofs. For example, the proof of type correctness for the FIFO queue of Figure 2 can be written as follows.

THEOREM FIFOType

∆ = FIFO ⇒ 2TypeOK 1 1. Init ⇒ TypeOK BY DEF Init, TypeOK 1 2. TypeOK ∧ [ Enq ∨ Deq ] vars ⇒ TypeOK BY DEF Enq, Deq, vars, TypeOK 1 3. QED BY 1 1, 1 2, PTL DEF FIFO
Following a standard pattern for invariance proofs (cf. also rule INV1 of Section 2.2), the first two steps of the proof establish that the initial predicate of the FIFO specification implies predicate TypeOK, and that the predicate is preserved by every step allowed by the next-state relation. The third step concludes the proof of the theorem. The justifications for each step are indicated following the keyword BY. For the first two steps, it suffices to expand the relevant definitions and then apply built-in automatic proof back-ends that mechanize standard mathematical reasoning. The justification of the third step uses the assertions of the two preceding steps and propositional temporal logic; it also expands the definition of FIFO in order to expose its initial and next-state predicates. Because the proof is so simple, we only needed one level of proof: all step names have the form 1 n. The steps of more complicated proofs can be decomposed into lower-level proof steps until TLAPS can prove the leaf steps of the proof automatically.

Figure 5 schematizes the architecture of TLAPS. The central component is the proof manager that interprets the proof language, maintains the context of each proof step (i.e., the visible identifiers, assumptions, and definitions) and computes the corresponding proof obligations. In a non-temporal step (such as the first two steps in the above example), primes are pushed inside complex expressions, and then primed symbols are replaced by fresh identifiers. Similarly, any temporal expressions appearing in the context are abstracted by fresh predicate symbols. Similarly, in a temporal step (such as the QED step above), any first-order formulas are abstracted by propositional variables. This transformation is called coalescing [START_REF] Doligez | Coalescing: Syntactic abstraction for reasoning in first-order modal logics[END_REF]; it is necessary so that back-end provers see the proof obligation either as . . . a standard formula of mathematical set theory or as a propositional temporal logic formula. The proof manager then calls back-end provers to attempt and prove the proof obligation. Currently, TLAPS supports SMT solvers (via a translation to the SMT-LIB2 language [START_REF] Barrett | Satisfiability modulo theories[END_REF]), the tableau prover Zenon [START_REF] Bonichon | Zenon: An extensible automated theorem prover producing checkable proofs[END_REF], and an encoding of TLA + 's mathematical set theory as an object logic in the logical framework Isabelle [START_REF] Paulson | Isabelle: A Generic Theorem Prover[END_REF] for proving non-temporal steps. It also comes with a decision procedure for propositional temporal logic [START_REF] Suda | A PLTL-prover based on labelled superposition with partial model guidance[END_REF] for proving temporal proof obligations. The architecture is open for supporting additional back-end provers through suitable translations of proof obligations into their input language. For increased confidence in the correctness of TLAPS proofs, when a back-end prover finds a proof it may return a justification to the proof manager for checking by the trusted kernel of Isabelle. This certification step is optional and currently only available for proofs found by Zenon.

TLAPS is currently restricted to proving safety properties. The planned extension to liveness properties requires support for handling ENABLED predicates and for first-order temporal logic reasoning, for example for mechanizing the Lattice rule of Section 2.2. TLAPS has been used for verifying several distributed algorithms, including variants of Paxos [START_REF] Chand | Formal verification of Multi-Paxos for distributed consensus[END_REF][START_REF] Lamport | Byzantizing Paxos by refinement[END_REF] and a version of the Pastry distributed hash table [START_REF] Azmy | A machine-checked correctness proof for Pastry[END_REF].

The TLA + Toolbox

Editing and analyzing TLA + specifications is facilitated by the TLA + Toolbox, an Eclipse application that provides an IDE (integrated development environment) for TLA + . It provides support for editing TLA + specifications and proofs, such as looking up operator definitions, properly indenting TLA + specifications, renumbering proof steps, and hiding subproofs that are irrelevant for the current branch. The Toolbox is integrated with the TLA + tools, including SANY, the TLA + syntactic and semantic analyzer, the TLAT E X pretty printer, TLC and TLAPS.

In particular, the user interface to TLC provided by the Toolbox greatly simplifies the definition of finite-state models to be verified, the analysis of counter-examples, and the evaluation of TLA + expressions. All TLA + tools are released as open-source software under permissive licences for use in industry or academia.

Impact

The concepts that Lamport introduced for the formal specification and verification of algorithms have deeply influenced the research community. The notions of safety, liveness, and fairness are universally recognized for their fundamental importance. The concept of stuttering invariance is valuable in contexts other than those strictly related to refinement and composition; in particular, it plays an important role for partial-order reductions used for model checking distributed systems [START_REF] Godefroid | A partial approach to model checking[END_REF][START_REF] Valmari | A stubborn attack on state explosion[END_REF]. The idea of writing system specifications in terms of state machines is widely accepted [START_REF]Modeling in Event-B[END_REF][START_REF] Gurevich | Evolving algebras 1993: Lipari guide[END_REF]. The specification language TLA + is taught at universities around the world, and PlusCal is starting to be used as a vehicle for teaching courses on distributed algorithms.

The historically first significant use of TLA + in industry was for specifying and verifying cache coherence protocols by a group of hardware engineers that designed Digital Equipment Corporation's Alpha processors [START_REF] Joshi | Checking cache-coherence protocols with TLA +[END_REF]. Members of that group subsequently moved to Intel and continued to use TLA + , although little is publicly known about the impact of that work. Work at Microsoft using TLA + started around 2003 with the specification of the Web Services Atomic Transaction protocol [START_REF] Johnson | Formal specification of a web services protocol[END_REF]. This experience was considered successful, and engineers at Microsoft continued to use TLA + . Reportedly, use of TLA + contributed to identifying a serious error in the XBox 360 memory system that would have been difficult to debug using conventional techniques. The Farsite project [START_REF] Bolosky | The Farsite project: a retrospective[END_REF] at Microsoft Research developed a scalable, serverless, and location-transparent distributed file system that could tolerate nodes being unavailable, as well as malicious participants. The designers used TLA + for specifying the distributed directory service and refined a centralized functional specification into the formal description of a distributed protocol. They report that the main benefit of using formal specification and verification was to understand the invariants that the system must maintain through different levels of refinement. They consider that it would have been far more costly to iterate through several designs at the implementation level where aspects related to the distributed protocol would have been mixed with low-level coding details. In contrast, they found that developing an implementation from the protocol specification was rather straightforward because only sequential code had to be written, without a need for thinking about aspects related to distributed execution. In the later IronFleet project [START_REF] Hawblitzel | Ironfleet: proving practical distributed systems correct[END_REF][START_REF] Hawblitzel | Ironfleet: proving safety and liveness of practical distributed systems[END_REF], researchers at Microsoft pushed this idea even further. Combining a TLA-style approach to state machine specification and refinement with a Floyd-Hoare style of reasoning about imperative programs provided by Dafny [START_REF] Leino | Dafny: An automatic program verifier for functional correctness[END_REF], they obtained a mechanized framework for designing, implementing, and verifying distributed systems from high-level (centralized) specifications to distributed protocols and further to executable code that exhibited competitive performance. Based on an embedding of TLA and its proof rules in Dafny, they could prove not only safety, but even liveness properties in a unified framework. The approach was used to develop a replicated state machine library and a sharded key-value store.

An interesting account of the use of TLA + in industry was provided by a group around Chris Newcombe working at Amazon Web Services [START_REF] Newcombe | How Amazon Web Services uses formal methods[END_REF]. They reported that not only have TLA + specifications contributed to finding subtle bugs in high-level designs of distributed protocols, but that the understanding and confidence obtained from formal specification and verification allowed them to make aggressive performance optimizations without sacrificing correctness. Several other companies developing web and cloud services, including the groups working on Azure at Microsoft, actively use TLA + and TLC for describing and verifying the protocols they design. The TLA + Google group 12 and regular in-person community meetings provide forums for the members of the TLA + community to exchange and help each other in case of problems.

TLA + is intended as a formalism for modeling and verifying high-level designs of algorithms and systems. Doing so does not prevent coding errors from creeping into implementations of verified algorithms: such errors can be caught using techniques of program verification. However, the implementation of a buggy design is virtually guaranteed to contain the design errors, and finding and fixing these issues at the level of executable code is much more difficult and costly than to do so at an early stage of development, using specifications written at the appropriate level of abstraction.

Figure 1

 1 Figure 1 Proof rules for simple TLA.

Figure 2

 2 Figure 2 TLA + specification of a FIFO queue.

Figure 3

 3 Figure 3 Composition of two FIFO queues.

Figure 5

 5 Figure 5 Architecture of the TLA + Proof System.

We could distinguish a level of constant formulas that do not contain any variables, but we will consider such formulas to be state formulas.

Of course, it is immaterial if the names of the bound variables in the two specifications are the same or not.

+can actually be expressed in TLA, but it is useful to consider it as a separate operator.

Some proof assistants such as Isabelle/HOL go even further and define n div 0 = 0, which is unlikely to hold in an implementation and may actually mask errors.

TLC will verify that an assumption evaluates to true for the concrete values substituted for the module parameters, but it will not evaluate axioms.

The horizontal bars are decorative and have no semantic meaning.

PlusCal does not support dynamic spawning of processes.

Some rules govern where labels must or cannot be placed, essentially to ensure that PlusCal algorithms are easy to translate into TLA + specifications.

For PlusCal variables that are not initialized, such as rcvd in our example, the translator adds a default initialization, which is necessary for model checking using TLC.

The specification TwoFIFO of Figure3needs to be rewritten in standard form so that TLC can verify it.

 [START_REF] Barrett | Satisfiability modulo theories[END_REF]https://groups.google.com/forum/#!forum/tlaplus Bibliography

MODULE ProducerConsumer

EXTENDS Naturals, Sequences CONSTANTS Data, maxCapacity

variable rcvd; { c : while (TRUE) { await nonempty; rcvd := Head(q); q := Tail(q) } } } *)

Figure 4 A specification of a producer-consumer system in PlusCal. two consecutive labels. For example, the loop body of the producer process of Figure 4 is represented by the action

For more complicated algorithms, the translator adds a variable pc that represents the current point of control of each process. When a process type has several instances, their local variables are represented using arrays (i.e., TLA + functions).


Comparative Study of Fingerprint Database Indexing Methods

Keywords: Biometrics, matching, indexing, fingerprint, minutiae, quality metrics, NFIQ2, Locality-sensitive Hashing

Nowadays, there are large country-sized fingerprint databases for identification purposes, for border access controls and also for Visa issuance procedures around the world. Fingerprint indexing techniques aim to speed up the research process in automatic fingerprint identification systems. Therefore, several preselection, classification and indexing techniques have been proposed in the literature. However, the proposed systems have been evaluated with different experimental protocols, that makes it difficult to assess their performances. The main objective of this paper is to provide a comparative study of fingerprint indexing methods using a common experimental protocol. Four fingerprint indexing methods, using naive, cascade, matcher and Minutiae Cylinder Code (MCC) approaches are evaluated on FVC databases from the Fingerprint Verification Competition (FVC) using the Cumulative Matches Curve (CMC) and for the first time using also the computing time required. Our study shows that MCC gives the best compromise between identification accuracy and computation time.

I. INTRODUCTION

Fingerprint biometric systems use fingerprint characteristics (unique, permanent and easy-to-acquire properties) for people recognition. Fingerprint databases are widely used for border control and administrative procedures. For example, Aadhaar is the largest biometric database, with more than 1 billion persons, built for indian population [START_REF]Unique Identification Authority of India UIDAI. Role of biometric technology in Aadhaar authentication[END_REF].

Two tasks are mainly achieved by biometric systems: verification and identification. Verification task, also referred as 1-1 matching, consists on deciding whether a person, who claims an identity, is or is not the owner of that identity. Verification systems are evaluated with two accuracy metrics: False Acceptance Rate (FAR) and False Reject Rate (FRR). The FAR is inversely related to FRR. Identification task, also referred as 1-N matching aims to find a target person in a biometric database. Identification task requires a long computation time to carry out the comparisons against all database entries. Moreover, performing all comparisons increases the identification error rates [START_REF] Asker | Indexing Fingerprint Databases Based on Multiple Features[END_REF]. Therefore, classification, clustering and indexing strategies are prominent to achieve the identification task in limited time. The first objective of indexing method is to split and filter a large database, to reduce the list of candidates. This is measured by the Penetration Rate (P R) computed as P R = #candidates * 100 database Size . The second objective is to ensure that the list of candidates contains the target. This is measured by the Hit Rate (HR) computed as HR = #W ell Identif ied Candidates * 100 #T otal Identif ied Candidates T est . The objective for an indexing method applied to fingerprint identification is to tend PR to 0 and HR to 100.

The main challenge in fingerprint identification is to achieve both high speed and accuracy. The recently proposed algorithms used different experimental protocols and have been evaluated on different fingerprint databases [START_REF] Zhou | Fingerprint indexing based on combination of novel minutiae triplet features[END_REF], [START_REF] Gyaourova | A Novel Coding Scheme for Indexing Fingerprint Patterns[END_REF]. Therefore, it is not simple to objectively compare the performance of the proposed algorithms. In this paper, we provide a comparative study of various state-of-the-art indexing algorithms. To our knowledge, such a comparative study was never proposed in previous works. This is our main contribution to an important topic in biometrics. The rest of this paper is organized as follows. In section II, various indexing algorithms applied to fingerprint identification are presented. Section III describes the four selected methods for our comparative study. In section IV, a common experimental protocol is proposed and evaluation performances are exposed. Conclusions and perspectives are given in Section V.

II. RELATED WORKS

There are two main categories for fingerprint features: global and local features. For global features, fingerprint representation uses the core point, ridges shapes, ridges number and singular points such as delta and loop [START_REF] Maltoni | Handbook of Fingerprint Recognition[END_REF]. On the other hand, local representation uses fingerprint minutiae points and pores to build a solid geometric neighborhood features (Triplets, quadruplets, circle or cylinder arround minutiae) [START_REF] Asker | Indexing Fingerprint Databases Based on Multiple Features[END_REF].

Generally, the problem of database searching is adressed using three strategies: classification, clustering and indexing. Classification is a supervised learning approach while clustering uses an unsupervised learning technique. Indexing is the combination of classification and clustering by assigning an index number to each database entry. Figure 1 shows the identification process using a classification/indexing strategy. The first classification method was proposed by Henry [START_REF] Henry | Classification and uses of finger prints[END_REF] in 1900 based on global features extraction. He proposed partitioning fingerprint databases into five classes: right loop, left loop, whorl, arch and tented arch. In [START_REF] Jain | A multichannel approach to fingerprint classification[END_REF], the authors proposed a five-class based classification. In order to improve the accuracy rate, they used the core point and built 48 areas of interest arround this point. In [START_REF] Zhang | Fingerprint classification based on extraction and analysis of singularities and pseudoridges[END_REF], [START_REF] Najim | Classification of Fingerprint Images Using Neural Networks Technique[END_REF], [START_REF] Karu | Fingerprint Classification[END_REF],

Joannes Falade, Sandra Cremer, Christophe Rosenberger authors proposed to increase the number of classes (from five to nine) to achieve better performances. However, exclusive classification into five to nine fingerprint classes is limited by the small number of classes [START_REF] Henry | Classification and uses of finger prints[END_REF]. Thus, fingerprint indexing methods are used in recent works to improve the PR and HR. Although many approaches used indexing strategy, they focused on fingerprint features representation as a discriminatory factor. In [START_REF] Parmar | Fingerprint Indexing Approches for Biometric Database: A Review[END_REF], a valuable review of fingerprint indexing methods was presented. In [START_REF] Iloanusi | Indexing fingerprints using minutiae quadruplets[END_REF], an original indexing fingerprint method based on minutiae quadruplets was described. In [START_REF] Khodadoust | Fingerprint indexing based on minutiae pairs and convex core point[END_REF] and [START_REF] Khodadoust | Fingerprint indexing based on expanded Delaunay triangulation[END_REF] an expanded Delaunay triangulation (triplets) and minutiae pairs was proposed to develop a fingerprint indexing method with good performances. A new triplets scheme for fingerprint indexing was detailled in [START_REF] Zhou | Fingerprint indexing based on combination of novel minutiae triplet features[END_REF] while in [START_REF] Cappelli | Candidate List Reduction Based on the analysis of Fingerprint Indexing Scores[END_REF], the authors proposed a comprehensive approach to reduce the list of possible candidates index. Note that indexing methods are generally based on the local features because they seem to be the most discriminative features.

III. SELECTED METHODS

In this part, we describe the selected methods for the comparative study. These methods are based on basic, cascade, matcher and MCC approaches. We choose these methods for their simplicity, good performances and the fact that our fingerprint representation is appropriate for their implementation. These methods are evaluated in terms of HR and P R along with the computing time.

Let's D be a database of size M and m i is a matcher. m i is characterized by F AR, F RR and a computation time for matching t i . We note T ime the time required for a fingerprint searching in D.

A. Basic method

The basic method for the identification task is also known as the naive one. It consists on considering identification as multiple successive verifications. In the database D, an input fingerptint I is compared to all M fingerprints to return a shortlist of best scores. The time required to compute basic is T ime = M * t i .

B. Cascade method

Cascade method is a combination of successive naive methods. Generally, the faster a matching algorithm is, the less precise it is. Therefore, the cascade is forged by the fastest matching algorithm at the front and the most accurate algorithm at the end (see figure 2). The time required to compute cascade is

T ime = l i=1 k i-1 * t i .

C. Matcher method

The matcher method was introduced by Arun Ross [START_REF] Gyaourova | A Novel Coding Scheme for Indexing Fingerprint Patterns[END_REF] for fingerprint indexing. This method was proposed to build a new input fingerprint index by using other specific fingerprints as references. Fingerprints which produce a high variance of matching scores against other fingers are chosen as references (discriminative property). These n references are at most 5% of M. Then, a quantification process used a threshold value to discretize each matching score against the references. The size of the created index is equal to the number of the chosen references. To retrieve the list of candidates for an input fingerprint I, the matching scores are only computed against references and then, the candidates list is the closest set of fingerprints to I according to the Hamming distance. This representation depends on the number of references n, discretization interval b and maximum Hamming distance, considered as valid, d. We compute the time as T ime = n * t i

D. Mcc method

Minutiae Cylinder Code (MCC) is a binary representation of a fingerprint proposed by Capelli et al. in [START_REF] Cappelli | BMinutia Cylinder-Code: A New Representation and Matching Technique for Fingerprint Recognition[END_REF]. Authors described each minutiae of a fingerprint as a discretized binary cylinder which represents its neighborhood. Localitysensitive Hashing (LSH) shows good performances for high binary dimension reduction. It is performed with MCC to create an indexing method as explained in [START_REF] Cappelli | Short papers: Fingerprint Indexing Based on Minutia Cylinder-Code[END_REF]. l multiple LSH functions are executed to index each minutia of each fingerprint template. The intuition is that the minutiae of similar templates have a good chance of being under the same index value for a reduced h dimension (h << n). To retrieve a shortlist for an input query fingerprint, the identifiers of template models that share the maximal indexes with the query are selected. We roughly assume MCC identification time is given as T ime = l * t i .

IV. EXPERIMENTAL PROTOCOL

In this section, fingerprint databases are presented. Then parameters of the selected methods are fixed. Finally, exper-imental results in terms of CMC and computing time are exposed.

A. Fingerprint Databases

To evaluate the four selected methods, we show the result on Fingerprint Verification Competition (FVC) databases FVC 2002DB1. This database contains 100 individuals and 8 samples per person. We also combined eleven FVC databases (2000DB1 to 2006DB4) to build challenging large database. This database is ten times larger than FVC2000DB1. We use the best sample, provided by NFIQ2 metric [14], for enrolment and the rest as queries.

B. Parameters Setups

Table I shows the performance of the different matching algorithms in terms of Equal Error Rate (EER) and computing time. EER is obtained with the threshold where FAR=FRR. The algorithms are commercial. 1 Basic method is applied with algo4. For cascade approach, algo1, algo2 and alog4 are executed in this order (see Figure 2). Matcher method is performed with algo3 using parameters such as: b = 2, n = 5 and d = 3. As previously explained, MCC method does not require a matching algorithm and its parameters are given such as: n = 1532, h = 32, l = 25, min = 5. Note that if the number of bit '1' in the minutiae hash is less than min, the minutiae is rejected.

C. Experimental results

The main contribution of the proposed study is to evaluate different indexing methods, with the same databases and ressources. The CMC (Cumulative Matches Curve), which combines P R and HR, is computed. We also add the computing time for each indexing method performance metrics for indexing methods. These conditions allow us to provide a solid and common environment benchmark for the different pre selection methods.

Figure 3 shows the CMC of basic, cascade, matcher and MCC methods. Furthermore, the computation time for each method is respectively 67, 21, 1 and 5 milliseconds for this database of 100 individuals. According to this CMC, the basic method seems to perform as the best. This is explained by two reasons. Firstly, the fingerprint query is compared to all database entries. Secondly, the best matching 1-1 algorithm (algo4) is used. However, the basic method gives the longest computing time. Therefore, this method is not appropriate for large database (as Aadhaar one as for example). The cascade method shows similar performances as the basic method. However, for the figure 3 , the CMC shows worse performances. As previously mentionned, the front matching algorithm for the cascade approach is algo1. The errors made by this algorithm cannot be recovered by the following matching algorithms (algo2 and algo4), which explains the difference with the basic approach results. The matcher method presents the worst performances. For example, to obtain a HR greater than 75%, the P R need to exceed 50%. On the other hand, for this method the computing time is the shortest because the indexes are computed from few matching references (just five matching 1-1 in our case and only 1millisecond required).

Figure 4 shows the CMC of basic, cascade, matcher and MCC methods, computed on the combined FVC databases. This explains the accuracy results under real conditions of challenging and large database. The MCC method seems to be the best identification strategy. Although the database is more complex, It achieves the best performance. The CMC curve is as good as the CMC of a simple FVC database which contains just 100 individuals (Green curves are the same for figures 3 and 4). The accuracy of basic and cascade methods has dropped sharply and show that these methods are not adapted to large database. So, the MCC appraoch presents the best compromise between performances and computing time. For a challenging and very short database, such as FVC2002DB1 (fig. 3), the MCC obtains similar result as basic approach and outperforms cascade and matcher approaches. We notice that for a P R = 10%, the HR > 95%. Moreover, for a large databases (more than 1000 individuals), MCC keeps the same CMC accuracy shape. This confirms that the MCC indexing strategy is independant from database complexity.

This study allows us to point out the following conclusions: The basic and cascade are not suited for very large databases more than 1000 individuals. These approaches are totally rely on the performances of the 1 -1 matching algorithm and are only appropriate for small-sized database (at most hundred of people). The Matcher method is appropriate for real-time application but depends on the performances of the discretization technique. The MCC technique is resistant to the quality of the figerprints and gives the best compromise between accuracy and computing time. This paper provides a comparative study of four fingerprint indexing methods. Basic, cascade, matcher and MCC approaches are selected to conduct this study. The main contribution of this paper is to compare the indexing methods under a common experimental protocol using FVC databases and also proposed a challenging large database for assessing indexing methods. Our study shows that MCC gives the best results in terms of CMC and computing time. In addition, we noticed that indexing techniques based on cascade approach depends on the 1-1 matching algorithms and the quality of fingerprint databases. Future works will be dedicated to extend this paper and details about each implemented method against more databases.

Figure 1 .

 1 Figure 1. Fingerprint identification process of an input fingerprint with a large database of size M. Identification strategies such as classification or indexing are used to retrieve a shortlist of k candidates for next verification step (on Matcher box). Note's, k << M

Figure 2 .

 2 Figure 2. Cascade chain for fingerprint identification

Figure 3 .Figure 4 .

 34 Figure 3. CMC identification performance on database FVC2002DB1

Table I PERFORMANCE

 I EVALUATION OF MATCHING ALGORITHMS IN TERMS OF EER AND COMPUTING TIME t i IN MILLISECOND ON EACH SIMPLE FVC

DATABASE.

Due to confidence issues, we are not allowed to communicate the name of commercial systems.