Computer Aided Verification

We study the verification of properties of communication protocols modeled by a finite set of finite-state machines that communicate by exchanging messages via unbounded FIFO queues. It is well-known that most interesting verification problems, such as deadlock detection, are undecidable for this class of systems. However, in practice, these verification problems may very well turn out to be decidable for a subclass containing most “real” protocols.Motivated by this optimistic (and, we claim, realistic) observation, we present an algorithm that may construct a finite and exact representation of the state space of a communication protocol, even if this state space is infinite. Our algorithm performs a loop-first search in the state space of the protocol being analyzed. A loop-first search is a search technique that attempts to explore first the results of successive executions of loops in the protocol description (code). A new data structure named Queue-content Decision Diagram (QDD) is introduced for representing (possibly infinite) sets of queue-contents. Operations for manipulating QDDs during a loop-first search are presented.A loop-first search using QDDs has been implemented, and experiments on several communication protocols with infinite state spaces have been performed. For these examples, our tool completed its search, and produced a finite symbolic representation for these infinite state

A canonical boolean representation is proposed, which decomposes a function into the conjunction of a sequence of components, based on a fixed variable order. The components can be represented in OBDD form. Algorithms for boolean operations and quantification are presented allowing the representation to be used for symbolic model checking. The decomposed form has a number of useful properties that OBDD's lack. For example, the size of conjunction of two independent functions is the sum of the sizes of the functions. The representation also factors out dependent variables, in the sense that a variable that is determined by the previous variables in the variable order appears in only one component of the decomposition. An example of verifying equivalence of sequential circuits is used to show the potential advantage of the decomposed representation over OBDD's.

In this paper, I show that methods from computational algebraic geometry can be used to carry out symbolic model checking using an encoding of Boolean sets as the common zeros of sets of polynomials. This approach could serve as a useful supplement to symbolic model checking methods based on Ordered Binary Decision Diagrams and may provide important theoretical insights by bringing the powerful mathematical machinery of algebraic geometry to bear on the model checking problem.

Various models and equivalence relations or preorders for probabilistic processes are proposed in the literature. This paper deals with a model based on labelled transition systems extended to the probabalistic setting and gives an O(n2·m) algorithm for testing probabilistic bisimulation and an O (n5·m2) algorithm for testing probabilistic simulation where n is the number of states and m the number of transitions in the underlying probabilistic transition systems.

Games given by transition graphs of pushdown processes are considered. It is shown that if there is a winning strategy in such a game then there is a winning strategy which is realized by a pushdown process. This fact turns out to be connected with the model checking problem for push-down automata and the propositional μ-calculus. It is show that this model checking problem is DEXPTIME-complete.

In computer system design, we distinguish between closed and open systems. A closed system is a system whose behavior is completely determined by the state of the system. An open system is a system that interacts with its environment and whose behavior depends on this interaction. The ability of temporal logics to describe an ongoing interaction of a reactive program with its environment makes them particularly appropriate for the specification of open systems. Nevertheless, model-checking algorithms used for the verification of closed systems are not appropriate for the verification of open systems. Correct model checking of open systems should check the system with respect to arbitrary environments and should take into account uncertainty regarding the environment. This is not the case with current model-checking algorithms and tools. In this paper we introduce and examine the problem of model checking of open systems (module checking, for short). We show that while module checking and model checking coincide for the linear-time paradigm, module checking is much harder than model checking for the branching-time paradigm. We prove that the problem of module checking is EXPTIME-complete for specifications in CTL and is 2EXPTIME-cornplete for specifications in CTL*. This bad news is also carried over when we consider the program-complexity of module checking. As good news, we show that for the commonly-used fragment of CTL (universal, possibly, and always possibly properties), current model-checking tools do work correctly, or can be easily adjusted to work correctly, with respect to both closed and open systems.

Systems with an arbitrary number of homogeneous processes occur in many applications. The Parameterized Model Checking Problem (PMCP) is to determine whether a temporal property is true of every size instance of the system. We consider systems formed by a synchronous parallel composition of a single control process with an arbitrary number of homogeneous user processes, and show that the PMCP is decidable for properties expressed in an indexed propositional temporal logic. While the problem is in general PSPACE-complete, our initial experimental results indicate that the method is usable in practice.

We develop a HORNSAT-based methodology for verification of finite state systems. This general methodology leads naturally to algorithms, that are local [25, 19], on the fly [28, 11, 13, 5] and incremental [24]. It also leads naturally to diagnostic behavioral relation checking

We verify the correctness of an SRT division circuit similar to the one in the Intel Pentium processor. The circuit and its correctness conditions are formalized as a set of algebraic relations on the real numbers. The main obstacle to applying theorem proving techniques for hardware verification is the need for detailed user guidance of proofs. We overcome the need for detailed proof guidance in this example by using a powerful theorem prover called Analytica. Analytica uses symbolic algebra techniques to carry out the proofs in this paper fully automatically.

We describe a formal specification and verification in PVS for the general theory of SRT division, and for the hardware design of a specific implementation. The specification demonstrates how attributes of the PVS language (in particular, predicate subtypes) allow the general theory to be developed in a readable manner that is similar to textbook presentations, while the PVS table construct allows direct specification of the implementation's quotient look-up table. Verification of the derivations in the SRT theory and for the data path and look-up table of the implementation are highly automated and performed for arbitrary, but finite precision; in addition, the theory is verified for general radix, while the implementation is specialized to radix 4. The effectiveness of the automation derives from PVS's tight integration of rewriting with decision procedures for equality, linear arithmetic over integers and rationals, and propositional logic. This example demonstrates that the resources of an expressive specification language and of a general-purpose theorem prover are not inimical to highly automated verification in this domain, and can contribute to clarity, generality, and reuse.

A methodology for mechanically verifying a family of parameterized multiplier circuits, including many well-known multiplier circuits such as the linear array, the Wallace tree and the 7-3 multiplier is proposed. A top level specification for these multipliers is obtained by abstracting the commonality in their behavior. The behavioral correctness of any multiplier in the family can be mechanically verified by a uniform proof strategy. Proofs of properties are done by rewriting and induction using an automated theorem prover RRL (Rewrite Rule Laboratory). The behavioral correctness of the circuits is established with respect to addition and multiplication on numbers. The automated proofs involve minimal user intervention in terms of intermediate lemmas required. Generic hardware components are used to segregate the specification and the implementation aspects, enabling verification of circuits in terms of behavioral constraints that can be realized in different ways. The use of generic components aids reuse of proofs and helps modularize the correctness proofs, allowing verification to go hand in hand with the hardware design process in a hierarchical fashion.

We present an extension to the Murϕ verifier to verify systems with replicated identical components. Verification is by explicit state enumeration in an abstract state space where states do not record the exact numbers of components. Through a new datatype, called RepetitiveID, the user can suggest the use of such an abstraction to verify a system of fixed size. Murϕ automatically checks the soundness of the abstract state graph, and automatically constructs the abstract state graph using the system description.Using a simple run time check, Murϕ can also determine if it can generalize the verification result of a system with fixed size to systems of larger sizes, including the system with infinite number of components.

Recently there have been a lot of progress in technologies for comparing two structurally similar large circuits [2, 14, 13]. Circuits having more than 10,000 gates, whose BDD cannot be built, have been verified in several minutes. However, arithmetic circuit verification with respect to specification is still a hard problem. As shown in [16] some arithmetic circuits, such as multipliers, square function. cube functions, etc., must satisfy some recurrence equations, such as f(x + 1,y=f(x,y) + y where f(x,y)=xy, and those equations can be used for verification. In this paper, we use such recurrence equations in order to drive Boolean comparison problems of structurally similar circuits. That is, left hand sides and right hand sides of equations are realized as separated circuits and then compared. Using the recurrence equation properly, these circuits have many internal equivalent signals and many implications among signals, by which Boolean comparison programs, such as [2, 14, 13], can work very effectively. Using the proposed method, 16-bit multipliers, such as C6288 of ISCAS85 benchmark circuits, are verified within 12 minutes.

The automated deduction and model checking communities have developed techniques that are impressively effective when applied to suitable problems. However, these problems seldom coincide exactly with those that arise in formal methods. Using small but realistic examples for illustration, I will argue that effective deductive support for formal methods requires cooperation among different techniques and an integrated approach to language, deduction, and supporting capabilities such as simulation and the construction of invariants and abstractions. Successful application of automated deduction to formal methods will enrich both fields, providing new opportunities for research and use of automated deduction, and making formal methods a truly useful and practical tool.

We describe a computer-aided verification system which combines deductive with algorithmic (model-checking) verification methods. The system, called tlv (for temporal verification system), is constructed as an additional layer superimposed on top of the cmu smv system, and can verify finite-state systems relative to linear temporal logic (ltl) as well as ctl specifications. The systems to be verified can be either hardware circuits written in the smv design language or finite-state reactive programs written in a simple programming language (spl).The paper presents a common computational model which can support these two types of applications and a high-level interactive language tlv-Basic, in which temporal verification rules, proofs, and complex assertions can be written. We illustrate the efficiency and generality gained by combining deductive with algorithmic techniques on several examples, culminating in verification of fragments of the Futurebus+ system. In the analysis of the Futurebus+ system, we even managed to detect a bug that was not discovered in a previous model-checking analysis of this system.

Our goal is to use a theorem prover in order to verify invariance properties of distributed systems in a “model checking like” manner. A system S is described by a set of sequential components, each one given by a transition relation and a predicate Init defining the set of initial states. In order to verify that P is an invariant of S, we try to compute, in a model checking like manner, the weakest predicate P′ stronger than P and weaker than Init which is an inductive invariant, that is, whenever P′ is true in some state, then P′ remains true after the execution of any possible transition. The fact that P is an invariant can be expressed by a set of predicates (having no more quantifiers than P) on the set of program variables, one for every possible transition of the system. In order to prove these predicates, we use either automatic or assisted theorem proving depending on their nature.We show in this paper how this can be done in an efficient way using the Prototype Verification System PVS. A tool implementing this verification method is presented.

We present an extension of classical tableau-based model checking procedures to the case of infinite-state systems, using deductive methods in an incremental construction of the behavior graph. Logical formulas are used to represent infinite sets of states in an abstraction of this graph, which is repeatedly refined in the search for a counterexample computation, ruling out large portions of the graph before they are expanded to the state-level. This can lead to large savings, even in the case of finite-state systems. Only local conditions need to be checked at each step, and previously proven properties can be used to further constrain the search. Although the resulting method is not always automatic, it provides a flexible and general framework that can be used to integrate a diverse number of other verification tools.

Theories with associative and commutative (AC) operators, such as arithmetic, process algebras, boolean algebras, sets, ... are ubiquitous in software and hardware verification. These AC operators are difficult to handle by automatic deduction since they generate complex proofs. In this paper, we present new techniques for combining induction and AC reasoning, in a rewrite-based theorem prover. The resulting system has proved to be quite successful for verification tasks. Thanks to its careful rewriting strategy, it needs less interaction on typical verification problems than well known tools like NQTHM, LP or PVS. We also believe that our approach can easily be integrated as an efficient tactic in other proof systems.

We adapt a generic minimal model generation algorithm to compute the coarsest finite model of the underlying infinite transition system of a timed automaton. This model is minimal modulo a time-abstracting bisimulation. Our algorithm uses a refinement method that avoids set complementation, and is considerably more efficient than previous ones. We use the constructed minimal model for verification purposes by defining abstraction criteria that allow to further reduce the model and to compare it to a specification.

In this paper we apply the tool Uppaal1 to an automatic analysis of a version of the Philips Audio Control Protocol with two senders and bus collision handling. This case study is significantly larger than the real-time/hybrid systems previously analysed by automatic tools. During the case study the tool Uppaal was extended with a new feature, committed locations, allowing efficient modelling of broadcast communication.

In this work we propose a verification methodology consisting of selective quantitative timing analysis and interval model checking. Our methods can aid not only in determining if a system works correctly, but also in understanding how well the system works. The seleptive quantitative algorithms compute minimum and maximum delays over a selected subset of system executions. A linear-time temporal logic (LTL) formula is used to select either infinite paths or finite intervals over which the computation is performed. We show how tableaux for LTL formulas can be used for selecting either paths or intervals and also for model checking formulas interpreted over paths or intervals.To demonstrate the usefulness of our methods we have verified a complex and realistic distributed real-time system: Our tool has been able to analyze the system and to compute the response time of the various components. Moreover, we have been able to identify inefficiencies that caused the response time to increase significantly (about 50%). After changing the design we not only verified that the response time was lower, but were also able to determine the causes for the poor performance of the original model using interval model checking.

We present a logical formalism for expressing properties of continuous time Markov chains. The semantics for such properties arise as a natural extension of previous work on discrete time Markov chains to continuous time. The major result is that the verification problem is decidable; this is shown using results in algebraic and transcendental number theory.

This paper presents an approach to verifying that a circuit as described by a continuous, differential equation model is a correct implementation of a discrete specification. The abstraction from continuous trajectories to discrete traces is based on topological features of the continuous model rather than quantizing the continuous phase space. An practical verification method based on numerical integration is presented. The method is demonstrated by the verification that a toggle circuit satisfies a discrete specification.

This paper presents a methodology for the verification of temporal properties of systems based on the gradual construction and algorithmic checking of fairness diagrams. Fairness diagrams correspond to abstractions of the system and its progress properties, and have a simple graphical representation.In the proposed methodology, a proof of a temporal property consists of a chain of diagram transformations, starting from a diagram representing the original system and ending with a diagram that either corresponds directly to the specification, or that can be shown to satisfy it by purely algorithmic methods. Each diagram transformation captures a natural step of the gradual process of system analysis and proof discovery. The structure of fairness diagrams simplifies reasoning about progress properties, and the graphical representation provided by the diagrams enables the user to direct the construction of the proof. The resulting methodology is complete for proving specifications written in first-order lineartime temporal logic, provided no temporal operator appears in the scope of a quantifier.

We present a new approach for using a theorem-prover to verify the correctness of protocols and distributed algorithms. The method compares a state graph of the implementation with a specification which is a state graph representing the desired abstract behavior. The steps in the specification correspond to atomic transactions, which are not atomic in the implementation.The method relies on an aggregation function, which is a type of an abstraction function that aggregates the steps of each transaction in the implementation into a single atomic transaction in the specification, The key idea in defining the aggregation function is that it must complete atomic transactions which have committed but are not finished.We illustrate the method on a simple but nontrivial example. We have successfully used it for other examples, including the cache coherence protocol for the Stanford FLASH multiprocessor.

Assertional methods tend to be useable for abstract, coarse-grained versions of concurrent algorithms, but quickly become intractable for more realistic, finer-grained implementations. Various trace-reduction methods have been proposed to transfer properties of coarse-grained versions to finer-grained versions. We show that a more direct approach, involving the explicit construction of an (inductive) invariant for the finer-grained version, is theoretically more powerful, and also more appropriate for computer-aided verification.

When proving invariance properties of programs one is faced with two problems. The first problem is related to the necessity of proving tautologies of the considered assertion language, whereas the second manifests in the need of finding sufficiently strong invariants. This paper focuses on the second problem and describes techniques for the automatic generation of invariants. The first set of these techniques is applicable on sequential transition systems and allows to derive so-called local invariants, i.e. predicates which are invariant at some control location. The second is applicable on networks of transition systems and allows to combine local invariants of the sequential components to obtain local invariants of the global systems. Furthermore, a refined strengthening technique is presented that allows to avoid the problem of size-increase of the considered predicates which is the main drawback of the usual strengthening technique. The proposed techniques are illustrated by examples.

Checking that a given finite state program satisfies a linear temporal logic property suffers from a severe space and time explosion. One way to cope with this is to reduce the state graph used for model checking. We present an algorithm for constructing a state graph that is a projection of the program's state graph. The algorithm maintains the transitions and states that affect the truth of the property to be checked. The algorithm works in conjunction with a partial order reduction algorithm. We show a substantial reduction in memory over current partial order reduction methods, both in the precomputation stage, and in the result presented to a model checker, with a price of a single additional traversal of the graph obtained with partial order reduction. As part of our space-saving methods, we present a new way to exploit Holzmann's Bit Hash Table, which assists us in solving the revisiting problem.

In this paper we attempt to demonstrate that on-the-fly techniques, developed in the context of verification, can help in deriving test suites. Test purposes are used in practice to select test cases according to some properties of the specification. We define a consistency pre-order linking test purposes and specifications. We give a set of rules to check this consistency and to derive a complete test case with preamble, postamble, verdicts and timers. The algorithm, which implements the construction rules, is based on a depth first traversal of a synchronous product between the test purpose and the specification. We shortly relate our experience on an industrial protocol with TGV, a first prototype of the algorithm implemented as a component of the C ADP toolbox.

This paper presents a method for automatically translating natural language specifications into temporal logic. Using this method, users may express complex specifications in relatively free natural language, allowing multi-sentence specifications, the use of pronouns instead of repeating the description of previously mentioned objects and complex temporal relations. These specifications are translated into temporal logic, while ensuring the correctness of the translation. This approach overcomes a well-known obstacle of applying model-checking industrially. In contrast to prior attempts, the translation is linguistically based on a modern formalism for discourse representation. An implementation of this translation method is presented in one of the modern computational linguistics systems.

In program verification, we check that an implementation meets its specification. Both the specification and the implementation describe the possible behaviors of the program, though at different levels of abstraction. We distinguish between two approaches to implementation of specifications. The first approach is trace-based implementation, where we require every computation of the implementation to correlate to some computation of the specification. The second approach is tree-based implementation, where we require every computation tree embodied in the implementation to correlate to some computation tree embodied in the specification. The two approaches to implementation are strongly related to the linear-time versus branching-time dichotomy in temporal logic.In this work we examine the trace-based and the tree-based approaches from a complexity-theoretic point of view. We consider and compare the complexity of verification of fair transition systems, modeling both the implementation and the specification, in the two approaches. We consider unconditional, weak, and strong fairness. For the trace-based approach, the corresponding problem is language containment. For the tree-based approach, the corresponding problem is fair simulation. We show that while both problems are PSPACE-complete, their complexities in terms of the size of the implementation do not coincide and the trace-based approach is more efficient. As the implementation is normally much bigger than the specification, we see this as an advantage of the trace-based approach. Our results are at variance with the known results for the case of transition systems with no fairness, where the tree-based approach is more efficient.

The number of installations of the Spin model checking tool is steadily increasing. There are well over two thousand installations today, divided roughly evenly over academic and industrial sites. The tool itself also continues to evolve; it has more than doubled in size, and hopefully at least equally so in functionality, since it was first distributed in early 1991. The tool runs on most standard workstations, and starting with version 2.8 also on standard PCs.In this overview, we summarize the design principles of the tool, and review its current state.

This is a brief overview of the Murϕ verification system.

The NCSU Concurrency Workbench is a tool for verifying finite-state systems. A key feature is its flexibility; its modular design eases the task of adding new analyses and changing the language users employ for describing systems. This note gives an overview of the system's features, including its capacity for generating diagnostic information for incorrect systems, and discusses some of its applications.

The Concurrency Factory supports the specification, simulation, verification, and implementation of real-time concurrent systems such as communication protocols and piocess control systems. While the system uses process algebra as its underlying design formalism, the primary focus of the project is practical utility: the tools should be usable by engineers who are not familiar with formal models of concurrency, and it should be capable of handling large-scale systems such as those found in the telecommunications industry.This paper serves as a status report for the Factory project and briefly describes a case-study involving the GNU UUCP i-protocol.

We present XVERSA, a set of tools for the specification and analysis of resource-bound real-time systems. XVERSA facilitates the use of the Algebra of Communicating Shared Resources (ACSR), a real-time process algebra with explicit notions of resources and priority. A text based user interface supports syntax checking, analysis based on equivalence checking, state space exploration, and algebraic rewriting. A graphical user interface allows systems to be described and analyzed using intuitive pictorial representations of ACSR language elements.

EVP is an integrated tool-set for specification and the analysis of communication protocols and distributed systems. Specifications in standard Formal Description Techniques (FDTs) like SDL or LOTOS are translated into a common language, and then analysed with tools for this internal representation. The common language is a concurrent logic language specially designed for distributed programming. The analysis consists in interactive simulation and automatic verification.

The Stanford Temporal Prover, STeP, combines deductive methods with algorithmic techniques to verify linear-time temporal logic specifications of reactive and real-time systems. STeP uses verification rules, verification diagrams, automatically generated invariants, model checking, and a collection of decision procedures to verify finite- and infinite-state systems.

Symbolic model checking is a powerful formal specification and verification method that has been applied successfully in several industrial designs. Using symbolic model checking techniques it is possible to verify industrial-size finite state systems. State spaces with up to 1030 states can be exhaustively searched in minutes. Models with more than 10120 states have been verified using special techniques.Several extensions to the original technique have been developed, making it even more powerful. Timing properties can be verified by performing a quantitative timing analysis [3, 5]. The designer can then analyze the performance of a system and gain insight in how well a system works early in the design process. Word-level model checking allows the verification of datapaths in addition to control [12]. Symmetry [8], abstraction [10, 15] and compositional reasoning [15] techniques significantly extend the power of model checking by exploiting the hierarchical structure of complex circuit designs and protocols.More information about SMV, as well as the source code for the model checker can be found at: http://www.cs.cmu.edu/∼modelcheck

COSPAN (Coordination Specification Analizer [AKS83]) is an algorithmic computer-aided verification system. It's semantic model [Ku94] is founded on ω-automata: for a process P (modelling a system to be verified) and a task T which P is intended to perform, verification consists of the automata language containment test $$\mathcal{L}(P) \subset \mathcal{L}(T).$$ If the test fails, COSPAN presents an error track which illustrates the error. Typically, P is not monolithic, but is represented as a (“synchronous”) parallel composition P=P₁⊗...⊗P _k of component processes (all modelled as ω-automata). Asynchronous coordination of component processes may be modelled through nondeterminism in the components. The process model can be set either to Mealy or Moore machines.COSPAN has been used on commercial applications for over a decade, both for software and hardware design verification [HK90]. Recently, it has been implemented as the “verification engine” in the commercial hardware verification tool FormalCheckTM, which is supported for hardware verification by the Bell Labs Design Automation center.The COSPAN application domains and utilities are enumerated.

Our experience in using the RTGIL tools has shown that these tools and the graphical representation of the logic are very helpful for specifying and verifying properties of concurrent real-time systems. In addition to the aircraft example, we have used these tools to specify and verify properties of a railroad crossing system, a robot, an alarm system, and a four-phase handshaking protocol.The RTGIL tools are implemented in Lucid Common Lisp and also in Franz Allegro Common Lisp, and require at least 32 MBytes of main memory and 64 Mbytes of swap space. The graphical editor was implemented using the Garnet graphics toolkit

Formal methods are recognized as the most promising way to produce high assurance software systems. In reality this fact is not enough to convince industry to use them. Formal methods must be applicable and usable in several areas (security, safety), engineers have to accept a change in software development work but should not be asked to give up the environment they are used to and bosses must realize that higher effort during the design phase can save money and time later. This paper describes the recently completed formal specification and verification tool Verification Support Environment (VSE). An advantage of the design of the VSE tool is the possibility of using formal and semiformal development methods combined in a unique working environment. After official release of the VSE-system March 1995 several pilot projects were carried out with industry. The paper gives an overview of the VSE-system and describes the results of the pilot applications.

This paper presents the structure of our tool Marrella the construction of which has been motivated by practical problems in the context of simulation and parallel program debugging, where the correct evaluation of global properties requires a careful analysis of the causal structure of the execution. The underlying model is based on prime event structures that are considered as exhibiting all the behaviors of distributed programs: the tool gives the possibilities of generating one, some or all of their executions. On one hand, a careful implementation spares memory; on the other hand, precise and neat algorithms benefit from the trace properties of prime event structures and thus gain in avoiding the enumerations of equivalent interleavings.

We describe our experience in the mechanical verification of the safety invariants of an asynchronous garbage-collection algorithm [1], using the TLP system [2]. We only give a cursory overview of the algorithm and its formalisation. Our main focus is on the lessons learned from carrying a sizeable (22,000+ lines) formal proof through an off-the-shelf prover. In particular, we found the TLP style of structured proofs to be particularly effective for organising, writing, and managing proof scripts.

As shown above, verification of temporal properties on behaviour abstractions is suitable for detecting service interactions. In the example that we briefly explained the abstraction step was not really necessary, for the example itself is small enough to check temporal properties directly on the behaviour.A complete analysis of the BCSM model already leads to a behaviour representation having several thousand states. Including services, we expect several tenthousand states. This reaches an order of magnitude of the number of states that makes abstraction techniques absolutely necessary. Here, even the analysis of the specification can become difficult with respect to complexity. Hence, a compositional analysis technique of specifications that allows to compute a representation of an abstract behaviour without exhaustive construction of the complete state space is currently developed [Och95]. We expect that our approach will allow us to check several combinations of services for undesired interactions where any direct verification approach without abstractions would be intractable.