Robots are generally composed of electromechanical parts with multiple sensors and actuators. The overall behavior of a robot emerges from coordination among its various parts and interaction with its environment. Developing intelligent, reliable, robust and safe robots, or real-time embedded systems, has become a focus of interest in recent years. In this thesis, we establish a foundation for modeling, specifying and verifying discrete/continuous hybrid systems and take an integrated approach to the design and analysis of robotic systems and behaviors.

A robotic system in general is a hybrid dynamic system, consisting of continuous, discrete and event-driven components. We develop a semantic model for dynamic systems, that we call Constraint Nets (CN). CN introduces an abstraction and a unitary framework to model discrete/continuous hybrid systems. CN provides aggregation operators to model a complex system hierarchically. CN supports multiple levels of abstraction, based on abstract algebra and topology, to model and analyze a system at different levels of detail. CN, because of its rigorous foundation, can be used to define programming semantics of real-time languages for control systems.

While modeling focuses on the underlying structure of a system --- the organization and coordination of its components --- requirements specification imposes global constraints on a system's behavior, and behavior verification ensures the correctness of the behavior with respect to its requirements specification. We develop a timed linear temporal logic and timed forall-automata to specify timed as well as sequential behaviors. We develop a formal verification method for timed forall-automata specification, by combining a generalized model checking technique for automata with a generalized stability analysis method for dynamic systems.

A good design methodology can simplify the verification of a robotic system. We develop a systematic approach to control synthesis from requirements specification, by exploring a relation between constraint satisfaction and dynamic systems using constraint methods. With this approach, control synthesis and behavior verification are coupled through requirements specification.

To model, synthesize, simulate, and understand various robotic systems we have studied in this research, we develop a visual programming and simulation environment that we call ALERT: A Laboratory for Embedded Real-Time systems.

Introduction: Uniform Modeling Approach

The heaven attained Oneness and became clear. 
The earth attained Oneness and became settled. 
The spirit attained Oneness and became numinous. 
Valleys attained Oneness and became reproductive. 
All things attained Oneness and became alive.

--- Tao Teh Ching, Lao Tzu

Time attains Oneness and becomes linear. 
Domains attain Oneness and become universal. 
Components attain Oneness and become functional. 
Systems attain Oneness and become alive. 
Design and analysis attain Oneness and become productive.

--- Zhang Ying

Part I: Semantic Model and Behavior Analysis

The  Tao  that can be taught is not the everlasting  Tao . 
The Name that can be named is not the everlasting Name. 
That which has no name is the origin of heaven and earth. 
That which has a name is the Mother of all things.

--- Tao Teh Ching, Lao Tzu

A system that can be modeled is not the system itself. 
A model that can be made is not the absolute model. 
That which has no model is the origin of a system. 
That which has a model is the understanding of the system.

--- Zhang Ying

Part II: Requirements Specification and Behavior Verification

The way of human follows the way of earth. 
The way of earth follows the way of heaven. 
The way of heaven follows the way of  Tao . 
The way of  Tao  follows the way of Nature.

--- Tao Teh Ching, Lao Tzu

Implementations follow algorithms. 
Algorithms follow specifications. 
Specifications follow ideas. 
Ideas follow the way of Nature.

--- Zhang Ying

Part III: Control Synthesis and Robotic Architecture

Attain utmost emptiness. 
Maintain profound tranquility. 
All things are running concurrently, 
cycle follows cycle. 

Activity overcomes cold. 
Tranquility overcomes heat. 
Peace and quiet is the true path in the world.

--- Tao Teh Ching, Lao Tzu

Attain utmost stability. 
Maintain minimum energy. 
All things are running concurrently, 
cycle follows cycle. 

Constraints overcome chaos. 
Stability overcomes disturbance. 
Peace and quiet is the true path in the world.

--- Zhang Ying

Conclusion: It's Far to Finish

The greatest accomplishment seems unfinished, 
yet its applications are endless. 
The greatest fullness seems empty, 
yet its applications are never exhausted.

--- Tao Teh Ching, Lao Tzu

The greatest conclusion seems stuttering, 
yet its implications are endless. 
The greatest future work seems crude, 
yet its fruits are never exhausted.

--- Zhang Ying