that has been optimised according to your answers to parts (a) and (b) above? [4 marks] (d) Two processors on a SoC have separate address spaces. What does this mean? Describe a simple hardware mechanism for sending non-trivial amounts of data between processors in separate address spaces. Interrupts should be used. [4 marks] (e) Briefly describe both a high-level and a mid-level model of your answer to part (d) where the mid-level model requires minimal or no modification to the device driver firmware but is not a net-level model and where the high-level model dispenses with much of the device driver code and many or all of the interrupts. [3 marks each] 10 CST.2011.9.11 11 Temporal Logic and Model Checking (a) Explain the difference between static and dynamic methods for property checking. Is LTL or CTL a better property language for dynamic checking? Justify your answer. [4 marks] (b) Outline an algorithm for model checking LTL properties of the form G p

where p is an atomic property. [4 marks] (c) What is the difference between explicit state and symbolic model checking? [4 marks] (d) Who is the person credited with introducing temporal logic as a property specification language? What were the main contributions of Clarke & Emerson