High Integrity Systems Engineering Subject Notes for SWEN90010
School of Computing and Information Systems
The University of Melbourne
Copyright By PowCoder代写 加微信 powcoder
1 Introduction to High Integrity Systems Engineering 7
1.1 Subjectinformation………………………………. 7 1.2 Introductiontohighintegritysystems ……………………… 9 1.3 Subjectoutline ………………………………… 10
2 Safety-critical and Security-critical systems engineering 12
2.1 Anintroductiontosoftwaresafety ……………………….. 12
2.2 Whysafetyengineering? ……………………………. 13
2.3 Safetyengineering ………………………………. 15
2.4 Accidentsandsafetyengineering………………………… 16
2.4.1 CaseStudy:TheA320Airbus ……………………… 17 2.4.2 Casestudy:Warsaw,Okecie–14September1993 . . . . . . . . . . . . . . . . 20 2.4.3 CaseStudy:Boeing737MAX……………………… 22 2.4.4 Theroleofaccidentanalysisinsafetyengineering . . . . . . . . . . . . . . . . 25
2.5 Toolsandtechniquesforsafetyengineering …………………… 27 2.5.1 Safetystandardsandsafetylifecycles ………………….. 27 2.5.2 Preliminaryhazardanalysis ………………………. 28
2.6 HazardAnalysisMethods……………………………. 31 2.6.1 HAZOPS……………………………….. 31 2.6.2 FaultTreeAnalysis…………………………… 37 2.6.3 FMEA ………………………………… 39
2.7 ThreatModellingforSecurity …………………………. 42 2.7.1 TheSTRIDEMethod………………………….. 42 2.7.2 AttackTrees ……………………………… 45
3 Model-based specification
3.1 Whatisformalspecification?………………………….. 49
3.2 Whatismodel-basedspecification?……………………….. 50
3.3 Thecostsofformalspecification………………………… 51
3.4 Logicandsettheory………………………………. 53
3.5 IntroductiontoAlloy ……………………………… 55
3.5.1 Keycharacteristics …………………………… 55
3.6 AlloyLogic………………………………….. 56
3.6.1 Everythingisarelation…………………………. 56
3.6.2 Operators……………………………….. 57
3.6.3 Temporal Logic: specifying systems that change over time . . . . . . . . . . . . 61
3.7 AlloyLanguage………………………………… 61 3.7.1 Modules ……………………………….. 61 3.7.2 Signatures……………………………….. 62 3.7.3 Facts …………………………………. 62 3.7.4 Predicates……………………………….. 63 3.7.5 Functions……………………………….. 64 3.7.6 Assertions……………………………….. 64 3.7.7 ThecompleteLastPassexample …………………… 65
3.8 AnalysiswiththeAlloyAnalyser………………………… 67 3.8.1 Runs …………………………………. 67 3.8.2 Checks ………………………………… 67 3.8.3 Scope…………………………………. 68
3.9 Abstraction and incremental specification of state machines using Alloy operators . . . . 69 3.9.1 Thespecificationprocess………………………… 69
3.10Trace-BasedModellinginAlloy ………………………… 73 3.11Verificationandvalidation …………………………… 74
4 Introduction to Ada 78
4.1 ThehistoryofAda ………………………………. 78 4.2 Adaforprogramming“inthelarge” ………………………. 79 4.3 HelloWorld………………………………….. 79 4.4 Specificationsandprogrambodies ……………………….. 81 4.5 Comments…………………………………… 83 4.6 Types …………………………………….. 83
4.6.1 ThepredefinedAdatypesystem…………………….. 83 4.6.2 Arrays…………………………………. 85 4.6.3 Definingnewtypes…………………………… 86
4.7 ControlStructures……………………………….. 87
4.8 ProceduralAbstractionsandFunctionalAbstractions . . . . . . . . . . . . . . . . . . . 90 4.8.1 ParameterModes……………………………. 90 4.8.2 Callingsubprograms ………………………….. 90
4.9 accessTypes:PassingParametersByReference ……………….. 91 4.9.1 AccessTypestoRead-OnlyData ……………………. 94 4.9.2 Summary……………………………….. 94
4.10Example:Insertionsort…………………………….. 94 4.11Concurrencywithtasks…………………………….. 95 4.12Furtherreading ………………………………… 98
5 Safe programming language subsets 100
5.1 Principlesofcorrectnessbyconstruction……………………..100
5.2 Safeprogramminglanguagesubsets ……………………….101
5.3 SPARK …………………………………….103
5.3.1 SPARKStructure…………………………….103
5.3.2 WhatisleftoutofAda? …………………………104
5.3.3 Why bother with SPARK or other safe programming language subsets? . . . . . 106
5.4 SPARKExaminer………………………………..107 5.4.1 Annotations……………………………….107 5.4.2 SPARKExaminer ……………………………108
6 Design by contract 111
6.1 IntroductiontoDesignbyContract………………………..111 6.1.1 History …………………………………111 6.1.2 SomeDefinitions…………………………….112
6.2 SpecifyingADTinterfaces……………………………112 6.2.1 ADTinterfacesasnatural-languagecomments . . . . . . . . . . . . . . . . . . 112 6.2.2 ADT interfaces as invariants, preconditions, and postconditions . . . . . . . . . 113 6.2.3 ADTinterfacesascontracts ……………………….114 6.2.4 Formalcontracts …………………………….116
6.2.5 Advantagesanddisadvantagesofformalcontracts . . . . . . . . . . . . . . . . 117
6.3 ContractsinSPARK ………………………………117 6.3.1 Syntax …………………………………117 6.3.2 SimilaritytoAlloy ……………………………121 6.3.3 Tools ………………………………….121
6.4 Additionalreading ……………………………….121
7 Reasoning about program correctness 122
7.1 Introductiontoreasoningaboutprograms …………………….123 7.1.1 Thecorrectnessofbinarysearch……………………..123
7.2 Asmallprogramminglanguage………………………….125
7.3 Hoarelogic …………………………………..126 7.3.1 IntroductiontoHoarelogic………………………..126
7.3.2 Anintroductoryexample—Incrementinganinteger . . . . . . . . . . . . . . . 127
7.4 TherulesofHoarelogic …………………………….127 7.4.1 Assignmentaxiom ……………………………127 7.4.2 Consequencerule…………………………….128 7.4.3 Sequentialcompositionrule ……………………….129 7.4.4 Emptystatementaxiom …………………………132 7.4.5 Conditionalrule …………………………….132 7.4.6 Iterationrule ………………………………133 7.4.7 Establishingloopinvariants ……………………….139 7.4.8 Arrayassignmentrule ………………………….142 7.4.9 Procedurecallrule ……………………………143 7.4.10 Otherrules ……………………………….146
7.5 MechanisingHoarelogic…………………………….146
7.6 Dijkstra’sweakestpreconditioncalculus……………………..147 7.6.1 Transformers………………………………147 7.6.2 Programproof ……………………………..147
7.7 Additionalreading ……………………………….148
8 Advanced Verification 149
8.1 PointersandAliasing………………………………149 8.2 Safe Programming with Pointers: Avoiding Unsafe Aliasing . . . . . . . . . . . . . . . 150
8.2.1 UnsafeAliasing……………………………..151 8.2.2 AvoidingUnsafeAliasinginSPARK …………………..151 8.2.3 Anti-AliasingAssumptionsinSPARK…………………..152 8.2.4 SPARKPointerChecks………………………….152 8.2.5 OtherProgrammingLanguages:Rust …………………..153
8.3 SeparationLogic ………………………………..153 8.3.1 PointersinC ………………………………153 8.3.2 SeparationLogic(forC)…………………………154 8.3.3 TheMeaningofSeparationLogicStatements……………….156 8.3.4 TheRulesofSeparationLogic………………………157 8.3.5 AnExampleProof ……………………………159
8.4 Security:InformationFlow……………………………161
9 Fault-tolerant design 162
9.1 Introductiontofault-tolerance ………………………….162
9.2 HardwareRedundancy ……………………………..165 9.2.1 Redundancy……………………………….165 9.2.2 Staticpairs ……………………………….166 9.2.3 Redundancyandvoting………………………….166 9.2.4 N-ModularRedundancy(NMR)……………………..170
9.3 SoftwareRedundancy………………………………171 9.3.1 N-VersionProgramming…………………………171 9.3.2 Recoveryblocks …………………………….173
9.4 ByzantineFailures ……………………………….176
9.5 InformationRedundancy…………………………….176 9.5.1 Duplication……………………………….176 9.5.2 Paritycoding………………………………177 9.5.3 Checksums……………………………….179
9.6 Faulttoleranceinpractice…………………………….179 9.6.1 AirbusA310–A380……………………………179 9.6.2 Boeing777……………………………….180 9.6.3 Boeing737MAXFlightControlRedesign ………………..180
9.7 Additionalreading ……………………………….180
Introduction to High Integrity Systems Engineering
1.1 Subject information Subject aims
The main aim of the subject is to explore the principles, techniques and tools used to analyse, design and implement high integrity systems. High integrity systems are systems that must operate with critical levels of security, safety, reliability, or performance. The engineering methods required to develop high integrity systems go well beyond the standards for less critical software.
Topics will include:
• high integrity system definition;
• programming languages for high-integrity systems; • safety and security analysis;
• modelling and analysis;
• fault tolerance; and
• proving program correctness.
Subject outcomes
On completion of this subject students should be able to:
• Demonstrate an understanding of the issues facing high integrity systems developers.
• Demonstrate the ability to analyse highly dependable systems and to synthesise requirements and operating parameters from their analysis.
• Demonstrate the ability to choose and make trade-offs between different software and systems architectures to achieve multiple objectives.
• Develop algorithms and code to meet high integrity requirements.
• Demonstrate the ability to assure high integrity systems.
Generic Skills
The subject is a technical subject. The aim is to explore the various approaches to building software with specific attributes into a system.
The subject will also aim to to develop a number of generic skills.
• We encourage independent research in order to develop your ability to learn independently, assess
what you learn, and apply what you learn.
• You will be developing experience at empirical software engineering, and the interpretation and assessment of quantitative and qualitative data.
• Finally, and perhaps most importantly, you will be encouraged to develop critical analysis skills that will complement and round what you have learnt so far in your degree.
Preconditions
The reason for giving preconditions is that the specify the knowledge assumed at the start of the subject and consequently the knowledge and skills upon which the subject builds. Preconditions also allow students from a Universities other than The University of Melbourne and who do not have the formal prerequisites listed above to judge whether or not they have the knowledge required for the subject. Specifically the subject assumes:
1. Knowledge and experience of software engineering processes and practices, the risks associated with software and system development, quality and quality assurance, software process, and soft- ware project management.
2. Knowledgeandexperienceofrequirementselicitationandanalysistechniques,requirementsmod- elling and specification, use-case modelling, and UML or similar modelling notations.
3. Knowledge and experience of software architectures, architectural styles and design patterns, de- sign with UML or similar graphical notation, developing code to meet architectural and detailed designs.
4. Knowledge and experience of discrete mathematics, including predicate logic and formal proof.
The LMS contains information about the subject staff, mode of delivery, and assessment criteria. It is the primary resource for the subject.
All announcements will be made via the LMS.
It also contains all assignment sheets, notes, lecture recordings, tutorial/workshop sheets and solutions.
http://www.lms.unimelb.edu.au/.
1.2 Introduction to high integrity systems What is a high integrity system?
High integrity systems a software controlled systems in which, in the event they fail, could result in harm to humans (including loss of life), harm on the environment, mass destruction of property, or harm to society in general.
There are four broad areas that are commonly considered as high integrity systems:
• Safety-critical systems: Systems whose failure may result in harm to humans or the environment. Examples include aerospace systems, medical devices, automotive systems, power systems, and railway systems.
• Security-critical systems: Systems whose failure may result in breach of security. Examples in- clude defence systems, government data stores.
• Mission-critical systems: Systems whose failure may result in the failure of some deliberative missions. Examples include navigation systems on autonomous aerospace vehicles, computer- aided dispatch systems (e.g. in emergency services), and command-and-control systems in armed forces.
• Business-critical systems: Systems whose failure may result in extreme financial loss to a business or businesses. Examples include stock exchange systems, trade platforms, and even accounting systems (e.g. in a bank).
What is high integrity systems engineering?
The high impact of failure of a high integrity system means that the software controlling the system must be highly dependable. The standard software engineering methods used for constructing good soft- ware systems typically do not lead to such dependability. As such, specialised methods for engineering software are required for high integrity systems.
Avizienis et al.’s work on dependability attributes help us to understand high integrity systems based on six key attributes, shown in Figure 1.1. For a single high integrity system, one or more of the above attributes will be of high importance.
How do we achieve high-integrity?
High integrity is achieved using a combination of:
• Rigorous engineering processes, such as strict configuration management, auditing, and review process. We will not introduce any new theory on these topics in this subject.
Availability
Readiness for use
Reliability
Continuity of Service
No catastrophic consequences for users or the environment
Dependability
Confidentiality
No unauthorised disclosure of confidential information
No improper system changes
Maintainability
The ability to undergo repairs and evolution.
Figure 1.1: Dependability model from “Avizienis, Laprie & Randell: Fundamental Concepts of Relia- bility”
• Specialised analysis and design methods, such as safety & hazard analysis and fault prediction methods. These will be covered in Part II of the subject.
• Specialised modelling and analysis methods/notations, such as mathematical logic and set theory. These will be covered in Part III of the subject.
• Fault tolerant design methods, such as redundancy, design diversity, and fault detection mecha- nisms. These will be covered in Part IV of the subject.
• Specialised assurance methods, such as model checking, proof, and model-based testing. These will be covered in Part V of the subject.
How do we achieve high-integrity?
Methods that are otherwise considered too expensive to apply to “standard” software systems become cost-effective in high integrity domains. This is because the cost of failure far outweighs the effort involved required to engineer a dependable product.
Of importance is that high dependability cannot be demonstrated by just running large set of tests. Al- though testing still plays an important role in high integrity systems, a really large set of tests is still usually only a fraction of all possible behaviour. As such, testing does not demonstrate dependability.
Perhaps the important lesson to learn from this introduction is:
“Program testing can be used to show the presence of bugs, but never to show their ab-
sence!” — Edsger W. Dijkstra [1].
1.3 Subject outline
Now that we have a better idea about high integrity systems engineering, we define the subject outline: Part I: Introduction to high integrity systems.
Safety- and security-critical systems.
Topics will be drawn from: safety engineering, and accident & hazard analysis for high- integrity systems; security analysis, cryptography.
Modelling and analysis.
Topics will be drawn from: discrete maths for software engineering, model-based specifica- tion and analysis, proof, and lightweight verification.
High integrity systems design.
Topics will be drawn from: reliability, fault detection, fault containment, fault tolerant design, and design by contract.
Assurance.
Topics will be drawn from: proving program correctness, programming languages for high integrity systems, safe-subset programming languages, programming tools for high integrity verification, and model-based testing.
Bibliography
[1] E. W. Dijkstra. Notes on structured programming. T. H. Report 70-WSK-03, Technological Univer- sity Eindhoven, Department of Mathematics, 1970.
Safety-critical and Security-critical systems engineering
2.1 An introduction to software safety
The trend in systems engineering is toward multi-disciplinary systems. Many of these systems are de- ployed outside of the standard desktop domain on which programming is typically taught. Such a trend has safety implications: if a piece of software is used to control a hardware system, it may have safety related issues.
For example, consider the following list of applications that have severe safety implications if they fail:
• Computer Aided Dispatch Systems (CAD);
• The A320 Airbus Electronic Flight Control System (EFCS);
• The Boeing 737 MAX 8 MCAS system
• Biomedical technology, such as pacemakers, and surgical robots; • Train protection systems;
• Space shuttle;
• Automated vehicle braking systems; and
• Chemical plant control systems.
Such systems have influence well beyond the desktop and an individual user. Software itself cannot harm people – it is merely an abstraction. However, software, when used to control hardware or other parts of a system (e.g. to make decisions or send orders on behalf of a human), can be a root cause of accidents and incidents.
The systems described above all rely on an integration of different technologies, and different engineering disciplines. What is perhaps new to most people in this subject is the reliance on computer systems and software to perform safety critical system functions.
The aim of the module on safety engineering is to develop an understanding of the safety engineering approach to developing safety-critical systems. Specifically:
• We will study accidents to get an idea of how they arise, how they are analysed, and what can be done to prevent or mitigate accidents.
• We will study safety engineering processes as the pathw
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com