E-Book, Englisch, 273 Seiten
Boca / Bowen / Siddiqi Formal Methods: State of the Art and New Directions
2010
ISBN: 978-1-84882-736-3
Verlag: Springer
Format: PDF
Kopierschutz: 1 - PDF Watermark
E-Book, Englisch, 273 Seiten
ISBN: 978-1-84882-736-3
Verlag: Springer
Format: PDF
Kopierschutz: 1 - PDF Watermark
Through fundamental contributions from leading researchers, this volume describes the use of formal modeling methods in the areas of requirements, design and validation. The self-contained chapters provide readers with rich background information and a diverse breadth of specialist material.
Autoren/Hrsg.
Weitere Infos & Material
1;Formal Methods: Stateof the Art and New Directions;1
1.1;1 Domain Engineering;21
1.1.1;1.1 Introduction;22
1.1.1.1;1.1.1 Application Cum Business Domains;22
1.1.1.2;1.1.2 Physics, Domains and Engineering;22
1.1.1.3;1.1.3 So, What is a Domain?;23
1.1.1.4;1.1.4 Relation to Previous Work;23
1.1.1.5;1.1.5 Structure of the Chapter;24
1.1.2;1.2 Domain Engineering: The Engineering Dogma;25
1.1.3;1.3 Entities, Functions, Events and Behaviours;26
1.1.3.1;1.3.1 Entities;26
1.1.3.1.1;Atomic Entities;26
1.1.3.1.2;Mereology;27
1.1.3.1.3;Composite Entities;27
1.1.3.1.4;States;28
1.1.3.2;1.3.2 Functions;28
1.1.3.2.1;Function Signatures;28
1.1.3.2.2;Function Descriptions;29
1.1.3.3;1.3.3 Events;29
1.1.3.4;1.3.4 Behaviours;30
1.1.3.5;1.3.5 Discussion;31
1.1.4;1.4 Domain Facets;31
1.1.4.1;1.4.1 Intrinsics;31
1.1.4.1.1;Conceptual vs. Actual Intrinsics;34
1.1.4.1.2;On Modelling Intrinsics;35
1.1.4.2;1.4.2 Support Technologies;35
1.1.4.2.1;On Modelling Support Technologies;37
1.1.4.3;1.4.3 Management and Organisation;37
1.1.4.3.1;Conceptual Analysis, First Part;39
1.1.4.3.2;Methodological Consequences;39
1.1.4.3.3;Conceptual Analysis, Second Part;39
1.1.4.3.4;On Modelling Management and Organisation;41
1.1.4.4;1.4.4 Rules and Regulations;41
1.1.4.4.1;A Meta-Characterisation of Rules and Regulations;42
1.1.4.4.2;On Modelling Rules and Regulations;44
1.1.4.5;1.4.5 Scripts and Licensing Languages;44
1.1.4.5.1;Licensing Languages;46
1.1.4.5.2;On Modelling Scripts;47
1.1.4.6;1.4.6 Human Behaviour;47
1.1.4.6.1;A Meta-Characterisation of Human Behaviour;48
1.1.4.6.2;On Modelling Human Behaviour;49
1.1.4.7;1.4.7 Completion;49
1.1.4.8;1.4.8 Integrating Formal Descriptions;50
1.1.5;1.5 On Modelling;50
1.1.5.1;1.5.1 Abstractions;50
1.1.5.2;1.5.2 Models;50
1.1.5.3;1.5.3 Real-World Constraints;50
1.1.5.4;1.5.4 Type Invariants;51
1.1.5.5;1.5.5 Vagaries of Domains;51
1.1.5.6;1.5.6 Monitoring of Domain States;51
1.1.5.7;1.5.7 Incompleteness and Inconsistency;51
1.1.6;1.6 From Domain Models to Requirements Models;52
1.1.6.1;1.6.1 Requirements Engineering Stages;52
1.1.6.2;1.6.2 Domain Requirements;53
1.1.6.3;1.6.3 Interface Requirements;53
1.1.6.4;1.6.4 Machine Requirements;53
1.1.6.5;1.6.5 Domain Descriptions vs. RequirementsPrescriptions;54
1.1.6.5.1;Indicative vs. Putative;54
1.1.6.5.2;Computability;54
1.1.6.5.3;Stability;54
1.1.6.5.4;Domain Engineering vs. Requirements Engineering Stages;55
1.1.7;1.7 Why Domain Engineering?;55
1.1.7.1;1.7.1 Two Reasons for Domain Engineering;55
1.1.7.2;1.7.2 An Engineering Reason for Domain Modelling;56
1.1.7.3;1.7.3 On a Science of Domains;56
1.1.7.3.1;Domain Theories;56
1.1.7.3.2;A Scientific Reason for Domain Modelling;57
1.1.8;1.8 Conclusion;57
1.1.8.1;1.8.1 Summary;57
1.1.8.2;1.8.2 Grand Challenges of Informatics;57
1.1.9;References;58
1.2;2 Program Verification and System Dependability;62
1.2.1;2.1 Introduction;62
1.2.1.1;2.1.1 The Grand Challenge Project;64
1.2.1.2;2.1.2 The Theme of This Paper;66
1.2.2;2.2 Dependability and the Problem World;67
1.2.2.1;2.2.1 Reasoning About the Machine and the World;67
1.2.2.2;2.2.2 Some Approaches to Reasoning About the World;69
1.2.2.3;2.2.3 Enhancing Reasoning for Dependability;72
1.2.3;2.3 Problem Decomposition;73
1.2.3.1;2.3.1 Complexity in Software-Intensive Systems;73
1.2.3.2;2.3.2 A Simplified Example;74
1.2.3.3;2.3.3 Subproblems and Further Decompositions;75
1.2.3.4;2.3.4 Subproblem Independence and Subproblem Composition;77
1.2.3.5;2.3.5 Normal Design;78
1.2.3.6;2.3.6 Verification and Subproblem Classes;80
1.2.3.7;2.3.7 Subproblem Concerns;82
1.2.3.8;2.3.8 Verifying Subproblem Concerns;83
1.2.3.9;2.3.9 Initialisation Concern;83
1.2.3.10;2.3.10 Completeness;84
1.2.4;2.4 Combining Subproblems;85
1.2.4.1;2.4.1 Composition Concerns;86
1.2.4.2;2.4.2 Switching;86
1.2.4.3;2.4.3 Requirement Conflict;87
1.2.4.4;2.4.4 Mode-Based Operation and Domain Properties;87
1.2.4.5;2.4.5 Relative Criticality;88
1.2.5;2.5 Non-Formal Problem Worlds;89
1.2.5.1;2.5.1 Alphabets and Designations;89
1.2.5.2;2.5.2 Formal Reasoning in Subproblem Composition;90
1.2.6;2.6 Concluding Reflections;92
1.2.7;References;95
1.3;3 The Abstract State Machines Method for High-Level System Design and Analysis;98
1.3.1;3.1 Introduction;98
1.3.2;3.2 Illustration by Examples;102
1.3.2.1;3.2.1 Sluice Gate Control;103
1.3.2.2;3.2.2 One-Way Traffic Light Control;106
1.3.2.3;3.2.3 Package Router Control;109
1.3.3;3.3 Enriching FSMs to ASMs;114
1.3.3.1;3.3.1 Generalising FSM States;114
1.3.3.2;3.3.2 Classification of Locations, Non-Determinism, Parallelism;117
1.3.4;3.4 ASM Ground Model Technique;118
1.3.5;3.5 ASM Refinement Concept for Detailed Design;120
1.3.6;3.6 Integration of Multiple Design and Analysis Methods;123
1.3.6.1;3.6.1 ASM-Characterisation of Event-B Machines;123
1.3.6.2;3.6.2 Integrating Special Purpose Methods;125
1.3.7;3.7 ASM Method Applications in a Nutshell;127
1.3.8;3.8 Concluding Remarks;128
1.3.9;References;129
1.4;4 Applications and Methodology of Z;136
1.4.1;4.1 Introduction;136
1.4.2;4.2 The Specification Logic Z – Overview I;137
1.4.2.1;4.2.1 Atomic State Specifications;137
1.4.2.2;4.2.2 Specification-Forming Operations;139
1.4.3;4.3 Case Studies and Methodology I;141
1.4.3.1;4.3.1 Conjunction;141
1.4.3.2;4.3.2 Methodology I;142
1.4.3.3;4.3.3 Primed and -Specifications;142
1.4.4;4.4 The Specification Logic Z – Overview II;142
1.4.4.1;4.4.1 Operation Specifications;143
1.4.4.2;4.4.2 Adding Inputs and Outputs;143
1.4.5;4.5 Case Studies and Methodology II;144
1.4.5.1;4.5.1 Guarded Specifications;144
1.4.5.2;4.5.2 Conditional Specifications;145
1.4.5.3;4.5.3 Methodology II;147
1.4.5.4;4.5.4 Varieties of Hiding;148
1.4.5.5;4.5.5 -Terms and -Schemas;148
1.4.6;4.6 Refinement;149
1.4.6.1;4.6.1 Refining Atomic Operations;150
1.4.6.2;4.6.2 Refining Guarded Specifications;150
1.4.6.3;4.6.3 Monotonicity in the Schema Calculus;150
1.4.6.4;4.6.4 Inequational Logic;151
1.4.7;4.7 Case Studies and Methodology III;152
1.4.7.1;4.7.1 Robust Operations;152
1.4.7.2;4.7.2 Methodology III;159
1.4.7.3;4.7.3 Promotion;160
1.4.8;4.8 Conclusions and Future Work;162
1.4.9;References;163
1.5;5 The Computer Ate My Vote;165
1.5.1;5.1 Introduction;166
1.5.2;5.2 The Challenge;167
1.5.3;5.3 Assumptions;168
1.5.4;5.4 Voting System Requirements;168
1.5.5;5.5 Sources of Assurance;170
1.5.5.1;5.5.1 Assurance of Privacy;171
1.5.6;5.6 Verifiable Voting Schemes;171
1.5.7;5.7 Related Work;171
1.5.8;5.8 Cryptographic Primitives;172
1.5.8.1;5.8.1 Public Key Cryptography;172
1.5.8.2;5.8.2 RSA Encryption;173
1.5.8.3;5.8.3 ElGamal Encryption;174
1.5.8.4;5.8.4 Paillier Encryption;175
1.5.8.5;5.8.5 Threshold Cryptography;176
1.5.8.6;5.8.6 Anonymising Mixes;176
1.5.8.7;5.8.7 Homomorphic Tabulation;177
1.5.8.8;5.8.8 Cut and Choose;177
1.5.8.9;5.8.9 Zero-Knowledge Proofs;178
1.5.8.10;5.8.10 Digital Signatures;179
1.5.9;5.9 Voter-Verifiable Schemes;179
1.5.10;5.10 Outline of Prêt à Voter;180
1.5.10.1;5.10.1 The Voting Ceremony;180
1.5.10.2;5.10.2 Vote Counting;182
1.5.11;5.11 Auditing the Election;184
1.5.11.1;5.11.1 Auditing the Ballot Generation Authority;184
1.5.11.2;5.11.2 Auditing the Mix Tellers;185
1.5.11.3;5.11.3 Auditing the Decryption Tellers;185
1.5.12;5.12 Threats and Trust Models;186
1.5.12.1;5.12.1 Leaky Ballot Creation Authority;186
1.5.12.2;5.12.2 Chain of Custody;187
1.5.12.3;5.12.3 Chain Voting;187
1.5.12.4;5.12.4 Side Channels and Subliminal Channels;188
1.5.12.5;5.12.5 Kleptographic Channels;188
1.5.12.6;5.12.6 Retention of the Candidate List;189
1.5.12.7;5.12.7 Collusion Between Mix Tellers and Auditors;189
1.5.12.8;5.12.8 Ballot Stuffing;189
1.5.13;5.13 Enhancements and Counter-Measures;190
1.5.13.1;5.13.1 On-Demand Generation of Prêt à Voter BallotForms;190
1.5.13.2;5.13.2 Distributed Generation of Paillier Encrypted Ballot Forms;191
1.5.14;5.14 Auditing ``On-Demand' Ballot Forms;193
1.5.15;5.15 Checking the Construction of the Ballot Forms;194
1.5.16;5.16 Re-Encryption/Tabulation Mixes;195
1.5.17;5.17 Handling Full Permutations and STV Style Elections;196
1.5.18;5.18 Conclusions;197
1.5.19;5.19 Future Work;199
1.5.20;References;200
1.6;6 Formal Methods for Biochemical Signalling Pathways;203
1.6.1;6.1 Introduction;203
1.6.2;6.2 Preliminaries;205
1.6.2.1;6.2.1 Continuous Time Markov Chains;205
1.6.2.2;6.2.2 Continuous Stochastic Logic;206
1.6.3;6.3 Modelling Biochemical Pathways;207
1.6.4;6.4 Modelling Pathways in PEPA;208
1.6.4.1;6.4.1 Syntax of the Language;208
1.6.4.2;6.4.2 Semantics of the Language;209
1.6.4.3;6.4.3 Reactions;210
1.6.4.4;6.4.4 Pathways and Discretisation;211
1.6.5;6.5 An Example: ERK Signalling Pathway;212
1.6.5.1;6.5.1 PEPA Model;214
1.6.5.2;6.5.2 Analysis;214
1.6.6;6.6 Modelling Pathways with Differential Equations;217
1.6.7;6.7 Modelling Pathways in PRISM;219
1.6.7.1;6.7.1 Reactions;219
1.6.7.2;6.7.2 Reaction Kinetics;221
1.6.7.2.1;Comparison of ODE and CTMC Models;222
1.6.7.3;6.7.3 Analysis of Example Pathway Using the PRISM Model Checker;223
1.6.7.3.1;Protein Stability;223
1.6.7.3.2;Activation Sequence;224
1.6.7.4;6.7.4 Further Properties;224
1.6.8;6.8 Discussion;225
1.6.8.1;6.8.1 Scalability;226
1.6.8.2;6.8.2 Relationship Between PEPA and PRISM;226
1.6.9;6.9 Related and Further Work;227
1.6.10;6.10 Conclusions;227
1.6.11;References;231
1.7;7 Separation Logic and Concurrency;234
1.7.1;7.1 Introduction;234
1.7.2;7.2 Background;235
1.7.2.1;7.2.1 Related Work;236
1.7.3;7.3 Hoare Logic;237
1.7.4;7.4 A Resource Logic for the Heap;238
1.7.5;7.5 A Resource Logic for Concurrency;242
1.7.5.1;7.5.1 Dealing with Semaphores;244
1.7.6;7.6 Permissions;249
1.7.7;7.7 A Resource Logic for Variables;250
1.7.7.1;7.7.1 Readers and Writers;251
1.7.8;7.8 Nonblocking Concurrency;255
1.7.8.1;7.8.1 What has Been Proved?;261
1.7.9;7.9 Conclusion;263
1.7.10;References;263
1.8;8 Programming Language Description Languages;266
1.8.1;8.1 Introduction;266
1.8.2;8.2 Programming Language Descriptions;268
1.8.2.1;8.2.1 Syntax;269
1.8.2.2;8.2.2 Semantics;270
1.8.3;8.3 Denotational Semantics;270
1.8.3.1;8.3.1 Towards a Formal Semantics;270
1.8.3.2;8.3.2 Mathematical Foundations;271
1.8.3.3;8.3.3 Development;272
1.8.3.4;8.3.4 Applications;273
1.8.4;8.4 Pragmatic Aspects;274
1.8.4.1;8.4.1 Scott–Strachey Semantics;274
1.8.4.2;8.4.2 Monadic Semantics;276
1.8.4.3;8.4.3 Action Semantics;277
1.8.4.4;8.4.4 Structural Operational Semantics;277
1.8.4.5;8.4.5 Modular SOS;279
1.8.5;8.5 Constructive Semantics;280
1.8.5.1;8.5.1 Modular Structure;280
1.8.5.2;8.5.2 Notation for Syntax;283
1.8.5.3;8.5.3 Tool Support;284
1.8.6;8.6 Future Directions: Semantics Online;285
1.8.7;8.7 Conclusion;287
1.8.8;References;287
