程序代写案例-ELEN90066

欢迎使用51辅导,51作业君孵化低价透明的学长辅导平台,服务保持优质,平均费用压低50%以上! 51fudao.top
THE UNIVERSITY OF MELBOURNE
Semester 1 Assessment, 2022
Department of Electrical and Electronic Engineering
ELEN90066 Embedded System Design
Re
ading/ printing time: 30 minutes, Writing time: 180 minutes
Scanning and submission time: 30 minutes
This examination paper has 11 pages
Authorised materials:
This is a Zoom-supervised, hand-written exam where only the following materials are permitted:
• Printed copy of this exam paper and/or an offline electronic PDF reader.
• Any material available in hardcopy or stored electronically on a device disconnected from
communication networks.
• A4 paper, pens, pencils, ruler. Electronic devices may not be used for writing your answers.
• Any calculator model.
Instructions to students:
• Attempt ALL questions.
• The questions carry weight in proportion to the marks stated for each question number. These
marks total 100 marks.
• During Reading Time, you may print out a hardcopy of the exam. Alternatively, you may
download the exam to an electronic PDF reading device, which must then be disconnected
from the internet.
• During Writing Time you may only interact with the device running the Zoom session with
supervisor permission. The printed test paper (or offline device containing the test paper) and
any other working sheets must be visible to Zoom invigilators.
• Write your exam answers using pens/pencils and A4 paper. Start each question on a new page
and write down the question numbers.
• During Scan/Upload Time, assemble your pages in question number order, and use a mobile
phone or tablet to scan and combine them into a single PDF file. Check that all pages are
included and clearly readable.
• Submit your PDF file to the Gradescope Assignment corresponding to this exam. Confirm
with your Zoom supervisor that you have received confirmation of your submission.
• Collusion is not allowed under any circumstances. Collusion includes, but is not limited
to, talking to, phoning, emailing, texting or using the internet to communicate with others.
• Plagiarism, through the use of sources without proper acknowledgement or referencing, is not
permitted and can attract serious penalties. Plagiarism includes copying and pasting from the
Internet without clear acknowledgement and paraphrasing or presenting someone else’s work
as your own.
ELEN90066 Embedded System Design, Semester 1 Assessment, 2022
Question 1 (13 marks)
Consider the representation of a synchronous scheduler interacting with a set of tasks shown by the
diagram in Figure 1, where i ∈ {1, N} and N is the number of tasks in the system.
AAAB73icbVBNS8NAEJ34WetX1 aOXxSp4KkkR9Vjw4rGC/YA2lM120i7dbOLuplBC/4QXD4p49e94 89+4bXPQ1gcDj/dmmJkXJIJr47rfztr6xubWdmGnuLu3f3BYOj pu6jhVDBssFrFqB1Sj4BIbhhuB7UQhjQKBrWB0N/NbY1Sax/LRT BL0IzqQPOSMGiu1qVJ8jD3eK5XdijsHWSVeTsqQo94rfXX7MUsj lIYJqnXHcxPjZ1QZzgROi91UY0LZiA6wY6mkEWo/m987JRdW6ZM wVrakIXP190RGI60nUWA7I2qGetmbif95ndSEt37GZZIalGyxKE wFMTGZPU/6XCEzYmIJZYrbWwkbUkWZsREVbQje8surpFmteNeV6 sNVuXaex1GAUziDS/DgBmpwD3VoAAMBz/AKb86T8+K8Ox+L1jUn nzmBP3A+fwA+3ZAE
arrivei
AAAB7XicbVBNS8NAEJ3Ur1q/q h69BKvgqSRF1GPBi8cK9gPaUDabSbt2sxt2N0Ip/Q9ePCji1f/j zX/jts1BWx8MPN6bYWZemHKmjed9O4W19Y3NreJ2aWd3b/+gfH jU0jJTFJtUcqk6IdHImcCmYYZjJ1VIkpBjOxzdzvz2EyrNpHgw4 xSDhAwEixklxkqtSArss3654lW9OdxV4uekAjka/fJXL5I0S1AY yonWXd9LTTAhyjDKcVrqZRpTQkdkgF1LBUlQB5P5tVP33CqRG0t lSxh3rv6emJBE63ES2s6EmKFe9mbif143M/FNMGEizQwKulgUZ9 w10p297kZMITV8bAmhitlbXTokilBjAyrZEPzll1dJq1b1r6q1+ 8tK/SyPowgncAoX4MM11OEOGtAECo/wDK/w5kjnxXl3PhatBSef OYY/cD5/AJc8jw0=
donei
AAAB7HicbVBNS8NAEJ34WetX1 aOXxSp4KkkR9Vjw4rGCaQttKJvtpF262YTdjVBCf4MXD4p49Qd5 89+4bXPQ1gcDj/dmmJkXpoJr47rfztr6xubWdmmnvLu3f3BYOT pu6SRTDH2WiER1QqpRcIm+4UZgJ1VI41BgOxzfzfz2EyrNE/loJ ikGMR1KHnFGjZV8lck+71eqbs2dg6wSryBVKNDsV756g4RlMUrD BNW667mpCXKqDGcCp+VepjGlbEyH2LVU0hh1kM+PnZILqwxIlCh b0pC5+nsip7HWkzi0nTE1I73szcT/vG5motsg5zLNDEq2WBRlgp iEzD4nA66QGTGxhDLF7a2EjaiizNh8yjYEb/nlVdKq17zrWv3hq to4L+IowSmcwSV4cAMNuIcm+MCAwzO8wpsjnRfn3flYtK45xcwJ /IHz+QP1vI6yruni
AAAB8HicbVDLSgMxFL1TX7W+q i7dBKvgqswUUZcFNy4r2Ie0Q8mkd9rQZGZIMkIZ+hVuXCji1s9x 59+YtrPQ1gOBwznnkntPkAiujet+O4W19Y3NreJ2aWd3b/+gfH jU0nGqGDZZLGLVCahGwSNsGm4EdhKFVAYC28H4dua3n1BpHkcPZ pKgL+kw4iFn1Fjp0WZRJqbP++WKW3XnIKvEy0kFcjT65a/eIGap xMgwQbXuem5i/Iwqw5nAaamXakwoG9Mhdi2NqETtZ/OFp+TcKgM Sxsq+yJC5+nsio1LriQxsUlIz0sveTPzP66YmvPEzHiWpwYgtPg pTQUxMZteTAVfIjJhYQpnidlfCRlRRZmxHJVuCt3zyKmnVqt5Vt XZ/Wamf5XUU4QRO4QI8uIY63EEDmsBAwjO8wpujnBfn3flYRAtO PnMMf+B8/gAXMpCC
preemptiAAAB8HicbVA9 SwNBEJ2LXzF+RS1tFqNgFe5Sq GXAxjKi+ZDkCHt7c8mS3btjd08 IIb/CxkIRW3+Onf/GTXKFJj4Y eLw3w8y8IBVcG9f9dgpr6xubW8 Xt0s7u3v5B+fCopZNMMWyyRCS qE1CNgsfYNNwI7KQKqQwEtoPRz cxvP6HSPIkfzDhFX9JBzCPOqL HS4z0bYpgJVP1yxa26c5BV4uW kAjka/fJXL0xYJjE2TFCtu56bG n9CleFM4LTUyzSmlI3oALuWxl Si9ifzg6fk3CohiRJlKzZkrv6e mFCp9VgGtlNSM9TL3kz8z+tmJ rr2JzxOM4MxWyyKMkFMQmbfk5A rZEaMLaFMcXsrYUOqKDM2o5IN wVt+eZW0alXvslq7q1XqZ3kcR TiBU7gAD66gDrfQgCYwkPAMr/D mKOfFeXc+Fq0FJ585hj9wPn8A 242QWg==
Scheduler
AAAB73icbVA9SwNBEJ2LXzF+R S1tFhPBKtylUMuAjZVEyBckR9jbzCVL9vbO3T0hhPwJGwtFbP07 dv4bN8kVmvhg4PHeDDPzgkRwbVz328ltbG5t7+R3C3v7B4dHxe OTlo5TxbDJYhGrTkA1Ci6xabgR2EkU0igQ2A7Gt3O//YRK81g2z CRBP6JDyUPOqLFSp0H1mJTvy/1iya24C5B14mWkBBnq/eJXbxCz NEJpmKBadz03Mf6UKsOZwFmhl2pMKBvTIXYtlTRC7U8X987IhVU GJIyVLWnIQv09MaWR1pMosJ0RNSO96s3F/7xuasIbf8plkhqUbL koTAUxMZk/TwZcITNiYgllittbCRtRRZmxERVsCN7qy+ukVa14V 5XqQ7VUK2dx5OEMzuESPLiGGtxBHZrAQMAzvMKb8+i8OO/Ox7I1 52Qzp/AHzucPq7aO+g==
Task N
AAAB73icbVA9SwNBEJ3zM8avq KXNYiJYhbsUahmwsYyQL0iOMLfZS5bs7Z27e0I48idsLBSx9e/Y +W/cJFdo4oOBx3szzMwLEsG1cd1vZ2Nza3tnt7BX3D84PDounZ y2dZwqylo0FrHqBqiZ4JK1DDeCdRPFMAoE6wSTu7nfeWJK81g2z TRhfoQjyUNO0Vip20Q9IRVeGZTKbtVdgKwTLydlyNEYlL76w5im EZOGCtS657mJ8TNUhlPBZsV+qlmCdIIj1rNUYsS0ny3unZFLqwx JGCtb0pCF+nsiw0jraRTYzgjNWK96c/E/r5ea8NbPuExSwyRdLg pTQUxM5s+TIVeMGjG1BKni9lZCx6iQGhtR0Ybgrb68Ttq1qnddr T3UyvVKHkcBzuECrsCDG6jDPTSgBRQEPMMrvDmPzovz7nwsWzec fOYM/sD5/AHUvY8V
Task i
Figure 1: Interaction between scheduler and a number of tasks
Each task is an independent process that communicates with the scheduler process responsible for
allocation of processor time via events on its output lines. Assume that the scheduler is scheduling
tasks for a uniprocessor system, and that only one task can be running at any one time.
Initially a task is idle. When task i needs processing time, it communicates with the scheduler using
the pure signal arrivei and will then wait until the scheduler decides to allocate the processor to the
task. The scheduler notifies the task of this using the pure signal runi and task i proceeds to run.
When the current instance of the task finishes its execution, it communicates with the scheduler
using the pure signal donei and returns to being idle.
The scheduler is able to preempt task i before it is complete via the pure signal preempti and then
allocate the processor to another task j that had already arrived using the runj signal.
(a) [4 marks] Draw a three-state Finite State Machine representing the operation of a task under
this model with the following inputs and outputs:
input: runi, preempti : pure
outputs: arrivei, donei : pure
(b) [6 marks] Consider the case where there are only two tasks and Task 1 has higher priority; that
is, if Task 2 is running and Task 1 needs processing time, Task 2 will be preempted and Task
1 will be given processor time. Draw a Finite State Machine representing the operation of the
scheduler under this model with the following inputs and outputs:
inputs: arrive1, done1, arrive2, done2 : pure
output: run1, preempt1, run2, preempt2 : pure
(c) [3 marks] Consider the LTL expression G¬(run1 ∧ run2). Is this an invariant, safety and/or
liveness property? Does it hold for the FSM you designed in part (b)? Explain your answer.
Page 2 of 11
ELEN90066 Embedded System Design, Semester 1 Assessment, 2022
Question 2 (16 marks)
A basic obstacle avoidance control algorithm for a robot is modelled by the Finite State Machine
(FSM), S, given below
variable: x: {0, · · · , 1500}
inputs: bump, go : pure
outputs: mL, mR ∈ R : mL, mR ∈ [−1, 1]
Idle Forwards
ReverseTurn
/ mL,mR = 0
x := 0
/ mL,mR = 0
go / mL,mR = 0.8
bump / mL,mR = −0.5
x := 0
/ mL,mR = 0.8
/ mL,mR = −0.5
x := x+ 1
x ≥ 1000 / mL = 0.8,mR = 0.4
x := 0
/ mL = 0.8,mR = 0.4
x := x+ 1
x ≥ 500 / mL,mR = 0.8
Figure 2: Robot FSM for Question 2
The input bump models a momentary contact switch by a pure signal that is only present when the
front of the robot has bumped into an object. The input go is a pure signal that results only when
a ‘go’ button is pushed on the robot’s body in order to initiate its obstacle avoidance manoeuvrers.
The motor outputs mL and mR are real number valued in the range [−1, 1] that represent a fraction
of full speed for the left and right motors, respectively, with a negative number indicating the
motor is to run in reverse. For example, (mL,mR) = (1, 1) would drive the robot straight ahead
at full speed, (mL,mR) = (1, 0.5) would cause the robot to make an arc turn to the right, and
(mL,mR) = (−0.5,−0.5) would cause the robot to reverse at 50% speed.
The model is time triggered by a signal that causes the machine to react once every millisecond.
Question 2 continues over the next page.
Page 3 of 11
ELEN90066 Embedded System Design, Semester 1 Assessment, 2022
Question 2 (continued)
(a) [2 marks] How many states does this state machine have?
(b) [2 marks] Give an execution trace of the Finite State Machine for the input sequence for
(go, bump) given by:
((present, absent), (absent, absent), (absent, absent), (absent, present), (present, absent)).
(c) [8 marks] For each of the following LTL formulae, determine whether it is TRUE or FALSE for
the FSM given in Figure 2. You MUST give an explanation for your answer. If FALSE, give a
counterexample.
(i) G(mL < 1)
(ii) F(mR ≤ 0)
(iii) FG(mL > mR)
(iv) GF(¬bump) =⇒ (¬FReverse)
(v) (G bump) =⇒ GF(x > 0)
(vi) (mL ≥ mR)
(vii) (mL = mR)U(bump)
(viii) G(Forwards =⇒ X2Turn)
(c) [4 marks] In order to perform model verification, a model of the environment, E, needs to be
constructed so that composing it with the robot control FSM, S, from Figure 2, yields a closed
system M . This can be represented by the following block diagram:
AAACBHicbVC7TsMwFHV4lvAKM HaJKEhMVdIBGCuxsCAVQR9SE1WOc9NadZzIdpCiqAMLv8LCAEKs fAQbf4PbZoCWI13p6Jx77XtPkDIqleN8Gyura+sbm5Utc3tnd2 /fOjjsyCQTBNokYYnoBVgCoxzaiioGvVQAjgMG3WB8NfW7DyAkT fi9ylPwYzzkNKIEKy0NrKpHgCsQlA8L8y6XCmLPM2+SENhkYNWc ujODvUzcktRQidbA+vLChGSxfpEwLGXfdVLlF1goShhMTC+TkGI yxkPoa8pxDNIvZkdM7FOthHaUCF1c2TP190SBYynzONCdMVYjue hNxf+8fqaiS7+gPM0UcDL/KMqYrRJ7mogdUgFEsVwTTATVu9pkh AUmOhZp6hDcxZOXSadRd8/rjdtGrXlSxlFBVXSMzpCLLlATXaMW aiOCHtEzekVvxpPxYrwbH/PWFaOcOUJ/YHz+AJYXl/U=
System
Model
AAAB8nicbVDL SgMxFL1TX7W+qi7dBKvgqsx0o S4LIrisYB8wHUomzbShmWRIMoU y9DPcuFDErV/jzr8x085CWw8E DufcQ+49YcKZNq777ZQ2Nre2d8 q7lb39g8Oj6vFJR8tUEdomkkv VC7GmnAnaNsxw2ksUxXHIaTec3 OV+d0qVZlI8mVlCgxiPBIsYwc ZK/r2YMiVFTIUZVGtu3V0ArRO vIDUo0BpUv/pDSdI8SzjW2vfcx AQZVoYRTueVfqppgskEj6hvqc Ax1UG2WHmOLq0yRJFU9gmDFurv RIZjrWdxaCdjbMZ61cvF/zw/N dFtkDGRpIYKsvwoSjkyEuX3oyF TlBg+swQTxeyuiIyxwsTYliq2 BG/15HXSadS963rjsVFrXhR1l OEMzuEKPLiBJjxAC9pAQMIzvMK bY5wX5935WI6WnCJzCn/gfP4A oriRZA==
Environment
AAAB6HicbVDLSgNBEOyNrxhfU Y9eBoOQU9gNoh4DXrwICZgHJEuYnfQmY2Znl5lZIYR8gRcPinj1 k7z5N06SPWhiQUNR1U13V5AIro3rfju5jc2t7Z38bmFv/+DwqH h80tJxqhg2WSxi1QmoRsElNg03AjuJQhoFAtvB+Hbut59QaR7LB zNJ0I/oUPKQM2qs1LjvF0tuxV2ArBMvIyXIUO8Xv3qDmKURSsME 1brruYnxp1QZzgTOCr1UY0LZmA6xa6mkEWp/ujh0Ri6sMiBhrGx JQxbq74kpjbSeRIHtjKgZ6VVvLv7ndVMT3vhTLpPUoGTLRWEqiI nJ/Gsy4AqZERNLKFPc3krYiCrKjM2mYEPwVl9eJ61qxbuqVBuXp Vo5iyMPZ3AOZfDgGmpwB3VoAgOEZ3iFN+fReXHenY9la87JZk7h D5zPH5+FjL4=
M
AAAB6HicbVDLTgJBEOzFF+IL9 ehlIjHhRHaJUY8kXjxClEcCGzI79MLI7OxmZtaEEL7AiweN8eon efNvHGAPClbSSaWqO91dQSK4Nq777eQ2Nre2d/K7hb39g8Oj4v FJS8epYthksYhVJ6AaBZfYNNwI7CQKaRQIbAfj27nffkKleSwfz CRBP6JDyUPOqLFS475fLLkVdwGyTryMlCBDvV/86g1ilkYoDRNU 667nJsafUmU4Ezgr9FKNCWVjOsSupZJGqP3p4tAZubDKgISxsiU NWai/J6Y00noSBbYzomakV725+J/XTU1440+5TFKDki0XhakgJi bzr8mAK2RGTCyhTHF7K2EjqigzNpuCDcFbfXmdtKoV76pSbVyWa uUsjjycwTmUwYNrqMEd1KEJDBCe4RXenEfnxXl3PpatOSebOYU/ cD5/AKidjMQ=
S
AAAB6HicbVDL SgNBEOyNrxhfUY9eBoOQU9gNo h4DInhMwDwgWcLspDcZMzu7zMw KIeQLvHhQxKuf5M2/cZLsQRML Goqqbrq7gkRwbVz328ltbG5t7+ R3C3v7B4dHxeOTlo5TxbDJYhG rTkA1Ci6xabgR2EkU0igQ2A7Gt 3O//YRK81g+mEmCfkSHkoecUW Olxl2/WHIr7gJknXgZKUGGer/ 41RvELI1QGiao1l3PTYw/pcpwJ nBW6KUaE8rGdIhdSyWNUPvTxa EzcmGVAQljZUsaslB/T0xppPUk CmxnRM1Ir3pz8T+vm5rwxp9ym aQGJVsuClNBTEzmX5MBV8iMmFh CmeL2VsJGVFFmbDYFG4K3+vI6 aVUr3lWl2rgs1cpZHHk4g3Mog wfXUIN7qEMTGCA8wyu8OY/Oi/P ufCxbc042cwp/4Hz+AJNljLY=
E
Devise an FSM model of the environment, E, that provides inputs to the FSM, S, that would
then be suitable for model verification against some specification. Be sure to specify the outputs
of the model and their types.
Page 4 of 11
ELEN90066 Embedded System Design, Semester 1 Assessment, 2022
Question 3 (18 marks)
Consider a model of a synchronous buffer that accepts integers in the range [0, 127], via an input
port in, and outputs them via an output port out after a certain delay. A block diagram of the
input and output of the buffer is shown in Figure 3.
input: in ∈ {0, . . . , 127}
output: out ∈ {0, . . . , 127}
Buffer
in out
Figure 3: Synchronous buffer for Question 3
The buffer is time triggered – that is, it reacts once on every positive edge of a periodic clock signal
(not shown on the block diagram). The buffer has a capacity of one integer, so that whenever an
input value is supplied to the empty buffer it is stored in an internal memory, causing the buffer to
be full. When the buffer is full, it simply ignores (and therefore loses) further inputs until it gets a
chance to output the stored value to the output out.
The delay between the reception of an input value and the transmission of the corresponding output
value is at least LB and at most UB time units, respectively. In other words, the buffer can produce
the output only after the lower bound LB (time units) on the delay and is guaranteed to produce the
output within the upper bound UB (time units) of receiving an input. It is assumed that each time
unit is equal to one clock cycle.
(a) [5 marks] Draw an Extended Finite State Machine modelling the behaviour of the synchronous
buffer as described above. You can consider the buffer to have two main states, Empty and Full.
Be sure to list any variables defined as part of the machine.
How many states would the Extended Finite State Machine have if it were converted to a regular
Finite State Machine, i.e. one with no variables in use? Explain your answer.
Question 3 continues over the next page.
Page 5 of 11
ELEN90066 Embedded System Design, Semester 1 Assessment, 2022
Question 3 (continued)
(b) [10 marks] Consider two instances of the synchronous buffer connected in series as shown in
Figure 4.
input: in ∈ {0, . . . , 127}
output: out ∈ {0, . . . , 127}
Buffer 1 Buffer 2
in out
Figure 4: Synchronous buffers in series
The delay between the reception of an input value and the transmission of the corresponding
output value is at least LBi and at most UBi time units, respectively, for each buffer, where
i ∈ {1, 2} refers to the buffer number.
Draw the flattened, Extended Finite State machine resulting from this composition. Be sure to
list any variables defined as part of the composed machine.
(c) [3 marks] Assume that UB1 < LB2 for the composition in Figure 4. Does this assumption always
guarantee that no information is lost in between the buffers (i.e. Buffer 2 not being ready to
accept Buffer 1’s output)? Explain your answer, either by providing a proof or a counterexample.
Page 6 of 11
ELEN90066 Embedded System Design, Semester 1 Assessment, 2022
Question 4 (10 marks)
For all compositions in this question, you are to assume a Synchronous Reactive Model of Compu-
tation.
(a) [2 marks] Consider a system A modelled by the Finite State Machine (FSM) inside the rect-
angle, connected with the output being fed back into the input:
input: c :pure
output: d :pure
s1 s2
¬c/d
c/d
c/¬d
¬c/¬d
A
Is the feedback composition is well-formed? Explain your answer.
(b) [4 marks] Consider the cascade composition of two instances of system A. Let the input and
output of the cascaded system be x and y, respectively, as shown in the block diagram below:
input: x :pure
output: y :pure
x
A
y
A
Construct a single, flattened FSM representing the composition of the cascade interconnection.
Question 4 continues over the next page.
Page 7 of 11
ELEN90066 Embedded System Design, Semester 1 Assessment, 2022
Question 4 (continued)
(c) [4 marks] Consider now the the feedback loop x = y around the cascade composition from part
(b), as shown in the block diagram below:
input: x :pure
output: y :pure
x y
A A
Show that the feedback composition above is well-formed and construct the flattened Finite State
Machine model for the composite system.
Page 8 of 11
ELEN90066 Embedded System Design, Semester 1 Assessment, 2022
Question 5 (16 marks)
Consider six tasks τ1, ..., τ6 with execution times, and deadlines presented below. Assume that all
tasks are released at time t = 0.
τ1 τ2 τ3 τ4 τ5 τ6
execution time, ei 2 3 1 3 3 2
deadline, di 6 5 8 10 12 14
(a) [2 marks] Does a scheduling approach based on Earliest Deadline First (EDF) yield a feasible
schedule? Explain why if the answer is ‘no’, or construct the schedule if the answer is ‘yes’.
(b) [4 marks] We say task τi precedes task τj if the predecessor must complete the execution of τi
before τj can execute. The precedence relationships between tasks τ1, ...,τ6 are as the following
• τ1 precedes τ2;
• τ2 precedes τ4;
• τ2 precedes τ3;
• τ3 precedes τ5;
• τ4 precedes τ5;
• τ5 precedes τ6.
Draw the directed acyclic graph representing the precedence of the tasks where a directed edge
marks a precedence.
(c) [8 marks] Now consider the same list of tasks τ1, ..., τ6, but now with release times, execution
times, and deadlines as given in the table below:
τ1 τ2 τ3 τ4 τ5 τ6
release time, ri 0 2 7 3 4 2
execution time, ei 2 3 1 3 3 2
deadline, di 6 5 8 10 12 14
Does Earliest Deadline First with Precedence (EDF*) yield a feasible schedule for the precedences
given in (b)? Explain why if the answer is ‘no’, and construct the schedule if the answer is ‘yes’.
You must provide sufficient reasoning for your answer.
(d) [2 marks] What is the maximum lateness for the scheduling scheme implemented in (c)? Is this
value minimised? Explain your answer.
Page 9 of 11
ELEN90066 Embedded System Design, Semester 1 Assessment, 2022
Question 6 (12 marks)
Consider Finite State Machines Σ1 and Σ2 depicted in Figure 5.
input: a, b :pure
output: y0 :pure
x0
x1
x2 x3
a/
true/
true/
true/¬y0
true/y0
(a) System Σ1
input: a :pure
output: y0 :pure
y0
y1 y2
y3 y4
a/ a/
true/ true/
true/¬y0
true/y0
(b) System Σ2
Figure 5: Systems Σ1 and Σ2 for Question 6.
(a) [5 marks] Is Σ1 simulated by Σ2? Prove your answer.
(b) [5 marks] Is Σ2 simulated by Σ1? Prove your answer.
(c) [2 marks] Are Σ1 and Σ2 bisimilar? Prove your answer.
Page 10 of 11
ELEN90066 Embedded System Design, Semester 1 Assessment, 2022
Question 7 (15 marks)
Figure 6 depicts an above view of the area of operation of a robot, where at any one time, the robot
is in one of the square regions Ri, where i ∈ {1, 2, ..., 6}.
R2 R4 R6
R1 R3 R5
Figure 6: Area of operation of a robot for Question 7.
The state of the robot can be considered to be the region it is currently in. On every reaction, the
robot can either remain in its current region or move only to another region that shares a common
edge with its current region. For example, it would NOT be permitted to make the diagonal move
R1 → R4 in a single reaction as R1 and R4 are not adjacent and do not share a common edge. Let
the logical proposition ri correspond to the robot being in region Ri.
(a) [4 marks] Draw a non-deterministic Finite State Machine (FSM), with no inputs or outputs,
that models the robot’s behaviour. Assume that the robot starts in R1.
(b) [4 marks] What does the LTL formula φ as defined below mean? Provide both a natural
language translation, and an interpretation, of the specification.
φ := ri ∧ Fr2 ∧ Fr3 ∧G¬r6
(c) [3 marks] Is it possible for the robot to meet specification φ? Explain.
(d) [4 marks] Consider now the case where there is a single obstacle. The obstacle is initially located
in R3, and, on every reaction, it can either remain in its current region or move only to another
region that is adjacent to the region it is currently in (i.e. it moves similarly to the robot). The
obstacle is shown as a shaded square in R3 in Figure 7.
R2 R4 R6
R1 R3 R5
Figure 7: Indicating initial obstacle position for Question 7.
The robot and the obstacle cannot co-exist in the same region at the same time and therefore
neither can move into the other’s region on a particular reaction.
If the starting region of the obstacle is R3, and the robot starts in R1, can the LTL specification
GFr5 be satisfied by the robot? You must explain your answer to receive marks.
END OF EXAMINATION
Page 11 of 11

欢迎咨询51作业君
51作业君

Email:51zuoyejun

@gmail.com

添加客服微信: abby12468