Safety Verification of Fault Tolerant Goal-Based Control Programs with Estimation Uncertainty - Braman2008p87382009_American_Control_Conference_Vols

Safety Verification of Fault Tolerant Goal-based Control Programs with

Estimation Uncertainty

Julia M. B. Braman and Richard M. Murray

Abstract

— Fault tolerance and safety verification of control

systems that have state variable estimation uncertainty are

essential for the success of autonomous robotic systems. A

software control architecture called Mission Data System,

developed at the Jet Propulsion Laboratory, uses goal networks

as the control program for autonomous systems. Certain types

of goal networks can be converted into linear hybrid systems

and verified for safety using existing symbolic model checking

software. A process for calculating the probability of failure of

certain classes of verifiable goal networks due to state estimation

uncertainty is presented. A verifiable example task is presented

and the failure probability of the control program based on

estimation uncertainty is found.

I. I

NTRODUCTION

Autonomous robotic missions by nature have complex

control systems. The necessary fault detection, isolation and

recovery software for these systems is often cumbersome

and added on as failure cases are encountered in simulation.

One way to systematically incorporate fault tolerance in

autonomous robotic control systems is to create a flexible

control system that can reconfigure itself in the presence

of faults. However, if the control system cannot be verified

for safety, even in the presence of state variable estimation

uncertainty, the added complexity of the reconfigurability of

a system could reduce the system’s effective fault tolerance.

A great deal of work to date has focused on detecting and

recovering from sensor failures in the control of autonomous

systems [1]. One particularly useful way to model a fault

tolerant control system is as a hybrid system. The control

of hybrid systems has been well studied [2]. When the

continuous dynamics of these systems are sufficiently simple,

it is possible to verify that the execution of the hybrid

control system will not fall into an unsafe regime [3]. There

are several software packages available that can be used

for this analysis, including HyTech [4], UPPAAL [5], and

PHAVer [6], all of which are symbolic model checkers.

PHAVer, the symbolic model checker used in this paper, is

able to exactly verify linear hybrid systems with piecewise

constant bounds on continuous state derivatives and is able

to handle arbitrarily large numbers due to the use of the

Parma Polyhedra Library. Safety verification for fault tolerant

hybrid control systems ensures that the occurrence of certain

faults will not cause the system to reach an unsafe state.

However, these verification software packages cannot

verify linear hybrid systems that have uncertainty in the

estimated state variables involved in transition condition

J. Braman and R. Murray are with the Dept. of Mech. Eng.,

California Institute of Technology, Pasadena, CA 91125, USA

braman@caltech.edu

logic. For autonomous systems, none of the state variables

used in the control system are known perfectly, and these

uncertainties can affect the safety of the system. Stochastic

hybrid systems include uncertainty in the transitions of

the hybrid automaton as probabilistic transition conditions.

Much work has been done on the verification of stochastic

hybrid systems. Prajna et al [7] use barrier certificates to

bound the upper limit of the probability of failure of the

stochastic hybrid system; Kwiatkowska et al [8] discuss

a probabilistic symbolic model checking software called

PRISM; and Amin et al [9] describe stochastic reachability

and maximal probabilistic safe set computations for discrete

time stochastic hybrid systems. However, purely probabilistic

transition conditions do not model estimation uncertainty

well; deterministic transitions with probabilistic components

may be a better model.

In this paper, Mission Data System (MDS), developed

at the Jet Propulsion Laboratory, is the goal-based control

architecture. The structure of this paper is as follows. Section

II summarizes important concepts of MDS that pertain

to this work and describes the goal network conversion

and verification procedure. Section III describes the major

contribution of this work, the process for calculating the

probability of entering the unsafe set due to estimation

uncertainty for certain classes of verifiable goal networks.

Section IV describes an example verification and failure

probability calculation. Finally, Section V concludes the

paper and discusses future directions of research.

II. B

ACKGROUND

NFORMATION

A. State Analysis and Mission Data System

State Analysis is a systems engineering methodology that

focuses on a state-based approach to the design of a system

[10]. Models of state effects in the system to be controlled

are used for such things as the estimation of state variables,

control of the system, planning, and goal scheduling. State

variables are representations of states or properties of the

system that are controlled or that affect a controlled state.

Examples of state variables could include the position of a

robot, the temperature of the environment, the health of a

sensor, or the position of a switch.

Goals and goal elaborations are created based on the

models. Goals are specific statements of intent used to

control a system by constraining a state variable in time.

Goals are elaborated from a parent goal based on the intent

and type of goal, the state models, and several intuitive rules,

described in [10]. A core concept of State Analysis is that the

language used to design the control system should be nearly

2008 American Control Conference

Westin Seattle Hotel, Seattle, Washington, USA

June 11-13, 2008

WeAI01.6

Authorized licensed use limited to: CALIFORNIA INSTITUTE OF TECHNOLOGY. Downloaded on April 14,2010 at 21:23:26 UTC from IEEE Xplore. Restrictions apply.

the same as the language used to implement the control

system. Therefore, the software architecture, MDS, is closely

related to State Analysis.

Goal networks replace command sequences as the control

input to the system. A goal network consists of a set of

goals with their associated starting and ending time points

and temporal constraints. A goal may cause other constraints

to be elaborated on the same state variable and/or on other

causally related state variables. The goals in the goal network

and their elaborations are scheduled by the scheduler soft-

ware component so that there are no conflicts in time, goal

order or intent. Each scheduled goal is then achieved by the

estimator or controller of the state variable constrained.

Elaboration allows MDS to handle tasks more flexibly

than control architectures based on command sequences. One

example is fault tolerance. Re-elaboration of failed goals is

an option if there are physical redundancies in the system,

many ways to accomplish the same task, or degraded modes

of operation that are acceptable for a task. The elaboration

class for a goal can include several pre-defined tactics. These

tactics are simply different ways to accomplish the intent

of the goal, and tactics may be logically chosen by the

elaborator based on programmer-defined conditions. This

capability allows for many common types and combinations

of faults to be accommodated automatically by the control

system [11].

B. Goal Network Conversion and Verification Procedure

Hybrid system analysis tools can be used to verify the

safe behavior of a hybrid system; therefore, a procedure to

convert goal networks into hybrid systems is an important

tool for goal network verification. A process for converting

certain types of goal networks is described in [12]. These

goal networks can have several state variables and several

layers of goal elaborations, however time points must be

well-ordered, which means that the time points fire in the

order they are listed in the elaboration.

Each state variable in the goal network is labeled as either

controllable, uncontrollable, or dependent. A controllable

state variable (CSV) is directly associated with a command

class. An uncontrollable state variable (USV) is not as-

sociated with a command class in any way. A dependent

state variable (DSV) has model dependencies on at least

one controllable state variable. Different hybrid automata are

created from goals on and states of these different types of

state variables.

An outline of the conversion procedure for the goals on

CSVs and DSVs is as follows:

1) Create elaboration and transition logic tables for each

goal that elaborates any constraints on CSVs and

for each CSV and continuous DSV, respectively. List

transition conditions between states for each discrete

DSV.

2) Place goals between consecutive time points into

groups.

3) In each group, create locations (modes) by combining

branch goals (goals on CSVs that are not ancestors

of other goals on CSVs in the group) with all parent

and sibling goals (goals in the same tactic or other

root goals) that constrain CSVs. Label each location

with the dynamical update equations for all CSVs and

continuous DSVs constrained in the location. Create

Success and Safing locations.

4) Create transitions between locations and groups using

the elaboration and transition logic tables found above.

Elaboration logic controls transitions into groups and

failure transitions between locations in a group, and

transition logic controls the transitions out of a group

to the next group or to the Success location.

5) Add exit and failure transitions based on time to

locations in groups that have time constraints. Add

entry actions that reset the time variable to zero when

transitions from the group connector into locations in

these groups are taken.

6) Remove unnecessary locations, groups, and transitions.

For each each USV, a separate hybrid automaton is created

by making locations from the discrete states or discrete

sets of states of the variable. The transition conditions

are stochastic rates or are based on the state models. For

safety verification, the hybrid automata are converted into

PHAVer code and the appropriate transitions are synchro-

nized between the automata. The unsafe (or incorrect) set

is determined and conditions that would cause the hybrid

automata to enter the unsafe set are searched for using the

verification software. If no such conditions are found, the

goal network is said to be verified.

III. F

AILURE

ROBABILITY

ERIVATION

An important assumption for the verification of the control

programs described in the previous section is that the values

of the state variables are known exactly. This is unrealistic

in autonomous systems, where the estimation of the states

of the system are bound to have some uncertainty. In this

section, a method for calculating the probability of failure

of a verifiable goal network is described for a subset of the

goal networks allowed in the previous section.

In addition to a goal network being verifiable without

estimation uncertainty, some restrictions must be placed on

the state variables that can be uncertain. Any uncontrollable

state variable may have bounded estimation uncertainty.

All uncontrollable state variables take values that fall into

discrete sets. In this work, each combination of discrete

values that the uncertain state variables can take must be

unambiguously associated with only one location in each

group of the hybrid automaton. Stated another way, the

location in a group that the automaton transitions into after

the initial transition into the group must only depend on the

values that the uncertain state variables take. Finally, it is

assumed that the probability of transitions of the uncertain

state variable from one value to another (or the same) value

only depends on the previous value of that state variable,

and therefore can be modeled as a stationary Markov process.

The probability that the estimated value of an uncertain state

Authorized licensed use limited to: CALIFORNIA INSTITUTE OF TECHNOLOGY. Downloaded on April 14,2010 at 21:23:26 UTC from IEEE Xplore. Restrictions apply.

variable is derived from the estimation uncertainty, and only

depends on the actual value of the state variable.

Several pieces of information that characterize the un-

certain state variables are assumed to be known. First, the

number of state variables that are uncertain is

and the

number of discrete states or sets of states that each uncertain

state variable can take is

, where

= 1

, ..., n

. Let

represent the

th possible value of the

th uncertain state

variable, where

= 1

, ..., m

∀

= 1

, ..., n

. Let

represent

the estimated value of the

th uncertain state variable and

let

represent the actual value of each uncertain state

variable. The Markov transition probabilities for the actual

values of the uncertain state variables are also given, and the

stationary probabilities represent the probability that each

state variable’s actual value is each of its possible values.

Finally, the estimation uncertainty of each state variable is

the probability distribution of the estimated value of the state

variable being

i,e

given that the actual value of the state

variable is

i,a

A. Problem Set-up

Let

be the set of all possible combinations of ac-

tual and estimated values that each uncertain state vari-

able can take; in Fig. 1,

is the overall closed set.

has

∏

elements, and each element takes the form

...v

. For each group

, where

, ..., N

and

is the number of groups in the automaton,

there are sets

Ω

⊂

, where the elements of

Ω

cause the

automaton to enter the unsafe set from

and are called “un-

safe” elements. Since the goal network is verifiable, entrance

into this set is always due to estimation uncertainty, and

the probability of entering this set is the failure probability.

Entrance into the unsafe set for each group is dictated by

the actual values of the uncertain state variables, while the

transition conditions within the group are dependent on the

estimated value of the uncertain state variable. There also are

sets

⊂

in which each element causes the automaton to

leave

and enter the Safing location without also entering

the unsafe set. A set

may be empty. Finally, there are

sets

≡

−

(Ω

)

(1)

to which the remainder of elements in

belong. Elements

, called “non-failing” elements, allow operation to

continue in the group or allow a successful transition out

of the group to the next one. These sets are represented

graphically in Fig. 1.

Some groups may be broken into two or more subgroups.

A subgroup of locations is a proper subset of locations in

the group that, once entered from the previous group (or

initially), is not exited until a transition out of the group is

taken (to Safing or to the next group). Subgroups are treated

like groups; adjustments to the numbering of the groups are

needed to account for them.

For each location

, h

= 1

, ..., λ

, where

is the number

of locations in each group (or subgroup), there is a set

that contains all of the initial conditions that will cause

Fig. 1. A representation of sets of uncertain state variable elements. Set

is the sum of the set of unsafe elements,

Ω

, the set of “Safing” elements,

, and the set of non-failing elements,

. The set of initial conditions,

⊆

, is the union of the sets of initial conditions for each of the

locations in the group,

, h

= 1

in this case. Set

∩

Ω

is the

set of unsafe initial conditions. A representative path starting at

(0) =

that the automaton takes through the sets in this group, with completion

time

= 5

, is shown.

the automaton to enter that location when entering

. The

intersection of

for any two locations in

is the empty

set and the set of initial conditions of

is the union of all

the sets of initial conditions for each of its locations,

k

⋃

(2)

is a subgroup,

will be a proper subset of set

; however if

is a group,

will equal

. A

representation of set

⊂

with

= 3

is shown in

Fig. 1.

For each group, the initial conditions that would cause

immediate failure of the group due to estimation uncertainty

can be found in set

∩

Ω

, which is shown

graphically in Fig. 1. The probability of failing due to the

initial condition can be found by summing the probability of

each element of

occurring,

∑

k

(

(0) =

)

where

be the number of elements in set

and

is the

th element in

k

∑

∏

(

i,ab

)

(

i,eb

i,ab

)

(3)

For the elements in

for each group, the vector

contains the probability of starting in each non-failing initial

condition. Let

be the number of elements in

and

(

)

be the

th element of

, where

= 1

, ..., p

and

(

) =

(

(0) =

)

(

) =

∏

(

i,ap

)

(

i,ep

i,ap

)

(4)

For each group, there is a

matrix,

, whose

elements are the probability of making a transition from

element

∈

to element

′

∈

, where

q, q

′

= 1

, ..., q

and

(

q, q

′

) =

(

+ 1) =

′

(

) =

)

and

is the

Authorized licensed use limited to: CALIFORNIA INSTITUTE OF TECHNOLOGY. Downloaded on April 14,2010 at 21:23:26 UTC from IEEE Xplore. Restrictions apply.

number of elements in set

(

q, q

′

) =

∏

(

i,aq

′

ai,p

i,aq

)

(

i,eq

′

i,aq

′

))

(5)

where

ai,p

is the previous actual value of the

th uncertain

state variable.

For each group, there exists a

vector,

u,k

, whose

elements are the sum of probabilities of the transitions from

the

th element in

to each element

Ω

, which is

the transition from each non-failure state to any failure state,

u,k

(

) =

∑

k

(

+ 1) =

(

) =

)

. Let

be the number of unsafe elements in

Ω

and

= 1

, ..., q

then

u,k

(

) =

k

∑

∏

(

i,au

ai,p

i,aq

)

(

i,eu

i,au

))

(6)

If set

⊂

, then there are two more definitions to

make,

uI,k

and

I,k

, which have probabilities of transi-

tions from elements in

to every element in

Ω

and

each element in

, respectively. Let

= 1

, ..., p

represent

the

th initial condition in

uI,k

(

) =

k

∑

∏

(

i,au

ai,p

i,ap

)

(

i,eu

i,au

))

(7)

and

I,k

(

p, q

) =

∏

(

i,aq

ai,p

i,ap

)

(

i,eq

i,aq

))

(8)

Each group

has a minimum execution time that could

be due to the completion of the goal constraints or to a

specific time constraint applied to the group. This minimum

execution time is called the completion time and is labeled

. There are only three possible ways of leaving a group:

1) The completion time is reached, and the execution

moves normally into the next group.

2) A transition to the “Safing” set,

(

)

∈

, is taken

before the completion time is reached.

3) A transition to the unsafe set,

(

)

∈

Ω

, is taken

before the completion time is reached.

Only the last condition is considered to be a failure case

that would contribute to the failure probability of that group.

There is a set of execution paths of a group,

, that end

with a transition into the unsafe set and each of these paths

has some probability of occurring. The failure probability of

the group,

(

)

, is the sum of the probabilities of all paths

∈

B. Uniform Completion Case

In the uniform completion case, the minimum execution

time of a group is also the maximum execution time; in other

words, all locations in the group contribute an equal amount

to the completion of the goals or to the time constraint placed

on the group. Therefore, a uniform completion time

would

require exactly

execution time steps before the group

would be exited normally. An example of this execution path

with

= 5

is shown in Fig. 1. Therefore, there are only

paths in

, each consisting of a failure after each step up

until the completion time.

For

= 1

, the only way to reach the unsafe set is to

start in it, the probability of which is represented by

. For

= 2

, the probability of starting in the non-failure initial

conditions and then making the transition to the unsafe set

is added to the probability of starting in the unsafe set, and

so on. The equations for the failure probability for different

cases of

, where

= 1

, ..., N

are

(

) =

, c

= 1

(9)

(

) =

uI,k

, c

= 2

(10)

and for

∈

∞

)

(

) =

[

uI,k

k

−

∑

I,k

u,k

]

(11)

I,k

and

uI,k

u,k

, the

∈

∞

)

equation

(

) =

[

k

−

∑

u,k

]

(12)

For the special case when

∞

, the equation for the

failure probability is

(

) =

[

uI,k

I,k

(

−

)

−

u,k

]

(13)

or, if

uI,k

u,k

and

I,k

(

) =

(

−

)

−

u,k

(14)

given that

(

−

)

−

∞

∑

(15)

C. Non-Uniform Completion Case

In the non-uniform completion case, the minimum execu-

tion time of a group is not the same as the maximum exe-

cution time. Sets of locations contribute a different amount

to the completion of goals or time constraints on the group.

An example of this is a group that cannot be transitioned out

of normally until the robot covers some distance, however,

different locations in this group constrain the maximum

speed of the robot to different values. The set of locations

with the maximum speed limit have a contribution to the

goal completion of

; that is, this set of locations dictates

the minimum execution time of the group. All other sets of

locations with lower speed limit constraints have contribution

values that are less than one. Paths in this group that exit

the group normally due to goal completion have location

Authorized licensed use limited to: CALIFORNIA INSTITUTE OF TECHNOLOGY. Downloaded on April 14,2010 at 21:23:26 UTC from IEEE Xplore. Restrictions apply.

Fig. 2. A representation of the sets of uncertain state variable elements

for the single uncertain state variable example.

contribution value sums that are equal to or exceed the

completion time.

While all normal completion paths in the uniform com-

pletion case had the same path length and the same contri-

bution value pattern (a sum of all ones), in the non-uniform

completion case, the normal completion paths have different

lengths and location contribution value patterns. Therefore,

the number of ways to reach group completion, and likewise

the unsafe set, is much greater in this case than in the uniform

completion case. The failure probability,

(

)

, for this

problem is calculated in the same way as in the uniform

completion case, by summing the path probabilities of each

path

∈

, however the determination of these paths is

a more difficult problem. This problem is solvable and is

addressed in [13].

IV. E

XAMPLES

A. Single Uncertain State Variable Example

Consider a verifiable goal network that has one uncer-

tain state variable that can take on two discrete values,

GOOD and POOR (G and P, respectively). The set

consists of four elements that all have the form

{

GG, GP, P G, P P

}

; one element is in the “Safing”

set

{

P P

}

, two are in the unsafe set

Ω

{

GP, P G

}

and one is in the non-failing completion set

{

}

. As

shown in Fig. 2, the set of initial conditions is

{

GG, GP, P G

}

The set of unsafe initial conditions is the intersection of the

set of initial conditions and the unsafe set,

∩

Ω

{

GP, P G

}

. Therefore, the calculation of the probability of

failure due to starting in the unsafe set is

(

(0) =

) +

(

(0) =

P G

)

(16)

The initial condition that is non-failing is

{

}

so the vector of the probabilities of starting in a non-failing

state is a scalar in this case, and is

(

(0) =

)

(17)

Likewise, since there is only one element in

, the vector

of transition probabilities from non-failing elements in

any of the unsafe elements in

Ω

is also a scalar in this case,

and is

(

+ 1) =

(

) =

(

+ 1) =

P G

(

) =

)

(18)

Fig. 3. Goal network for precision orientation device example; S1 = sensor

1, S2 = sensor 2, S1H = sensor 1 health, S2H = sensor 2 health. The dashed

line indicates that the goals below it are elaborated from the goal above the

line. The curved arrow indicates a time constraint.

The transition matrix between non-failing elements in

again a scalar in this case, and is

(

+ 1) =

(

) =

)

(19)

Since there is only one element in

, this is a uniform

completion case. Once given the value of

, an equation can

be chosen (either (9) or (12)) and used to find the probability

of reaching the unsafe set due to estimation uncertainty in

this group.

B. Precision Orientation Device Example

An example for the uniform completion case involves

two sensors that are used to estimate the orientation for

a precision orientation device. The first sensor is more

accurate, reliable, and has less estimation uncertainty than

the second sensor; therefore, when turning, the first sensor

is used if its health is estimated to be ‘GOOD.’ If the first

sensor’s health is estimated to be ‘FAIR’ or lower and the

second sensor’s health is estimated to be ‘GOOD,’ the second

sensor is used to estimate the orientation. If both sensors’

healths are estimated to be ‘FAIR,’ both are used to estimate

the orientation. Otherwise, the goal network safes, stopping

the turning mechanism.

It takes five time steps in any combination of the turning

goal’s tactics, shown in Fig. 3, to complete the turn. The

goal network then transitions into a maintenance goal on

the orientation that is also active for five time steps before

moving onto the next goal.

The breakdown of state variable types is one controllable

state variable, the orientation state variable; two uncontrol-

lable state variables, the sensor health state variables; and

no dependent state variables. The hybrid automaton created

from the goals on the orientation state variable is shown

in Fig. 4 and the automata created from Sensor 1 Health

and Sensor 2 Health state variables are shown in Fig. 5. The

unsafe set for this system is the union of several states, listed

as follows:

Authorized licensed use limited to: CALIFORNIA INSTITUTE OF TECHNOLOGY. Downloaded on April 14,2010 at 21:23:26 UTC from IEEE Xplore. Restrictions apply.

Fig. 4. Hybrid automaton for the CSV, orientation; S1HG = sensor 1

health is GOOD, S1HF = sensor 1 health is FAIR, S1HP = sensor 1 health

is POOR, and likewise for sensor 2.

Fig. 5. Hybrid automaton for Sensor 1 Health (Sensor 2 Health) state

variable.

1) Orientation in TurnS1 and

> α

2) Orientation in TurnS2 and

> γ

3) Orientation in TurnS12 and

> α

< α

> γ

< γ

4) Orientation in Maintain and

> α

and

> γ

The hybrid system was successfully verified for safety over

all values of

, and

The failure probabilities for each group were calculated

for several values of estimation uncertainty and one choice

of stationary Markov transition probabilities, and the results

can be found in Fig. 6.

V. C

ONCLUSIONS AND

UTURE

ORK

This paper derives the failure probability of certain veri-

fiable goal networks due to state variable estimation uncer-

tainty. An example goal network was verified and its failure

probability given the estimation uncertainty was calculated.

The calculation of the failure probability for the different

groups of a goal network can be used as a verification of the

Fig. 6. Calculated group failure probabilities vs. sensor health uncertainty

values

goal network in the presence of estimation uncertainty as

well as a design tool to drive the design of goal networks or

the choice of sensors and estimators to reduce the probability

of failure.

Future work includes extending the calculation of a failure

probability to include other types of uncertainty. Uncertainty

in group transitions, controllable state variables, completion

times, and the given probability distributions are all examples

of possible types of uncertainty to include. The verification

of goal networks in the presence of different forms of

uncertainty, including estimation uncertainty, is an important

problem, and this approach seems promising, at least for

certain types of goal networks.

VI. A

CKNOWLEDGEMENTS

The authors would like to gratefully acknowledge Michel

Ingham, David Wagner, Robert Rasmussen, and the MDS

team at JPL for feedback, suggestions, answered questions,

and MDS and State Analysis instruction. This work was

funded in part by an NSF graduate fellowship and an AFOSR

MURI grant, FA9550-06-1-0303.

EFERENCES

[1] Z.-H. Duan, Z.-X. Cai, and J.-X. Yu, “Fault diagnosis and fault tolerant

control for wheeled mobile robots under unknown environments: A

survey,”

IEEE Int’l Conference on Robotics and Automation

, pp. 3428–

3433, 2005.

[2] G. Labinaz, M. M. Bayoumi, and K. Rudie, “A survey of modeling

and control of hybrid systems,”

Annual Reviews of Control

, 1997.

[3] R. Alur, T. Henzinger, and P.-H. Ho, “Automatic symbolic verification

of embedded systems,”

IEEE Transactions on Software Engineering

vol. 22, no. 3, pp. 181–201, 1996.

[4] T. A. Henzinger, P.-H. Ho, and H. Wong-Toi, “HyTech: A model

checker for hybrid systems,”

International Journal on Software Tools

for Technology Transfer

, 1997.

[5] K. Larsen, P. Pettersson, and W. Yi, “UPPAAL in a nutshell,”

Inter-

national Journal on Software Tools for Technology Transfer

, vol. 1,

no. 1-2, pp. 134–152, 1997.

[6] G. Frehse, “PHAVer: Algorithmic verification of hybrid systems past

HyTech,”

International Conference on Hybrid Systems: Computation

and Control

, 2005.

[7] S. Prajna, A. Jadbabaie, and G. J. Pappas, “Stochastic safety verifi-

cation using barrier certificates,”

IEEE Conference on Decision and

Control

, 2004.

[8] M. Kwiatkowska, G. Norman, and D. Parker, “Probabilistic symbolic

model checking with PRISM: a hybrid approach,”

Int J Software Tools

Technology Transfer

, vol. 6, pp. 128–142, 2004.

[9] S. Amin, A. Abate, M. Prandini, J. Lygeros, and S. Sastry, “Reacha-

bility analysis for controlled discrete time stochastic systems,”

Inter-

national Conference on Hybrid Systems: Computation and Control

pp. 49–63, 2006.

[10] M. Ingham, R. Rasmussen, M. Bennett, and A. Moncada, “Engineering

complex embedded systems with State Analysis and the Mission Data

System,”

AIAA Journal of Aerospace Computing, Information and

Communication

, vol. 2, pp. 507–536, December 2005.

[11] R. D. Rasmussen, “Goal-based fault tolerance for space systems using

the Mission Data System,”

IEEE Aerospace Conference Proceedings

vol. 5, pp. 2401–2410, March 2001.

[12] J. M. Braman, R. M. Murray, and D. A. Wagner, “Safety verification of

a fault tolerant reconfigurable autonomous goal-based robotic control

system,”

IEEE/RSJ International Conference on Intelligent Robots and

Systems

, 2007.

[13] J. M. Braman and R. M. Murray, “Failure probability of verifiable

goal-based control programs due to state estimation uncertainty.”

Submitted, IEEE Conference on Decision and Control, 2008.

Authorized licensed use limited to: CALIFORNIA INSTITUTE OF TECHNOLOGY. Downloaded on April 14,2010 at 21:23:26 UTC from IEEE Xplore. Restrictions apply.