THE UNIVERSITY OF MELBOURNE Semester 1 Assessment, 2022 Department of Electrical and Electronic Engineering ELEN90066 Embedded System Design Reading/ 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 preempti
AAAB8HicbVA9 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作业君