The University of Melbourne SWEN90010: High Integrity Systems Engineering
Learning Outcomes
By the end of this subject, a student should be able to do the following (categorised by chapters in the course notes):
Chapter 1 — An Introduction to HISE
Copyright By PowCoder代写 加微信 powcoder
• Define the term “high-integrity system”
• Define the different classes of high-integrity system
Chapter 2 — Safety and Security engineering
• Explain the role of safety engineering in the system engineering lifecycle. • Discuss the role of accidents and incidents in the safety analysis process • Perform a preliminary hazard analsyis using the HAZOP method
• Apply the fault-tree analysis method to a system for a given fault
• Explain the role of threat modelling for building secure systems
• Apply the STRIDE methodology to enumerate security threats to a system design
Chapter 3 — Model-based specification
• Explain the advantages and disadvantages of formal model-based specification in software engineering
• Apply basic logic, set/relational theory concepts to software-based problems
• Model a domain using the Alloy language
• Define and check assertions using the Alloy language and tool
• Model and reason about (properties of) execution sequences in Alloy
Chapter 4 — Ada
• Describe the features of Ada that make it suitable for high-integrity software • Read, write, and modify basic Ada programs
Chapter 5 and Section 6.3 — SPARK
• Describe the features of SPARK that make it suitable for high-integrity software
• Read and write basic SPARK programs
• Understand what the SPARK Examiner checks of SPARK programs
• Read and write basic preconditions and postconditions for SPARK programs.
• Read and write loop invariants for SPARK programs to enable the SPARK Prover to prove that they meet their specifications.
Chapter 7 — Reasoning about program correctness
• Explain the advantages and disadvantages of program proof compared to other program verification techniques.
• Explain the meaning of Hoare logic statements: {P } S {Q}
• Devise appropriate loop invariants for reasoning about loops using Hoare logic
• By hand, prove the correctness or otherwise of small programs using Hoare logic
Chapter 8 — Advanced Verification
• Explain what Ghost Code is and why it is useful when verifying practical programs e.g. in the SPARK Prover
• Explain the problem of pointer aliasing and why it complicates reasoning about programs
• Explain the simple aliasing restrictions of SPARK
• Write and read simple pre- and post-conditions written in separation logic
Chapter 9 — Fault-tolerant design
• Explain the concept of fault tolerance in systems engineering
• Compare hardware and software fault tolerance
• Design, analyse, and critique a fault-tolerant hardware design
• Design, analyse, and critique a fault-tolerant software design
• Implement algorithms for majority voting, median voting, and k-plurality voting
• Compare and contrast the different voting algorithms, and evaluate their use in specific systems
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com