Suchen und Finden
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
Alle Preise verstehen sich inklusive der gesetzlichen MwSt.