SWEN90010 Sample exam questions
In 2022 (as in 2020 and 2021) the exam will be on-line. So the format of the exam questions will be different from what has been used in prior years. However, this booklet contains a sample of pre 2020 exam style questions. You should use these to test your knowledge of the learning outcomes. But keep in mind that the style of exam questions on the final exam may be different.
Part A – Safety engineering
Question 1 [10 Marks]
Copyright By PowCoder代写 加微信 powcoder
Explain the purpose, the information derived from a typical analysis and the use of hazard analysis in the safety engineering process.
Question 2 [15 Marks]
Consider the following description of a nuclear power system, which controls the temperature of the nuclear core. The system consists of an array of sensors, three assessors, a voter, a controller, and an actuator. A system architecture is shown in Figure 1.
• There is an array of sensors monitoring the temperature of the core. Sensors are accurate to 0.1%, but can fail by not providing a reading, or by providing a reading outside of the 0.1% range.
• Three assessors each read the temperature signals sent from all sensors, and use a majority vote to determine the core temperature. Two sensor readings are considered sufficiently equal if they are within 0.4% of each other.
If any assessor detects that less than half of the sensors are sufficiently equal to the others, it should send a shutdown signal to the voter. Otherwise, it sends its estimated temperature.
• The voter using a voting algorithm to detect any non-functioning assessor. If the voter detects that more than one assessor has failed, or it receives a shutdown signal from any assessor, it should send a shutdown signal to the controller. Otherwise, it sends its estimated temperature to the controller.
• The controller controls the actuator by lowering or raising cooling rods into the core based on the estimated temperature sent from the voter. If it receives a shutdown signal, it will lower the rods completely and raise an alert.
• The actuator controls the rods. The level of the rods should be in correlation with the core temperature; that is, if the temperature is high, the rods should be lowered further into the core than if the temperature is low.
Figure 1: A system architecture for a nuclear reactor.
Perform a Hazard and Operability Study (HAZOP) on the assessors of this system, paying attention to any safety concerns. You will need to tabulate consequences, potential causes, and risks.
On a closed book exam, any question about HAZOP would include the HAZOP guidewords. Question 3 [15 Marks]
Choose one hazard from either of the previous two questions. Use fault-tree analysis to analyse causes of this hazard.
On a closed book exam, any question on fault tree analysis will include the symbols used for fault trees.
Part B – Model-based specification
Consider a simple scheduling module for a single processor. A set of processes are running on the system, but the processor can execute only one at each time. Each process must be in exactly one of the following states:
1. active: currently executing on the processor;
2. ready: not executing, but ready to be executed; or
3. waiting: waiting on some other resource, so not ready to be executed.
At any point, there must be at most one active process. There should be no ready processes if there is no active process — that is, the processor must be in use as much as possible.
Question 4 [7 Marks]
Model the state and state invariant of the single processor scheduler using an Alloy signature and predicate respectively. The signature should model all active, ready, and waiting processors, and the invariant predicate should model the constraints between them; e.g. only one active process at at time.
Your solution should assume the existence a signature ProcessID, which is the set of all process IDs, declared as follows:
sig ProcessID {}
Question 5 [5 Marks]
New processes can be added into the scheduling system. A new process must not be an existing process in the system. When a new process is added into the system, by default it is in the waiting state.
Model an operation called NewProcess as an Alloy predicate, which takes, as input, a process ID (ProcessID) and adds the process to the scheduling system.
Question 6 [7 Marks]
Model an operation called Ready as an Alloy predicate, which takes, as input, a process ID, and switches this process out of the waiting state. The specified process must be a waiting process. If there is no active process, the specified process becomes the new active process. Otherwise, it becomes a ready process.
Question 7 [7 Marks]
Model an operation called Swap as an Alloy predicate, which models the case of an active process switching into a waiting process; that is, the process has finished executing for now. In addition to swapping out the active process, the scheduler should select any of the ready processes to become the new active process. If there are no ready processes, then there is no new active process. This operation should take no input.
Part C – Fault-tolerant design Question 8
What is design diversity and how does it contribute to software redundancy?
Question 9
Do recovery blocks require design diversity? Justify your answer.
Question 10 [7 Marks]
Systems that must detect up to n non-malicious failures require 2n+1 redundant components. How many components do systems with malicious (or Byzantine) failures require to detect n failures? Why is this the case?
Part D – Correctness by construction
Question 11 [7 Marks]
You are working in a company that specialises in high-integrity software. SPARK is the imple- mentation language of choice. A new manager arrives at the company and shows a preference for switching to Ada instead of using the SPARK safe subset. The manager’s preference is based on a study that showed that more lines of code are required in safe programming language subsets than in the superset language to write the same program. The manager asserts that this increases the cost of the project.
Do you agree or disagree with the manager’s assertion?
Question 12 [3 Marks] Why did the designers of SPARK (prior to GNAT 2019) prohibit dynamic memory allocation?
Part E – Advanced Verification
Question 13 [3 Marks]
GNAT 2019 added limited support to SPARK for programs with dynamic memory allocation, by allowing limited reasoning about programs with pointers. Explain the problem of aliasing and how it complicates reasoning about programs with pointers. You might like to give an example program to illustrate.
Question 14
Would the following program satisfy SPARK’s aliasing restrictions?
procedure Pointers is
X : access Integer := new Integer’(5);
Y : access Integer := X;
X.all := 10;
end Pointers;
If so, explain why. If not, explain how to modify it so that it behaves identically but would satisfy the aliasing restrictions.
procedure PowerOfTwo(N : in Integer; Result : out Integer) with
Post => (Result = 2**N);
K : Integer;
Result := 1;
while K /= N loop
pragma Loop_Invariant (Result = 2**K);
K := K + 1;
Result := 2 * Result;
end PowerOfTwo;
Figure 2: An Ada program for calculating a power of two.
Question 15
Explain the meaning of the points-to “→” and separating conjunction “⋆” connectives in separation logic? You might like to give example assertions that use these connectives to explain them.
Question 16 [2 Marks] In the following assertion, explain why it implies that pointers p and q cannot alias:
Question 17
[12 Marks]
p → 10 ⋆ q → 10
NOTE: Many of the following questions require you do to Hoare logic proofs over Ada programs. On a real exam, however, Hoare logic questions would be written in the simple programming language explained in lectures on Hoare logic.
Figure 2 shows an Ada program for calculating the power of two of an integer. The postcondition is that Result = 2**N, in which 2**N is defined as:
2**0 =1 2**(N+1) = 2*(2**N)
The loop invariant has been provided. Using Hoare logic, show that this program either establishes its contract, or fails to establish its contract.
Question 18 [12 Marks]
Use Hoare logic to establish whether the following program establishes is contract or not. The loop invariant Min(A, J, MinIndex) is defined as follows:
Min(A, J, MinIndex) = for all I in Index range 1 .. J => (A(I) >= A(MinIndex)) 5
This states that the element at MinIndex is the smallest element found so far. subtype Index is Integer range 1 .. 10;
type IntArray is array(Index) of Integer;
procedure FindMinIndex(A : in IntArray; MinIndex : out Index) with
Post => (for all I in Index range 1 .. A’Length => (A(I) >= A(MinIndex)));
J : Index;
— find the minimum element in the list
MinIndex := 1;
while J < A’Length loop
pragma Loop_Invariant (Min(A, J, MinIndex));
J := J + 1;
if A(J) < A(MinIndex) then
MinIndex := J;
end FindMinIndex;
Question 19
Figure 3 shows an Ada program for calculating the average of an array of integers. The program includes a contract with the postcondition:
(if A’Length = 0 then Result = 0 else
Result = summation(1, A’Length) / A’Length);
where summation(X,Y) = Yi=X A(i).
The program loops through all elements in the array, keeping a running tally in the variable Sum.
(4 marks) Write down a suitable loop invariant for this program, which is suitable to establish the postcondition required at the end of the loop:
Result = summation(1, A’Length)
(2 marks) Use Hoare logic to show that if this postcondition holds at the end of the loop, then the remainder of the program will establish the postcondition in its contract above.
Question 20 [20 Marks]
Figure 4 contains a SPARK implementation of a binary search algorithm. The program assumes that the list is sorted, and also that the target is in the list. The postcondition is that the variable Index is the index of the variable Target in the array A. The predicate Sorted(A) is defined as:
Sorted(A) = for all I in Index range 1 .. A’Length - 1 => (A(I) <= A(I+1))
The loop invariant has been provided. It states that the precondition always holds (which is true 6
type IntArray is array(<>) of Integer;
procedure ListAverage(A : in IntArray; Result : out Float) with
Post => (if A’Length = 0 then Result = 0 else
else Result = summation(1, A’Length) / A’Length);
Sum, I : Integer;
while I /= A’Length loop
I := I + 1;
Sum := Sum + A(I);
if A’Length = 0 then
Result := 0;
Result := Sum / A’Length;
end ListAverage;
where summation(X,Y) = Yi=X A(i).
Figure 3: An Ada program for calculating the average from an array of integers.
because the list A never changes) and that the target always remains in the range [Low..Result]. Use Hoare logic to establish whether the following program establishes is contract or not.
procedure BinarySearch(A : in IntArray;
Target : in Integer;
Result : out Index) with
Pre => Sorted(A) and
(for some I in Index range 1 .. A’Length => (A(I) = Target)),
Post => A(Result) = Target;
Low : Index := Index’First;
Mid : Index;
Result := Index’Last;
while (Low < Result) loop
pragma Loop_Lnvariant (Sorted(A) and A(Low) <= Target and Target <= A(Result));
Mid := (Low + Result) / 2;
if A(Mid) < Target then
Low := Mid + 1;
Result := Mid;
end BinarySearch;
Figure 4: An Ada program implementing the binary search algorithm
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com