Sayan Mitra - Verifying Cyber-Physical Systems: A Path to Safe Autonomy (Cyber Physical Systems Series)

List of Figures

An autonomous vehicle system. Top. Polaris GEM-based electric vehicle platform created by AutonomousStuff. Bottom. Modules in the computational pipeline of an HAV and their typical models. Perception modules work on sensor data and construct representations for location, obstacles, and other elements. Decision, planning, and control modules are based on geometric and dynamical representation of the physical space and agents around the vehicle.

Verification in the design automation ecosystem.

Dependency graph of the book chapters.

JK flip-flop timing diagram of variables. Initially, J = K = 1, and Q toggles at every falling clk edge. At the sixth clock tick, the input signal K is set to 0, and later J also becomes 0.

A specification of a JK flip-flop.

Legal (left) and illegal (right) token ring configurations. The gray processes have tokens.

An asynchronous model of Dijkstras unidirectional token ring algorithm.

A generic leader election algorithm on a bidirectional ring.

3-bit ripple counter.

Trajectory of position (x), velocity (v), and input acceleration (a) for the simple car model of . To reach and stop at the target position of x = 30, the car applies a maximum acceleration (amax = 1) to reach the maximum speed, then cruises (a = 0) for a while, and finally applies maximum braking force (amin = 2).

A vehicle traveling in a single lane.

A pendulum.

Trajectories of the pendulum systems with friction (top) and without friction (bottom). Both systems have a stable equilibrium point at (0, 0) and an unstable equilibrium at (, 0). The system with friction is asymptotically stable, and without friction, it is only Lyapunov stable.

Kinematic (bicycle) model of a vehicle. Left: Stationary coordinates. Right: The rear-wheel no-slip condition in local coordinates rotated by .

Specification of the open-loop kinematic vehicle model.

Path following the trajectory of kinematic Vehicle model.

Trajectories of the simple economy model. Left: Phase portrait for the model of for = 3, = 1.5, k =.1, and g0 = 3. The sublevel sets of the Lyapunov function are shown in dotted lines. Right: Evolution of the solutions over time.

Simulated trajectories for the helicopter system of . Here, the midpoint method and the fourth-order RungeKutta method give almost indistinguishable simulated points, while the results from the Euler method differ significantly.

A closed-loop control system.

Motion of a rimless wheel down an inclined plane. Swinging around (left) and impact ( right).

HA model of RimlessWheel.

HA specification of a generic switched system.

Thermostat-heater system.

Graphical representation of the Thermostat HA.

An execution of RimlessWheel with six spokes. The discrete transitions punctuate the continuously evolving trajectories, bringing about instantaneous changes in the angular position and the angular speed .

An LTI HA with two stable modes and the trajectories of the individual modes. Left: HA. Right: Converging trajectories for the stable LTI modes (with mode0 in gray and mode1 in black).

Unstable (left) and stable (right) executions of HA that combine two individually stable linear systems.

Orbits for spacecraft docking. Initial orbit of active spacecraft (solid black), transfer orbit (dashed), and the orbit of the passive spacecraft (solid gray).

Satellite rendezvous system.

SATS airspace. Left: SATS airspace zones from a pilots perspective. The left and right zones are named from the perspective of the control tower. Right: Abstract model of the zones for the SATS automaton.

Small Aircraft Transportation System.

IOA model of an untimed FIFO channel.

The Lamport clock protocol.

Interconnection of the Lamport process and FifoCh channel automata: (M, 3). The arrows go from output to input.

Composed IOA (M, n).

A sample run of (M, 3). The occurrences of eventis are marked by black dots; arrows correspond to sendij and recvij actions. The numbers on the dots give the value of the clocki variable after the action updates the state.

Composing modified FlipFlops to create a leader-follower circuit.

Hybrid input/output model of FlipFlop from Chapter 2.

An HIOA model of a timed channel.

PulseGen automaton (left) and the Oscillator (right).

Sample execution of cardiac Oscillator composed with a PulseGen. Trajectories in mode are shown in black, and those in mode are in gray.

Sequence of n (=3) cars driving in the same lane, with automatic emergency braking (AEB). The safe-braking profile of 2 depends on the initial conditions and the behavior of the other drivers.

Composition of HIOA modeling AEB on single-lane highways. The parameters d12 and d23 are set to be equal to d.

A verification algorithm takes as input an automaton from a class of models and a requirement R from a class of requirements, and it either gives a proof establishing that all behaviors of meet R or gives a particular behavior of that violates R.

The states q0, q1, and q2 have labels {a}, {b, c}, and {c}, respectively.

A bouncing ball.

Fischers timing-based mutual exclusion protocol.

A hybrid automaton model of a process participating in Fischers mutual exclusion protocol.

An invariant set for the helicopter model. The tangent (gray), the normal (dashed gray) and the subtangential vector field (gray arrow) are shown for a particular point p on the boundary of the invariant.

Architecture of an SMT solver.

Timed automaton abstraction of the automaton