sec in autonomus systems

Page 1

CPS 573: Security and Safety in Autonomous Systems, Fall 2021

University of Dayton

Homework Assignment 1, Due: 11:55 PM, 09/18/2021

Note: Students should start working on homework as early as possible. Please work by yourself

submit your solution as one file to Isidore.

Problem 1 (30 points): Consider a modified version of the Delay component, called OddDelay,

that has a Boolean input variable in, a Boolean output variable out, and two Boolean state variables

x and y. Both the state variables are initialized to 0, and the reaction description is given by:

if y then out := x else out := 0;

x := in;

y := ¬y.

a. Describe in words the behavior of the component OddDelay. (Hint: what is the output at odd

and even rounds?)

b. List a possible execution of the component if it is supplied with the sequence of inputs 0, 1, 1,

0, 1, 1, 1, 0, 0, 1 for the first tenth rounds.

c. Describe the component OddDelay as an extended-state machine with two modes. The mode

of the state machine should capture the value of the state variable y, while the state variable x

should be updated using assignments in the mode-switches.

d. Is the OddDelay component finite-state? Draw the corresponding Mealy machine.

Recall that Delay is:

Problem 2 (20 points): An Xor (Exclusive-Or) gate has two Boolean inputs 𝑖𝑛1 and 𝑖𝑛2, and a

Boolean output 𝑜𝑢𝑡. The output is 1 when exactly one of its two inputs are 1 and is 0 otherwise. Design the combinational component SyncXor to capture this desired functionality by composing

And, Or, and Not gates.

Problem 3 (30 points): In this problem, we will design a synchronous reactive component to set

the cruising speed of a vehicle. This component corresponds to the SetSpeed component in the

cruise-control system CruiseController. The SetSpeed component takes the following inputs:

– event(bool) cruise: This event models the user turning the cruise control on or off.

– nat speed: This input models the speed input from the vehicle (corresponds to the current

speed of the vehicle).

– event inc: This input models the user requesting an increase in the cruising speed.

– event dec: This input models the user requesting a decrease in the cruising speed.

It has one output:

– event(nat) cruiseSpeed: this output, if presents, contains the current cruising speed.

Page 2

The component maintains two state variables:

– an enumerated type variable called mode = {on, off} that keeps track of whether the

controller is turned on or off.

– a current desired (nat) speed s.

There are two constants called minSpeed and maxSpeed that we will use within the component.

The operation of the component is as follows. The component updates the state variable on

according to the following rule: every time the event cruise occurs, the variable mode is set to on.

Then the component outputs the cruising speed using the cruiseSpeed output variable. If the current

speed s is within the legal range minSpeed and maxSpeed, then the cruiseSpeed variable is set to

s; if not, it is set to the closest legal value (i.e. minSpeed or maxSpeed). Also, when mode is on, if

a dec event is received, then the cruising speed is decremented (restricting the lowest speed to

minSpeed), and when the inc event is received, the cruising speed is incremented (restricting the

highest speed to maxSpeed). If the mode variable is set to off, all input events except cruise are

ignored, and there is no output.

a. Show the synchronous reactive component that implements this functionality.

b. Suppose we want to add another input control for the driver, pause, with the following desired

behavior. When the cruise controller is on, if the driver presses pause, then the controller is

temporarily turned off. In the resulting paused state, the output cruiseSpeed should be absent,

and the events inc and dec should be ignored. Pressing pause again in this paused state should

resume the operation of the cruise controller, restoring the desired speed on pausing. Pressing

cruise in the paused state should switch the system off, and when the controller is off, pressing

pause should have no effect. Redesign the component SetSpeed with this additional input event

pause to capture the above specification. Hint: the component SetSpeed now maintains a state

variable mode that can be either on, paused, or off, i.e., mode = {on, paused, off}.

Problem 4 (20 points): We want to design an asynchronous process Split that is the dual of

Merge. The process Split has one input channel 𝑖𝑛 and two output channels 𝑜𝑢𝑡1 and 𝑜𝑢𝑡2. The messages received on the input channel should

be routed to one of the output channels in a

nondeterministic manner so that all possible

splittings of the input stream are feasible

executions. Describe all the components of the

desired process Split.

Asynchronous merge component

Problem 5 (Bonus 20 points): Consider the asynchronous process

Merge[𝑜𝑢𝑡 ↦ 𝑡𝑒𝑚𝑝] | Merge[𝑖𝑛1 ↦ 𝑡𝑒𝑚𝑝][ 𝑖𝑛2 ↦ 𝑖𝑛3]

obtained by connecting two instances of the process Merge. Show the “compiled” version of this

composite process. Explain the input/output behavior of this composite process.