Formal Verification of Autonomous Systems
`NASA Intelligent Systems Program
`
`Edmund Clarke, David Garlan, Bruce Krogh,
`Reid Simmons, and Jeannette Wing
`
`Computer Science Department
`Institute for Software Research, International
`Electrical and Computer Engineering Department
`The Robotics Institute
`
`Carnegie Mellon University
`Pittsburgh, PA 15213
`
`September 25, 2001
`
`1 Abstract
`
`The success of safety-critical NASA missions depends on reliable software. As both space and
`ground software systems become more complex, and increasingly more autonomous, guarantees
`of software correctness becomes even more crucial. While traditional approaches to validation
`– simulation and testing – are useful, they cannot, in general, be used to check all possible sce-
`narios. Formal verification techniques, such as model checking, can complement such validation
`approaches by providing guarantees that certain system properties hold (such as absence of dead-
`lock or resource contention).
`While completely verifying large software systems is infeasible, guaranteeing properties of
`critical components of a system can yield huge payoffs. We propose to develop new verifica-
`tion techniques and tools that enable semantic analyses of complex, time-dependent software, and
`which can be used routinely by software engineers during design and development to check for
`critical system errors. Detecting such design flaws early in the development process can reduce
`the cost of later validation efforts. Traditional simulation and testing can then be more narrowly
`focused on those areas that formal verification does not readily handle.
`Autonomous systems are concurrent and distributed tasks that must operate robustly and in real
`time. They must actively manage limited physical resources such as power, devices, and communi-
`cation. They must sense and act in environments that have complex, potentially uncertain, dynam-
`ics. We will focus our efforts on verifying the part of autonomous space systems that interact with
`
`1
`
`Page 1 of 17
`
`Mercedes Exhibit 1026
`
`

`
`the environment. Task executives decide how to act (and react) in response to sensory information.
`Their behavior is complicated by concurrency, distributed processing, limited resources, and oper-
`ating in a rich, complex environment. Our research focus on environmental interaction will address
`important, space-relevant issues, including modeling uncertainty and continuous dynamics.
`Our approach to verification of such systems is two-pronged:
`
`1. We will adapt methods for formal verification (model checking) and integrate them with
`other techniques (such as Markov models, control flow analysis, and theorem proving) to
`develop powerful new tools, usable by space engineers, for verifying properties related to
`control flow, communication protocols, and resource usage.
`
`2. We will develop fundamental new verification techniques for analyzing system interaction
`with the environment. In particular, we will develop formal verification techniques for hybrid
`and probabilistic models. In these cases, we will use NASA problems to focus the research.
`As these new techniques mature, we will encapsulate them in semantic analysis tools, as
`described above.
`
`Specifically, this proposal addresses concerns in Automated Reasoning related to automated
`verification of autonomous systems, formal specification languages for describing software, and
`advanced development environments to facilitate rapid (and reliable!) development of autonomous
`software. We expect that this work will also have longer-term downstream impact on industry
`for the development of robust commercial autonomous and embedded real-time systems. It also
`complements ongoing work at NASA Ames to verify other aspects of autonomous systems (such as
`the diagnostic component). While formal verification is not a panacea, its regular use by developers
`can go a long way towards helping to create reliable and robust software systems.
`
`2 Objectives
`
`The success of safety-critical NASA missions depends on reliable software. As both space and
`ground software systems become more complex, and increasingly more autonomous, guarantees
`of software correctness become even more crucial. While traditional simulation and testing are
`useful validation methodologies, in general they are expensive, time consuming, and cannot pro-
`vide guarantees of system correctness.
`In contrast, formal verification tools like model checking can be used to provide guarantees in
`terms of certain models of software systems and to identify serious system flaws [10]. To date,
`however, such techniques have not been widely applied to space applications, due to the difficulty
`of creating appropriate and tractable models of software systems and their interactions with the
`environment. We propose to develop novel techniques and tools that address the difficulties of
`modeling and verifying real-time system interactions with uncertain environments. Our long-term
`goal is to enable developers of autonomous systems to use tools based on formal methods rou-
`tinely. Just as engineers now rely on compilers to provide syntactic analyses of programs, we
`envision engineers in the future relying on formal verification tools to provide semantic analy-
`ses (and explanations) of complex spacecraft software. The results will complement traditional
`validation techniques, resulting in much more reliable software at lower overall development cost.
`The main thrusts of this proposal are
`
`2
`
`Page 2 of 17
`
`

`
`Autonomous System
`
`Environment
`
`System Integrity Properties
`
`Modeling the Environment
`
`Communication
`Protocols
`Architecture
`
`Resources
`
`Control Flow
`Exceptions
`
`Task Sychronization
`
`System−Environment
`Interactions
`Hybrid Dynamics
`
`Modeling Uncertainty
`
`Stochastic Models
`
`Foundational Technology
`Model checking techniques and tools
`Task−level system architecture, task executive languages
`Compilation techniques
`Continuous domains, quantitative analysis, reliability analysis
`
`Figure 1: Overview of Our Verification Research Plan
`
`(cid:15) To target general verification techniques on several key aspects of autonomous systems:
`communication, control flow, and resource usage. This thrust is illustrated in Figure 1 in the
`left-hand box labeled “System Integrity Properties,” since we are concerned with knowing
`whether the system is internally correct.
`
`(cid:15) To develop novel verification techniques for reasoning about system/environment interac-
`tions, especially for largely unpredictable and continuously-varying environments. Here,
`fundamental research is needed to develop models for representing the interactions and al-
`gorithms for verifying those models effectively and efficiently. This thrust is illustrated in
`Figure 1 in the right-hand box labeled “Modeling the Environment.” We will explore both
`hybrid models to handle continuous dynamics and stochastic models to deal with uncertainty.
`
`The bottom box in Figure 1 illustrates the foundational building blocks that we rely on to
`support these two thrusts of our research. First, model checking is central to our project: We have
`developed, and continue to develop, new data structures for representing large state spaces, new
`algorithms for analyzing our models, and new tools that perform automated verification. Second,
`the level of abstraction of our models is the task-level: Rather than focus on verifying source
`code, our research is focused on verifying higher-level descriptions of task-level architectures in
`terms of task executive languages. Third, we integrate model checking with other relevant analysis
`techniques: For instance, we use control flow graph construction techniques from the compiler
`community to help generate abstract models automatically. Finally, our work on specifying and
`verifying resource constraints and interactions between a system and its environment relies on
`continuous mathematics to support hybrid dynamics analysis, quantitative analysis, and reliability
`analysis.
`
`3
`
`Page 3 of 17
`
`

`
`3 Technical Approach
`
`A critical capability of space systems is task execution – carrying out planned activities. Examples
`include orbital and “delta-V” maneuvers, planetary navigation, and automated science experiments
`on space stations. Task execution is a special concern for autonomous systems because their tasks
`are typically more complex and their plans are typically more sophisticated – including conditional
`execution and dynamic handling of contingencies. Also, task activities are often scheduled with
`high degrees of flexibility, which makes it difficult to know which activities could possibly overlap
`and potentially interfere with each other.
`As noted above, we propose to focus on aspects of both internal and external interactions that
`are central to the successful execution of task plans:
`
`1. System Integrity: Communication is critical because task execution software is typically dis-
`tributed, in order to handle concurrent tasks and react in real time to exceptional situations.
`Verifying control flow is critical because the combination of distribution, concurrency, real
`time, and exceptional situations makes the space of reactions to situations very large and
`difficult to comprehend. Reasoning about resource constraints is critical because space sys-
`tems typically have strict limits on resources. Such constraints can refer to both continuous
`(power, computation, storage) and discrete (cameras, motors) physical resources.
`
`2. Environmental Interactions: At the core, the correctness of an autonomous space system
`depends on how it interacts with its environment. The system must behave in such a way
`as to achieve its goals while maintaining its own health and safety. This is complicated by
`the fact that the environment is uncertain, and that the combination of the system and its
`environment is a hybrid (discrete/continuous) system. For instance, the way a rover should
`drive depends on the slope and type of terrain, as well as the status of its motors. This
`is further complicated by the fact that the roll/pitch sensors may be noisy, and often have
`significant latency.
`
`Of these problems, current model-checking techniques are in principle well-suited for verify-
`ing system integrity properties. Issues include formalizing the appropriate behaviors (both nominal
`and exceptional) and dealing with issues of concurrency, distribution, and real time. For many of
`these problems, it will be necessary to integrate model-checking techniques with other analysis
`techniques (such as control flow analysis). We will look at verifying both publish-subscribe com-
`munication systems (a popular architecture for implementing distributed autonomous systems) and
`real-time, fault-tolerant communication protocols. We will investigate techniques to automate the
`checking of properties having to do with handling of exceptions, synchronizing tasks, and resource
`utilization, leading to effective tools that can be used by spacecraft engineers. Section 3.1 describes
`our research plan to address these system integrity issues.
`Much more difficult is the problem of verifying the system’s interaction with its environment.
`Here, we will address two inherent characteristics of a space system’s environment: continuous
`dynamics, for which we will generate approximate discrete models from the continuous dynamic
`models (differential equations), and uncertainty, for which we will accommodate using stochastic
`models. This part of the work is more fundamental in nature, and will have wide and far-reaching
`applicability for verification of autonomous and real-time software systems. Section 3.2 describes
`our research plan to address these environmental interaction issues.
`
`4
`
`Page 4 of 17
`
`

`
`3.1 System Integrity
`
`Most autonomous systems are constructed as loosely coupled, distributed subsystems. The subsys-
`tems communicate with one another, synchronize their activities for both nominal and exceptional
`situations, and share resources. Software errors that cause such systems to misbehave often arise
`from subtle interactions amongst the concurrent subsystems (e.g., race conditions, missed events,
`deadlocks, resource contention, etc.). Since these bugs may manifest themselves only for particular
`interleavings of actions, the programmer may not be able to reproduce the problem at will. Thus,
`it is often difficult to track down the sources of bugs in task executives using traditional testing and
`code inspection techniques.
`Fortunately, such problems are particularly well suited to automated formal verification using
`model checking. Model checking starts with a finite state model of the software system under
`consideration. The model-checking tool then examines all possible interleavings of computations
`in the model in order to expose any violations of task synchronization constraints. To the extent
`that the model faithfully reflects the actual system, errors found in the model represent problems
`with the system and vice versa.
`Unfortunately, model checking is only useful when one has first created a model to check. For
`large, complex systems the creation of such models is often a formidable task, since one must find
`a way to reduce the infinite state software system to a model with finite state. This is challenging
`because the model must be rich enough to exhibit the class of problem that one wants to check,
`while simple enough (in terms of the size of its state space) that checking it is tractable using
`current model checking technology.
`We propose to tackle this problem by focusing on models that expose aspects of the system that
`are the most frequent sources of errors. Specifically, we plan to develop the underlying scientific
`base and tools to verify three critical aspects: system communication, control flow, and resource
`utilization. By focusing on these limited, but critical, areas we believe that we can make progress
`in the larger goal of verifying autonomous system behavior as a whole.
`
`3.1.1 Verifying Communication
`
`Verifying Publish-Subscribe Systems
`
`We propose to develop automated model generators for publish-subscribe and cyclic-task soft-
`ware architectures. To support coordination among behaviors, while maintaining loose coupling
`between tasks, autonomous systems often adopt one of two forms of component integration:
`
`1. Using publish-subscribe interaction [17, 41] tasks are responsible for announcing (or “pub-
`lishing”) significant events. Other tasks may register to be informed of (or “subscribe to”)
`a set of events. When one task publishes an event, it is sent to all subscribers. In this way
`tasks remain independent since a publisher does not know the identity, or even existence, of
`other subscriber tasks.
`
`2. Using cyclic tasks with shared variables, a similar effect is typically achieved by assigning
`each task to a task slot that is repeatedly run at some fixed period – say every 50 milliseconds.
`At each activation a task examines a set of input variables in some shared variable space and,
`based on those values, it writes derived values to a set of output variables. Readers of shared
`
`5
`
`Page 5 of 17
`
`

`
`variables do not know which tasks set those values, or which tasks will “consume” the values
`of the variables to which they write. Thus, the shared variables serve the role of the events
`in the publish-subscribe architectures of autonomous systems.
`
`While both architectures are good from an engineering point of view, reasoning about their
`aggregate behavior is problematic. For example, one would like to be able to guarantee that if
`a sensor detects that a temperature value goes over a maximum limit then some other part of
`the system will take appropriate corrective action to preserve overall stability. This is hard to
`do with such systems, however, because interactions between the parts of the system are indirect
`and asynchronous. In particular, the non-determinism inherent in the invocation of tasks and the
`communication delays inherent in a distributed publish-subscribe system (many events may be in
`transit) make it difficult to reason about properties such as global invariants or timely response to
`certain trigger events. (For example: Are sufficient events published to allow interested parties
`to respond in a timely fashion? Is there potential interference between components that subscribe
`to the same event?) Analogously, for shared-variable cyclic systems it is difficult to determine
`whether a given assignment of tasks to periodic buckets and the ordering of tasks within a bucket
`are sufficient to guarantee some property under all possible scenarios. (For example: Are there
`implicit ordering assumptions in the reading and writing of shared variables that may be violated?)
`While model checking appears to be a good solution for verification of such properties, it is
`not immediately obvious how to map these kinds of systems into appropriate models. In previous
`research we have developed techniques for reasoning about such systems [13, 12]. The basic idea
`underlying the work is that one can provide a precise description of the cause and effect of each
`event to reason locally about how a component behaves in isolation. Then, using local correctness
`of the components and properties of events, we can infer the desired global property of the overall
`system. We believe it should be possible to map these descriptions automatically into a form
`that can be model checked. Moreover, many of the standard problems about event ordering and
`interference (mentioned above) can be built in as standard checks that are automatically verified.
`Over the past year we have made progress in this area by creating a prototype model checker
`for publish-subscribe systems. Although still primitive, it provides a starting point for further in-
`vestigation of ways of checking key properties and for extracting the necessary model information
`from existing publish-subscribe systems [16].
`
`Verifying Real-Time, Fault-Tolerant Protocols
`
`Mission critical components are frequently connected by digital communication busses. The
`failure of such a bus is not tolerable, therefore redundant busses are often used in safety-critical
`environments to handle device faults. Besides fault tolerance, many applications require real-time
`guarantees such as a deterministic message latency. There are various protocols for such purposes,
`with different complexities, which are used by the avionics industry, such as Airbus and Boeing.
`Boeing is using the ARINC 629 bus for the new fly-by-wire aircraft, such as the Boeing 777
`(http://www.boeing.com). Other protocols for this domain are the Time Triggered Architecture
`(TTA) protocols [25, 1] and FlexRay [5].
`FlexRay is a new real-time protocol, not yet released to the public, being developed by a con-
`sortium of companies. Although used primarily for automotive applications, it is representative of
`state-of-the-art safety critical real-time protocols. The goal of the project is to verify formally the
`specification and the reference models for the FlexRay Protocol. The reference models are defined
`
`6
`
`Page 6 of 17
`
`

`
`in the ANSI-C language and in VHDL. While model-checking yields good results when applied to
`hardware, software is still a major challenge because of the huge state spaces that must be covered.
`We have succeeded in verifying critical parts of a protocol that uses the Time Triggered Architec-
`ture (TTP/C), and both the software and hardware reference models for the calculation of the error
`detection code of the FlexRay protocol.
`Further work includes the formal verification of the specification of the FlexRay protocol, in
`particular, we will be investigating the new fault tolerant clock synchronization mechanism, and
`larger parts of the reference models. For this task, we plan to use a combination of model-checking
`and theorem proving. The theorem proving part of the tool will allow for compositional reasoning,
`while powerful decision procedures will provide a high degree of automation.
`
`3.1.2 Verifying Control Flow
`
`Verifying Exception Handling
`
`Detecting and reacting to exceptional situations is critical for autonomous systems. Handling
`such exceptions typically introduces non-local flow of control in the system, leading to situations
`in which capabilities are exercised in unexpected contexts. Such situations have the potential of
`producing catastrophic consequences, but they are typically difficult to detect and analyze at design
`time due to the non-locality of the control flow. The problem is further exacerbated by the presence
`of concurrent tasks.
`Fortunately, task-executive languages, such as ESL [18] and TDL [38] (as well as many modern
`programming and design languages), include explicit constructs for exception handling. These
`typically adopt a termination model of exception handling (in which a raised exception terminates
`the block in which the exception was raised), with dynamically scoped exception handlers. We
`can make use of syntactic constructs to (a) constrain the types of control flow that we need to
`analyze and (b) automate the construction of formal models needed for verification. Given these
`models, the verification problem is similar to other aspects of autonomous systems: We desire to
`know whether the exception handling is complete (i.e., all exceptions have associated handlers)
`and whether the system performs correctly in the presence of exceptions (e.g., are resources used
`correctly, or are task synchronization constraints adhered to).
`Our approach is to define an Intermediate Exception Language (IEL) that captures the syn-
`tax and semantics of the various task executive and programming languages under consideration.
`Recent work in compilers has developed an algorithm for creating control-flow graphs that take
`exception handling constructs into account [40]. Such control-flow graphs can be analyzed for
`certain types of static properties of interest (such as determining whether all exceptions will be
`caught by some handler).
`We propose to extend this work in several ways to make it more useful for verification of au-
`tonomous systems. First, we will extend the control-flow graph generation algorithm to handle
`the resumption model of exception handling. We will further extend the algorithm to deal with
`concurrent tasks, where one task might throw an exception caught by another task. More impor-
`tantly, we will provide methods for annotating the control-flow graph with state information (such
`as resource utilization), and use the annotated control-flow graphs to construct finite-state models
`that can be model-checked for temporal properties of interest (such as absence of deadlock in con-
`
`7
`
`Page 7 of 17
`
`

`
`Control
`Flow
`Analysis
`
`Model
`Checker
`
`Verified Static
`Properties
`
`Verified Temporal
`Properties
`
`Counterexamples
`
`Explanation Generator
`
`Specifications
`
`IEL
`
`Control
`Flow
`Generator
`
`Translator
`
`C++
`Java
`ESL
`TDL
`System Design
`
`Figure 2: Verifying Static and Temporal Properties Associated with Exception Handling
`
`current situations, or that all acquired resources will eventually be released before they are needed
`again). Important aspects of the research will involve identifying the types of state information
`that make the approach both tractable and useful to system designers and developers, and deter-
`mining classes of properties that can be feasibly checked. Our overall approach to this problem is
`illustrated in Figure 2.
`Over the past year we have made some progress in this area by identifying appropriate model
`construction algorithms and developing a preliminary design for the IEL.
`
`Verifying Task Synchronization
`
`Task synchronization is an important aspect of task execution. In many cases, specialized lan-
`guages, such as RAPs [15], ESL [18], and TDL [38], are used to implement task executives for
`autonomous systems. In such languages, the synchronization constraints are explicit, so extraction
`and translation of constraints are facilitated. In previous research at Carnegie Mellon, in collabora-
`tion with Ames [33, 39], we developed a tool to produce SMV models automatically from models
`written in MPL, the language used in the Livingstone fault diagnosis system [42].
`We propose to create similar translators for task execution languages. The difficulty here is
`that such languages are typically quite expressive (including conditional, iterative, and recursive
`constructs), and care must be taken to produce models at the right level of abstraction so that they
`can be verified efficiently. In addition, we propose to develop specialized languages to enable
`engineers to encode properties of interest easily. In some cases, we will extend the task execution
`languages so as to be able to support directly the inclusion of such properties, much as the “assert”
`property in C. To test the approach, we will focus on being able to encode flight rules from various
`missions, such as DS1.
`
`3.1.3 Verifying Resource Constraints
`
`Space systems are typically resource-limited, and so autonomous space systems must be concerned
`with resource allocation, ensuring that they do not exceed resource bounds. While the use of
`autonomous planning and scheduling can significantly decrease resource conflicts [31], problems
`can still arise [32]. Model checking is particularly well suited for detecting potential violations of
`
`8
`
`Page 8 of 17
`
`

`
`resource constraints because it can examine all possible execution traces and interleavings of tasks.
`Resources can be categorized into four types [11]:
`
`1. Single sharable – a discrete, single unit, such as a camera. Sharable resources can be used
`by only a single task at any given time.
`2. Multiple sharable – multiple discrete units, such as a team of rovers exploring a planetary
`surface. Multiple sharable resources may be interchangeable, but difficulties arise when the
`resources are interchangeable for some purposes but not others (e.g., wheeled rovers, but
`with different sensors).
`3. Consumable – continuous resource, such as fuel. Consumable resources can be used for any
`task, at any time, but eventually can be used up.
`4. Renewable – continuous resource that can be replenished, such as disk space or telemetry
`bandwidth. Renewable resources are critical in space systems, and must be very carefully
`managed to avoid over-subscription.
`
`It is conceptually straightforward to use model checking for verifying resource constraints.
`Single sharable resources can be synchronized using a mutex Boolean variable. Multiple sharable
`resources can be represented using an integer variable with a given, finite range. Although, in
`general, allocating multiple sharable resources is a computationally complex problem, verifying
`the absence of resource conflicts is no more difficult than other discrete, symbolic model-checking
`problems. To reason about continuous (consumable and renewable) resources, algorithms for real-
`time model checking can be adapted [23, 6]. In many cases, resources are consumed and renewed
`at a constant rate and their constraints are independent. This corresponds to multi-rate clocks, or
`rectangular automata, for which many verification problems of practical interest are decidable [3,
`20]. Consumption and renewal rates that are not constant can be modeled in this framework using
`piecewise constant approximations.
`Our research on resource constraints will develop three innovations: (1) verification of resource
`constraints for multiple scheduled current threads of control in the task executive; (2) quantifying
`the satisfaction and violation of resource constraint violations; (3) new schemes for specifying
`resource constraints and interpreting verification results.
`The first innovation addresses the problems that arise when complex task executives involving
`several parallel threads of execution are implemented using a particular scheduling paradigm. In
`a current project sponsored by the DARPA MoBIES program, we have addressed this issue in
`the context of real-time embedded systems. For this application, we have developed a new tool
`that combines model checking with rate monotonic analysis. Most existing approaches to worst-
`case execution time analysis (WCET) [14] rely on simulation or static analysis techniques and
`require a high degree of user interaction (for instance, it is common to have the user annotate
`while loops with an upper limit of the number of iterations). In contrast, we use symbolic (BDD)
`based techniques to compute task-level worst-case execution times automatically from execution
`times of basic blocks. Computation time of basic blocks is obtained from assembly code analysis.
`Execution time information is used in a rate monotonic schedulability analysis [28] tool to generate
`a scheduler that is combined with the code representations for model checking. This makes it
`possible to verify properties of the system, as it will execute using this scheduling mechanism. We
`propose to develop a similar approach to analyzing multi-threaded task executives by automatically
`
`9
`
`Page 9 of 17
`
`

`
`generating faithful representations of the actual mechanisms used to manage the shared processing
`resources in these systems.
`The second innovation addresses the degree to which constraints on consumable resources are
`used by the system. Often, it is important to know not just whether a resource constraint has
`been violated, but how close one is to a violation in the best and worst cases. We propose to
`deliver this quantitative information for critical constraints selected by the designer by analyzing
`the representations of reachable sets in the space of variables characterizing the consumption of
`continuous resources. For example, in the case of linear constraints, it will be possible to evaluate
`the worst-case proximity to specified resource constraints using linear programming techniques.
`This research will make it possible for the designer to identify the most critical constraints in the
`system.
`The third innovation will help automate the verification process with respect to resource con-
`straints. We propose to develop an effective syntax for specifying resource constraints to be com-
`bined automatically with the models generated for exception handling and synchronization con-
`straints (Section 3.1.2). We will also extend our recently begun work in automatic generation of
`explanations to handle counterexamples that demonstrate resource violations. The development of
`these automatic translation and explanation capabilities, together with the development of novel
`model-checking algorithms to handle continuous resources, will provide engineers with important
`and valuable new tools for verifying resource-limited space systems.
`
`3.2 Verifying Environmental Interaction
`
`Reasoning about system interaction with the environment is difficult, due to the fact that the system
`is a discrete system but the environment is continuous, and due to the fact that our models of the
`environment are typically quite uncertain. We propose fundamental work to address both these
`difficulties.
`
`3.2.1 Handling Both Continuous and Discrete State Variables
`
`The laws of continuous dynamics, usually modeled by differential and algebraic equations, govern
`the operations of autonomous systems and their interactions with the physical world.
`In con-
`trast, current model checking tools are based on discrete-state models of computation. Timing is
`typically the only mechanism for incorporating features of physical environments into these mod-
`els. Our goal is to create tools for analyzing models of physical dynamic systems, by abstracting
`tractable behavioral models and verifying task plans with respect to environmental constraints.
`Autonomous systems interacting with physical environments can be modeled as hybrid dy-
`namic systems, that is, systems with both continuous and discrete state variables. Hybrid dynamics
`can also appear in the environment itself when the continuous dynamics depend on discrete con-
`ditions, such as the influence of contact surfaces on mechanism dynamics. Central issues in recent
`research on hybrid dynamic systems include numerical methods for determining the accuracy of
`an approximation, identifying and characterizing qualitative behaviors such as invariants and limit
`cycles, synthesizing controllers for various objectives such as stability and reachability, and formal
`verification [4, 30, 36].
`This latter research on formal verification is most germane to the present proposal. In contrast
`
`10
`
`Page 10 of 17
`
`

`
`to model checking for finite-state systems, algorithmic verification is possible for hybrid dynamic
`systems with only very simple classes of continuous dynamics [22, 21, 29]. Consequently, the
`best one can hope for is to use conservative models that represent outer or inner approximations
`to the families of exact system behaviors. Based on our experience and that of o