Formal Methods: State of the Art and New Directions (eBook)

Formal Methods: Stateof the Art and New Directions 1
1 Domain Engineering 21
1.1 Introduction 22
1.1.1 Application Cum Business Domains 22
1.1.2 Physics, Domains and Engineering 22
1.1.3 So, What is a Domain? 23
1.1.4 Relation to Previous Work 23
1.1.5 Structure of the Chapter 24
1.2 Domain Engineering: The Engineering Dogma 25
1.3 Entities, Functions, Events and Behaviours 26
1.3.1 Entities 26
Atomic Entities 26
Mereology 27
Composite Entities 27
States 28
1.3.2 Functions 28
Function Signatures 28
Function Descriptions 29
1.3.3 Events 29
1.3.4 Behaviours 30
1.3.5 Discussion 31
1.4 Domain Facets 31
1.4.1 Intrinsics 31
Conceptual vs. Actual Intrinsics 34
On Modelling Intrinsics 35
1.4.2 Support Technologies 35
On Modelling Support Technologies 37
1.4.3 Management and Organisation 37
Conceptual Analysis, First Part 39
Methodological Consequences 39
Conceptual Analysis, Second Part 39
On Modelling Management and Organisation 41
1.4.4 Rules and Regulations 41
A Meta-Characterisation of Rules and Regulations 42
On Modelling Rules and Regulations 44
1.4.5 Scripts and Licensing Languages 44
Licensing Languages 46
On Modelling Scripts 47
1.4.6 Human Behaviour 47
A Meta-Characterisation of Human Behaviour 48
On Modelling Human Behaviour 49
1.4.7 Completion 49
1.4.8 Integrating Formal Descriptions 50
1.5 On Modelling 50
1.5.1 Abstractions 50
1.5.2 Models 50
1.5.3 Real-World Constraints 50
1.5.4 Type Invariants 51
1.5.5 Vagaries of Domains 51
1.5.6 Monitoring of Domain States 51
1.5.7 Incompleteness and Inconsistency 51
1.6 From Domain Models to Requirements Models 52
1.6.1 Requirements Engineering Stages 52
1.6.2 Domain Requirements 53
1.6.3 Interface Requirements 53
1.6.4 Machine Requirements 53
1.6.5 Domain Descriptions vs. RequirementsPrescriptions 54
Indicative vs. Putative 54
Computability 54
Stability 54
Domain Engineering vs. Requirements Engineering Stages 55
1.7 Why Domain Engineering? 55
1.7.1 Two Reasons for Domain Engineering 55
1.7.2 An Engineering Reason for Domain Modelling 56
1.7.3 On a Science of Domains 56
Domain Theories 56
A Scientific Reason for Domain Modelling 57
1.8 Conclusion 57
1.8.1 Summary 57
1.8.2 Grand Challenges of Informatics 57
References 58
2 Program Verification and System Dependability 62
2.1 Introduction 62
2.1.1 The Grand Challenge Project 64
2.1.2 The Theme of This Paper 66
2.2 Dependability and the Problem World 67
2.2.1 Reasoning About the Machine and the World 67
2.2.2 Some Approaches to Reasoning About the World 69
2.2.3 Enhancing Reasoning for Dependability 72
2.3 Problem Decomposition 73
2.3.1 Complexity in Software-Intensive Systems 73
2.3.2 A Simplified Example 74
2.3.3 Subproblems and Further Decompositions 75
2.3.4 Subproblem Independence and Subproblem Composition 77
2.3.5 Normal Design 78
2.3.6 Verification and Subproblem Classes 80
2.3.7 Subproblem Concerns 82
2.3.8 Verifying Subproblem Concerns 83
2.3.9 Initialisation Concern 83
2.3.10 Completeness 84
2.4 Combining Subproblems 85
2.4.1 Composition Concerns 86
2.4.2 Switching 86
2.4.3 Requirement Conflict 87
2.4.4 Mode-Based Operation and Domain Properties 87
2.4.5 Relative Criticality 88
2.5 Non-Formal Problem Worlds 89
2.5.1 Alphabets and Designations 89
2.5.2 Formal Reasoning in Subproblem Composition 90
2.6 Concluding Reflections 92
References 95
3 The Abstract State Machines Method for High-Level System Design and Analysis 98
3.1 Introduction 98
3.2 Illustration by Examples 102
3.2.1 Sluice Gate Control 103
3.2.2 One-Way Traffic Light Control 106
3.2.3 Package Router Control 109
3.3 Enriching FSMs to ASMs 114
3.3.1 Generalising FSM States 114
3.3.2 Classification of Locations, Non-Determinism, Parallelism 117
3.4 ASM Ground Model Technique 118
3.5 ASM Refinement Concept for Detailed Design 120
3.6 Integration of Multiple Design and Analysis Methods 123
3.6.1 ASM-Characterisation of Event-B Machines 123
3.6.2 Integrating Special Purpose Methods 125
3.7 ASM Method Applications in a Nutshell 127
3.8 Concluding Remarks 128
References 129
4 Applications and Methodology of Z 136
4.1 Introduction 136
4.2 The Specification Logic Z – Overview I 137
4.2.1 Atomic State Specifications 137
4.2.2 Specification-Forming Operations 139
4.3 Case Studies and Methodology I 141
4.3.1 Conjunction 141
4.3.2 Methodology I 142
4.3.3 Primed and -Specifications 142
4.4 The Specification Logic Z – Overview II 142
4.4.1 Operation Specifications 143
4.4.2 Adding Inputs and Outputs 143
4.5 Case Studies and Methodology II 144
4.5.1 Guarded Specifications 144
4.5.2 Conditional Specifications 145
4.5.3 Methodology II 147
4.5.4 Varieties of Hiding 148
4.5.5 -Terms and -Schemas 148
4.6 Refinement 149
4.6.1 Refining Atomic Operations 150
4.6.2 Refining Guarded Specifications 150
4.6.3 Monotonicity in the Schema Calculus 150
4.6.4 Inequational Logic 151
4.7 Case Studies and Methodology III 152
4.7.1 Robust Operations 152
4.7.2 Methodology III 159
4.7.3 Promotion 160
4.8 Conclusions and Future Work 162
References 163
5 The Computer Ate My Vote 165
5.1 Introduction 166
5.2 The Challenge 167
5.3 Assumptions 168
5.4 Voting System Requirements 168
5.5 Sources of Assurance 170
5.5.1 Assurance of Privacy 171
5.6 Verifiable Voting Schemes 171
5.7 Related Work 171
5.8 Cryptographic Primitives 172
5.8.1 Public Key Cryptography 172
5.8.2 RSA Encryption 173
5.8.3 ElGamal Encryption 174
5.8.4 Paillier Encryption 175
5.8.5 Threshold Cryptography 176
5.8.6 Anonymising Mixes 176
5.8.7 Homomorphic Tabulation 177
5.8.8 Cut and Choose 177
5.8.9 Zero-Knowledge Proofs 178
5.8.10 Digital Signatures 179
5.9 Voter-Verifiable Schemes 179
5.10 Outline of Prêt à Voter 180
5.10.1 The Voting Ceremony 180
5.10.2 Vote Counting 182
5.11 Auditing the Election 184
5.11.1 Auditing the Ballot Generation Authority 184
5.11.2 Auditing the Mix Tellers 185
5.11.3 Auditing the Decryption Tellers 185
5.12 Threats and Trust Models 186
5.12.1 Leaky Ballot Creation Authority 186
5.12.2 Chain of Custody 187
5.12.3 Chain Voting 187
5.12.4 Side Channels and Subliminal Channels 188
5.12.5 Kleptographic Channels 188
5.12.6 Retention of the Candidate List 189
5.12.7 Collusion Between Mix Tellers and Auditors 189
5.12.8 Ballot Stuffing 189
5.13 Enhancements and Counter-Measures 190
5.13.1 On-Demand Generation of Prêt à Voter BallotForms 190
5.13.2 Distributed Generation of Paillier Encrypted Ballot Forms 191
5.14 Auditing ``On-Demand' Ballot Forms 193
5.15 Checking the Construction of the Ballot Forms 194
5.16 Re-Encryption/Tabulation Mixes 195
5.17 Handling Full Permutations and STV Style Elections 196
5.18 Conclusions 197
5.19 Future Work 199
References 200
6 Formal Methods for Biochemical Signalling Pathways 203
6.1 Introduction 203
6.2 Preliminaries 205
6.2.1 Continuous Time Markov Chains 205
6.2.2 Continuous Stochastic Logic 206
6.3 Modelling Biochemical Pathways 207
6.4 Modelling Pathways in PEPA 208
6.4.1 Syntax of the Language 208
6.4.2 Semantics of the Language 209
6.4.3 Reactions 210
6.4.4 Pathways and Discretisation 211
6.5 An Example: ERK Signalling Pathway 212
6.5.1 PEPA Model 214
6.5.2 Analysis 214
6.6 Modelling Pathways with Differential Equations 217
6.7 Modelling Pathways in PRISM 219
6.7.1 Reactions 219
6.7.2 Reaction Kinetics 221
Comparison of ODE and CTMC Models 222
6.7.3 Analysis of Example Pathway Using the PRISM Model Checker 223
Protein Stability 223
Activation Sequence 224
6.7.4 Further Properties 224
6.8 Discussion 225
6.8.1 Scalability 226
6.8.2 Relationship Between PEPA and PRISM 226
6.9 Related and Further Work 227
6.10 Conclusions 227
References 231
7 Separation Logic and Concurrency 234
7.1 Introduction 234
7.2 Background 235
7.2.1 Related Work 236
7.3 Hoare Logic 237
7.4 A Resource Logic for the Heap 238
7.5 A Resource Logic for Concurrency 242
7.5.1 Dealing with Semaphores 244
7.6 Permissions 249
7.7 A Resource Logic for Variables 250
7.7.1 Readers and Writers 251
7.8 Nonblocking Concurrency 255
7.8.1 What has Been Proved? 261
7.9 Conclusion 263
References 263
8 Programming Language Description Languages 266
8.1 Introduction 266
8.2 Programming Language Descriptions 268
8.2.1 Syntax 269
8.2.2 Semantics 270
8.3 Denotational Semantics 270
8.3.1 Towards a Formal Semantics 270
8.3.2 Mathematical Foundations 271
8.3.3 Development 272
8.3.4 Applications 273
8.4 Pragmatic Aspects 274
8.4.1 Scott–Strachey Semantics 274
8.4.2 Monadic Semantics 276
8.4.3 Action Semantics 277
8.4.4 Structural Operational Semantics 277
8.4.5 Modular SOS 279
8.5 Constructive Semantics 280
8.5.1 Modular Structure 280
8.5.2 Notation for Syntax 283
8.5.3 Tool Support 284
8.6 Future Directions: Semantics Online 285
8.7 Conclusion 287
References 287