160 REAL-TIME LOGIC, GRAPH-THEORETIC ANALYSIS, AND MODECHART

is, literals ¬F and ¬G. To build the second level, the algorithm adds the literals in the second clause of S2, that is, literals ¬B, ¬D, and ¬F, to each subtree rooted by literals ¬F and ¬G. Similarly, the algorithm constructs the remaining levels in the tree. Figure 6.2 shows the worst-case search tree for the set S2. A worst-case tree is one in which all conjunctions of literals are explored. However, in practice, a large number of nodes need not be constructed (1) by checking for unsatisfiability as soon as the algorithm creates a new node or (2) by rearranging the order of the clauses in S2 according to certain heuristics to reduce the size of the tree.

To prove that the conjunction of clauses in S1 and S2 is unsatisfiable, we need to show that each leaf node in the tree satisfies one of the following two conditions:

(1)the conjunction of literals in the leaf node and at least one clause in S1 is false, or

(2)the conjunction of literals in the leaf node is by itself unsatisfiable.

The first condition follows from basic logic: Ck ¬Ck where Ck is a clause in set S1 and ¬Ck is the conjunction of literals in a leaf node; that is,

(Lk,1 Lk,2 · · · Lk,mk ) (¬Lk,1 ¬Lk,2 · · · ¬Lk,mk )

is always false, making the collection of clauses in S1 and S2 unsatisfiable. The leftmost leaf node of our example tree is the conjunction ¬F ¬B ¬A, which can be “and-ed” with either of the first two clauses of S1, that is, A or B, making the conjunction false. Since the conjunction of literals in every leaf node of the tree makes at least one clause in S1 is unsatisfiable, we can conclude that the collection of clauses in S1 and S2 is unsatisfiable. The second condition follows from a similar reasoning.

6.6.1 Analysis Complexity and Optimization

In the worst case, where the full search tree is constructed using all positive cycles detected, the running time of the unsatisfiability check algorithm is exponential with respect to the number of positive cycles found. For example, if there are n positive cycles and each cycle has m edges, there are m literals in each clause with only negated literals in S2. Therefore, there are mn leaf nodes (conjunctions) in the worstcase search tree and thus the running time is proportional to mn .

Several ways are available to reduce the size of the search tree and hence speed up the analysis. The first optimization approach stops expanding a node if its labeled conjunction of negated literals makes S1 unsatisfiable. If a newly created node in the tree has a conjunction of negated literals that makes a clause in S1 unsatisfiable, then every node in the subtree rooted by that node has the same property and thus needs not be generated. In our example search tree, the nodes in the subtree rooted by the node labeled (¬F, ¬B) need not be created since this conjunction together with the second clause, B, of S1 is false, and hence this node makes S1 unsatisfiable. Similarly, the nodes in the subtree rooted by the node labeled (¬F, ¬D) need not be created since this conjunction together with the fourth clause, D, of S1 is false, and hence this node makes S1 unsatisfiable.

B

D

F A

F C

F

F G

F E

F

F G

Figure 6.3 Rearranging positive cycles to trim the search tree.

The second optimization approach rearranges the order of the clauses in S2 (corresponding to the positive cycles found) so that the first approach can be applied as soon as possible, that is, closer to the root of the search tree. This may require backtracking by undoing the generation of a tree node. In our example search tree, the node labeled (¬F, ¬B) makes S1 unsatisfiable because ¬B “and-ed” with the second clause, B, is false. Note that the first negated literal ¬F does not contribute to the unsatisfiability of S1. We can reject the first positive cycle by rearranging the first and second clauses, corresponding to the first and second positive cycles found, so that the second clause appears first. This makes it possible to declare unsatisfiability of S1 for two nodes ¬B and ¬D at the first level of the tree. This approach may trim the tree under many conditions, as shown in Figure 6.3.

The third optimization approach, which is not pointed out in [Jahanian and Mok, 1987], reuses the unsatisfiability of previously generated nodes to declare that a newly generated node v makes S1 unsatisfiable if the labels of v have been generated earlier. In our example, note that the labels of the last node (¬F, ¬G) are the same as those of a previous leaf node.

6.7 INDUSTRIAL EXAMPLE: NASA X-38 CREW RETURN VEHICLE

Now we use RTL to specify and analyze the timing properties of the avionics of the X-38, a family of vehicles built as incremental development prototypes for the Crew Return Vehicle (CRV) of the International Space Station (ISS). The CRV, planned for a 2003 launch on board the Space Shuttle, will be attached to the ISS and will have the capability to automatically and safely bring to earth a crew of seven passengers in the event of an emergency ISS evacuation. The CRV will be designed to autonomously perform all guidance, navigation, and control functions, the deorbit burn, a parafoil-assisted glide through the atmosphere, and will be designed to land horizontally at one of several predetermined landing sites.

162 REAL-TIME LOGIC, GRAPH-THEORETIC ANALYSIS, AND MODECHART

The X-38 131 model vehicle was successfully drop-tested from a B-52 in March 1998 to demonstrate body design and parafoil landing. The X-38 132 model will incrementally employ increased automatic guidance capability and will undergo several atmospheric drop tests. The immediate precursor to the CRV, the X-38 281 model vehicle, is being designed and is planned for a 2001–2002 on-orbit deployment from the Space Shuttle. It will perform the CRV functions of automatic guidance, re-entry, glide, and landing, but be unmanned. Here we focus on the X-38 201 vehicle avionics design. A more detailed description and analysis of the X-38 avionics is found in [Rice and Cheng, 1999].

6.7.1 X-38 Avionics Architecture

Here, we focus on the timing within the quad-redundant embedded avionic control units, called Flight Critical Computers (FCC) 1 through 4, of the preliminary X-38 201 vehicle data system architecture. These units receive all sensor input values, provide all embedded guidance and application processing, and control actuation. Each FCC is a unit comprised of two PowerPC processors, Input/Output cards, and several other devices in a Versa Module Europa (VME) bus chassis. The first processor, called the Flight Critical Processor (FCP), houses all application software, such as guidance, navigation, and control. The second processor, the Instrumentation Control Processor (ICP), is responsible for assembling inputs from all other sensors and sending the data over the VME backplane to the FCP for processing. Both processors run the VxWorks real-time operating system as well as specially developed system services.

6.7.2 Timing Properties

For safety and verifiability reasons, all X-38 avionics design efforts have focused on designing a system that is highly deterministic. The quad-redundant design of the four FCCs relies on Byzantine agreement (a voting and message-passing protocol) to tolerate a single Byzantine fault [Pease, Shostak, and Lamport, 1980; Lamport, Shostak, and Pease, 1982]. Because of this design, tasks are required to run at the same time in all processors, with results of their processing being voted every 20-ms “minor” frame. The ICP and FCP processors are thus synchronized to the same 20-ms processing frame. Another example of similar real-time fault-tolerant avionics is the quad-redundant fly-by-wire flight control of the Lockheed F-117A stealth fighter aircraft. Other examples of fault-tolerant avionics include the Boeing 777 Integrated Airplane Information Management System [Yeh, 1998] and the Airbus 340 Flight Warning System.

We consider a snapshot of the anticipated task timing relationships for the X-38 vehicle. The most critical control loop begins 18 ms into the processing frame where the ICP inputs all 50 Hz (cycles per second) sensor data. These data are passed to the FCP, which reads the sensor data, processes them, and provides output actuator commands back to the ICP. The ICP then reads and issues those commands to affected actuators. To effect safe guidance of the vehicle, this whole processing loop must be completed within 10 ms. To ensure this type of deterministic processing, tasks are

generally assigned fixed priorities based upon the Rate-Monotonic Scheduling algorithm presented in chapter 3, and scheduling is partially accomplished with the aid of a cyclic executive.

6.7.3 Timing and Safety Analysis Using RTL

To analyze and verify system timing properties, we use RTL, described in this chapter, to specify the safety-critical aspects of the X-38 system. As we have seen, RTL allows timing and safety analysis which may flexibly be used for what-if scenarios as well as life-cycle system verification, and may be extensible to represent broader aspects of the X-38 avionic system. The two X-38 flight-critical control loops, as well as one non-flight critical control loop and the associated safety assertion, are modeled. After converting the RTL representation into a Presburger arithmetic format and ultimately a constraint graph, cycle analysis verifies safety assertion satisfaction.

6.7.4 RTL Specification

This section presents the RTL specification for a representative set of X-38 tasks. The tasks listed under “workload and event definitions” contain the workloads in milliseconds (ms) for each task modeled. Nomenclature of the task names are that the first three characters define the processor; the next character designates either I(input), P(process), or O(output); the number identifies the speed of the process in Hertz or cycles per second, next is the criticality such as FC(flight-critical) or NFC(non-flight-critical); and last is any other necessary information such as data type. The variable i represents the loop count or iteration number. For example, the set of tasks in the flight critical 50-Hz control loop are the first five listed and are shown below.

; 50HzFCworkloads

i@(↑ ICP I50FC SENSOR, i) + 2 ≥ @(↓ ICP I50FCSENSOR, i)

i@(↑ FCP I50FC, i) + 1 ≥ @(↓ FCP I50FC, i)

i@(↑ FCP P50FC, i) + 5 ≥ @(↓ FCP P50FC, i)

i@(↑ FCP O50FC, i) + 1 ≥ @(↓ FCP O50FC, i)

i@(↑ ICP I50FC CMDS, i) + 1 ≥ @(↓ ICP I50FC CMDS, i)

The workload for the first task, designated “Instrumentation Control Processor (ICP) Input (I) of 50 Hz Flight Critical (FC) Sensor Data,” is a maximum of 2 ms. The above group of tasks are representative of the ICP reading all 50-Hz flightcritical sensors, such as flap, rudder positions, and Global Positioning System data; passing that data to the FCP as input; having the guidance application process that data and formulate command output; passing that output to the ICP; and having the ICP actuate the command. This list is the first of two flight-critical timing loops, requiring completion within 10 ms for safe vehicle control. The 10-Hz flight-critical

164 REAL-TIME LOGIC, GRAPH-THEORETIC ANALYSIS, AND MODECHART

control loop is similar, but a loop completion time of 50 ms, rather than 10 ms, is required. This completion requirement is represented in the safety assertion section. The non-flight-critical tasks only receive sensor input, produce no command output, and are included as a representation of the many non-flight-critical tasks that run in the background but whose execution is not considered safety-critical. The precedence-relations section depicts the order in which the tasks must execute. For example, to properly specify system behavior, it must be stated that the end of any task must not occur before its beginning.

i@(↑ ICP I50FC SENSOR, i) ≤ @(↓ ICP I50FC SENSOR, i)

Furthermore, the beginning of the next task to execute must not occur before the end of its predecessor. In this case, the FCP’s input of flight critical data must happen after the ICP’s 50 Hz sensor scan.

; 50 Hz FC precedence relations

i@(↓ ICP I50FC SENSOR, i) ≤ @(↑ FCP I50FC, i)

A precedence relationship between the end of the successor task and the initiation of the predecessor task must also be represented. In this case, the FCP’s input of flight-critical data should happen at or before the completion of the ICP’s sensor scan predecessor task workload. In reality, we want the FCP I50FC task to happen precisely after the completion of the ICP I50FC SENSOR task, but this truth is captured by the clauses cited above in addition to the workload definition.

i@(↑ FCP I50FC, i) − 2 ≤ @(↑ ICP I50FC SENSOR, i)

The priority assertions loosely mimic a rate-monotonic scheduling paradigm in which the higher rate tasks have priority over lower rate tasks. For example, the following formula states that the flight-critical 50-Hz task has precedence over the flight-critical 10-Hz task.

i@(↓ FCP I50FC, i) ≤ @(↑ FCP I10FC, i)

; 50 Hz FC higher priority than 10 Hz FC

i@(↓ FCP I50FC, i) ≤ @(↑ FCP I50NFC, i)

; 50 Hz FC higher priority than 50 Hz NFC

The periodicity section simply defines the rates at which the tasks execute, in ms, and in this case they are to run precisely every 20 or 100 ms, so they are found in pairs as follows.

i@(↑ ICP I50FC SENSOR, i) + 20 ≤ @(↑ ICP I50FC SENSOR, i + 1)

i@(↑ ICP I50FC SENSOR, i + 1) − 20 ≤ @(↑ ICP I50FC SENSOR, i)

Finally, the safety assertion, shown below, states that each of the flight-critical control loops, the 50-Hz and the 10-Hz, from initial sensor read through command actuation, must execute within 10 and 50 ms, respectively.

i@((↓ ICP I50FC CMDS, i) ≤ @(↑ ICP I50FC SENSOR, i) + 10

(↓ ICP I10FC CMDS, i) ≤ @(↑ ICP I10FC SENSOR, i) + 50)

The negation of the safety assertion is ultimately used to verify safety-critical system performance through constraint graph analysis.

RTL System Specification Representation:

Workload and event definitions: ; 50 Hz FC workloads

i@(↑ ICP I50FC SENSOR, i) + 2 ≥ @(↓ ICP I50FCSENSOR, i)

i@(↑ FCP I50FC, i) + 1 ≥ @(↓ FCP I50FC, i)

i@(↑ FCP P50FC, i) + 5 ≥ @(↓ FCP P50FC, i)

i@(↑ FCP O50FC, i) + 1 ≥ @(↓ FCP O50FC, i)

i@(↑ ICP I50FC CMDS, i) + 1 ≥ @(↓ ICP I50FC CMDS, i)

; 10 Hz FC workloads

i@(↑ ICP I10FC SENSOR, i) + 2 ≥ @(↓ ICP I10FCSENSOR, i)

i@(↑ FCP I10FC, i) + 1 ≥ @(↓ FCP I10FC, i)

i@(↑ FCP P10FC, i) + 40 ≥ @(↓ FCP P10FC, i)

i@(↑ FCP O10FC, i) + 1 ≥ @(↓ FCP O10FC, i)

i@(↑ ICP I10FC CMDS, i) + 1 ≥ @(↓ ICP I10FC CMDS, i)

; 50 Hz NFC workloads

i@(↑ ICP I50NFC SENSOR, i) + 5 ≥ @(↓ ICP I50NFCSENSOR, i)

i@(↑ FCP I50NFC, i) + 1 ≥ @(↓ FCP I50NFC, i)

Precedence relations:

; precedence between start and stop events

i@(↑ ICP I50FC SENSOR, i) ≤ @(↓ CP I50FCSENSOR, i)

i@(↑ FCP I50FC, i) ≤ @(↓ FCP I50FC, i)

i@(↑ FCP P50FC, i) ≤ @(↓ FCP P50FC, i)

i@(↑ FCP O50FC, i) ≤ @(↓ FCP O50FC, i)

i@(↑ ICP I50FC CMDS, i) ≤ @(↓ ICP I50FC CMDS, i)

i@(↑ ICP I10FC SENSOR, i) ≤ @(↓ ICP I10FCSENSOR, i)

166 REAL-TIME LOGIC, GRAPH-THEORETIC ANALYSIS, AND MODECHART

i@(↑ FCP I10FC, i) ≤ @(↓ FCP I10FC, i)

i@(↑ FCP P10FC, i) ≤ @(↓ FCP P10FC, i)

i@(↑ FCP O10FC, i) ≤ @(↓ FCP O10FC, i)

i@(↑ ICP I10FC CMDS, i) ≤ @(↓ ICP I10FC CMDS, i)

i@(↑ ICP I50NFC SENSOR, i) ≤ @(ICP I50NFCSENSOR, i)

i@(↑ FCP I50NFC, i) ≤ @(FCP I50NFC, i)

i@(↑ FCP P50NFC, i) ≤ @(FCP P50NFC, i)

;precedence between end of first task and beginning of next

;50 Hz FC precedence relations

i@(ICP I50FC SENSOR, i) ≤ @(↑ FCP I50FC, i) f oralli@(FCP I50FC, i) ≤ @(↑ FCP P50FC, i)

i@(FCP P50FC, i) ≤ @(↑ FCP O50FC, i)

i@(FCP O50FC, i) ≤ @(↑ ICP I50FC CMDS, i)

; 10 Hz FC precedence relations

i@(↓ ICP I10FC SENSOR, i) ≤ @(↑ FCP I10FC, i)

i@(↓ FCP I10FC, i) ≤ @(↑ FCP P10FC, i)

i@(↓ FCP P10FC, i) ≤ @(↑ FCP O10FC, i)

i@(↓ FCP O10FC, i) ≤ @(↑ ICP I10FC CMDS, i)

; 50 Hz NFC precedence relations

i@(↓ ICP I50NFC SENSOR, i) ≤ @(↑ FCP I50NFC, i)

i@(↓ FCP I50NFC, i) ≤ @(↑ FCP P50NFC, i)

;precedence between beginning of prior task and beginning of next

i@(↑ FCP I50FC, i) − 2 ≤ @(↑ ICP I50FC SENSOR, i)

i@(↑ FCP P50FC, i) − 1 ≤ @(↑ FCP I50FC, i)

i@(↑ FCP O50FC, i) − 5 ≤ @(↑ FCP P50FC, i)

i@(↑ ICP I50FC CMDS, i) − 1 ≤ @(↑ FCP O50FC, i)

i@(↑ FCP I10FC, i) − 2 ≤ @(↑ ICP I10FC SENSOR, i)

i@(↑ FCP P10FC, i) − 1 ≤ @(↑ FCP I10FC, i)

i@(↑ FCP O10FC, i) − 40 ≤ @(↑ FCP P10FC, i)

i@(↑ ICP I10FC CMDS, i) − 1 ≤ @(↑ FCP O10FC, i)

i@(↑ FCP I50NFC, i) − 5 ≤ @(↑ ICP I50NFC SENSOR, i)

i@(↑ FCP P50NFC, i) − 1 ≤ @(↑ FCP I50NFC, i)

INDUSTRIAL EXAMPLE: NASA X-38 CREW RETURN VEHICLE 167

Priority assertions:

; 50 Hz FC higher priority than 10 Hz FC

i@(FCP I50FC, i) ≤ @(↑ FCP I10FC, i)

; 50 Hz FC higher priority than 50 Hz NFC

i@(FCP I50FC, i) ≤ @(↑ FCP I50NFC, i)

Periodicity:

; 50 Hz FC tasks, p = 20

i@(↑ ICP I50FC SENSOR, i) + 20 ≤ @(↑ ICP I50FC SENSOR, i + 1)

i@(↑ FCP I50FC, i) + 20 ≤ @(↑ FCP I50FC, i + 1)

i@(↑ FCP P50FC, i) + 20 ≤ @(↑ FCP P50FC, i + 1)

i@(↑ FCP O50FC, i) + 20 ≤ @(↑ FCP O50FC, i + 1)

i@(↑ ICP I50FC CMDS, i) + 20 ≤ @(↑ ICP I50FC CMDS, i + 1)

i@(↑ ICP I50FC SENSOR, i + 1) − 20 ≤ @(↑ ICP I50FC SENSOR, i)

i@(↑ FCP I50FC, i + 1) − 20 ≤ @(↑ FCP I50FC, i)

i@(↑ FCP P50FC, i + 1) − 20 ≤ @(↑ FCP P50FC, i)

i@(↑ FCP O50FC, i + 1) − 20 ≤ @(↑ FCP O50FC, i)

i@(↑ ICP I50FC CMDS, i + 1) − 20 ≤ @(↑ ICP I50FC CMDS, i)

; 10 Hz FC tasks, p = 100

i@(↑ ICP I10FC SENSOR, i) + 100 ≤ @(↑ ICP I10FC SENSOR, i + 1)

i@(↑ FCP I10FC, i) + 100 ≤ @(↑ FCP I10FC, i + 1)

i@(↑ FCP P10FC, i) + 100 ≤ @(↑ FCP P10FC, i + 1)

i@(↑ FCP O10FC, i) + 100 ≤ @(↑ FCP O10FC, i + 1)

i@(↑ ICP I10FC CMDS, i) + 100 ≤ @(↑ ICP I10FC CMDS, i + 1)

i@(↑ ICP I10FC SENSOR, i + 1) − 100 ≤ @(↑ ICP I10FC SENSOR, i)

i@(↑ FCP I10FC, i + 1) − 100 ≤ @(↑ FCP I10FC, i)

i@(↑ FCP P10FC, i + 1) − 100 ≤ @(↑ FCP P10FC, i)

i@(↑ FCP O10FC, i + 1) − 100 ≤ @(↑ FCP O10FC, i)

i@(↑ I C P I 10FC C M DS, i + 1) − 100 ≤ @(↑ I C P I 10FC C M DS, i)

; 50 Hz NFC tasks

i@(↑ ICP I50NFC SENSOR, i) + 20 ≤ @(↑ ICP I50NFC SENSOR, i + 1)

i@(↑ FCP I50NFC, i) + 20 ≤ @(↑ FCP I50NFC, i + 1)

i@(↑ FCP P50NFC, i) + 20 ≤ @(↑ FCP P50NFC, i + 1)