Formal Methods: State of the Art and New Directions

Formal Methods: Stateof the Art and New Directions

1 Domain Engineering

1.1 Introduction

1.1.1 Application Cum Business Domains

1.1.2 Physics, Domains and Engineering

1.1.3 So, What is a Domain?

1.1.4 Relation to Previous Work

1.1.5 Structure of the Chapter

1.2 Domain Engineering: The Engineering Dogma

1.3 Entities, Functions, Events and Behaviours

1.3.1 Entities

Atomic Entities

Mereology

Composite Entities

States

1.3.2 Functions

Function Signatures

Function Descriptions

1.3.3 Events

1.3.4 Behaviours

1.3.5 Discussion

1.4 Domain Facets

1.4.1 Intrinsics

Conceptual vs. Actual Intrinsics

On Modelling Intrinsics

1.4.2 Support Technologies

On Modelling Support Technologies

1.4.3 Management and Organisation

Conceptual Analysis, First Part

Methodological Consequences

Conceptual Analysis, Second Part

On Modelling Management and Organisation

1.4.4 Rules and Regulations

A Meta-Characterisation of Rules and Regulations

On Modelling Rules and Regulations

1.4.5 Scripts and Licensing Languages

Licensing Languages

On Modelling Scripts

1.4.6 Human Behaviour

A Meta-Characterisation of Human Behaviour

On Modelling Human Behaviour

1.4.7 Completion

1.4.8 Integrating Formal Descriptions

1.5 On Modelling

1.5.1 Abstractions

1.5.2 Models

1.5.3 Real-World Constraints

1.5.4 Type Invariants

1.5.5 Vagaries of Domains

1.5.6 Monitoring of Domain States

1.5.7 Incompleteness and Inconsistency

1.6 From Domain Models to Requirements Models

1.6.1 Requirements Engineering Stages

1.6.2 Domain Requirements

1.6.3 Interface Requirements

1.6.4 Machine Requirements

1.6.5 Domain Descriptions vs. RequirementsPrescriptions

Indicative vs. Putative

Computability

Stability

Domain Engineering vs. Requirements Engineering Stages

1.7 Why Domain Engineering?

1.7.1 Two Reasons for Domain Engineering

1.7.2 An Engineering Reason for Domain Modelling

1.7.3 On a Science of Domains

Domain Theories

A Scientific Reason for Domain Modelling

1.8 Conclusion

1.8.1 Summary

1.8.2 Grand Challenges of Informatics

References

2 Program Verification and System Dependability

2.1 Introduction

2.1.1 The Grand Challenge Project

2.1.2 The Theme of This Paper

2.2 Dependability and the Problem World

2.2.1 Reasoning About the Machine and the World

2.2.2 Some Approaches to Reasoning About the World

2.2.3 Enhancing Reasoning for Dependability

2.3 Problem Decomposition

2.3.1 Complexity in Software-Intensive Systems

2.3.2 A Simplified Example

2.3.3 Subproblems and Further Decompositions

2.3.4 Subproblem Independence and Subproblem Composition

2.3.5 Normal Design

2.3.6 Verification and Subproblem Classes

2.3.7 Subproblem Concerns

2.3.8 Verifying Subproblem Concerns

2.3.9 Initialisation Concern

2.3.10 Completeness

2.4 Combining Subproblems

2.4.1 Composition Concerns

2.4.2 Switching

2.4.3 Requirement Conflict

2.4.4 Mode-Based Operation and Domain Properties

2.4.5 Relative Criticality

2.5 Non-Formal Problem Worlds

2.5.1 Alphabets and Designations

2.5.2 Formal Reasoning in Subproblem Composition

2.6 Concluding Reflections

References

3 The Abstract State Machines Method for High-Level System Design and Analysis

3.1 Introduction

3.2 Illustration by Examples

3.2.1 Sluice Gate Control

3.2.2 One-Way Traffic Light Control

3.2.3 Package Router Control

3.3 Enriching FSMs to ASMs

3.3.1 Generalising FSM States

3.3.2 Classification of Locations, Non-Determinism, Parallelism

3.4 ASM Ground Model Technique

3.5 ASM Refinement Concept for Detailed Design

3.6 Integration of Multiple Design and Analysis Methods

3.6.1 ASM-Characterisation of Event-B Machines

3.6.2 Integrating Special Purpose Methods

3.7 ASM Method Applications in a Nutshell

3.8 Concluding Remarks

References

4 Applications and Methodology of Z

4.1 Introduction

4.2 The Specification Logic Z – Overview I

4.2.1 Atomic State Specifications

4.2.2 Specification-Forming Operations

4.3 Case Studies and Methodology I

4.3.1 Conjunction

4.3.2 Methodology I

4.3.3 Primed and -Specifications

4.4 The Specification Logic Z – Overview II

4.4.1 Operation Specifications

4.4.2 Adding Inputs and Outputs

4.5 Case Studies and Methodology II

4.5.1 Guarded Specifications

4.5.2 Conditional Specifications

4.5.3 Methodology II

4.5.4 Varieties of Hiding

4.5.5 -Terms and -Schemas

4.6 Refinement

4.6.1 Refining Atomic Operations

4.6.2 Refining Guarded Specifications

4.6.3 Monotonicity in the Schema Calculus

4.6.4 Inequational Logic

4.7 Case Studies and Methodology III

4.7.1 Robust Operations

4.7.2 Methodology III

4.7.3 Promotion

4.8 Conclusions and Future Work

References

5 The Computer Ate My Vote

5.1 Introduction

5.2 The Challenge

5.3 Assumptions

5.4 Voting System Requirements

5.5 Sources of Assurance

5.5.1 Assurance of Privacy

5.6 Verifiable Voting Schemes

5.7 Related Work

5.8 Cryptographic Primitives

5.8.1 Public Key Cryptography

5.8.2 RSA Encryption

5.8.3 ElGamal Encryption

5.8.4 Paillier Encryption

5.8.5 Threshold Cryptography

5.8.6 Anonymising Mixes

5.8.7 Homomorphic Tabulation

5.8.8 Cut and Choose

5.8.9 Zero-Knowledge Proofs

5.8.10 Digital Signatures

5.9 Voter-Verifiable Schemes

5.10 Outline of Prêt à Voter

5.10.1 The Voting Ceremony

5.10.2 Vote Counting

5.11 Auditing the Election

5.11.1 Auditing the Ballot Generation Authority

5.11.2 Auditing the Mix Tellers

5.11.3 Auditing the Decryption Tellers

5.12 Threats and Trust Models

5.12.1 Leaky Ballot Creation Authority

5.12.2 Chain of Custody

5.12.3 Chain Voting

5.12.4 Side Channels and Subliminal Channels

5.12.5 Kleptographic Channels

5.12.6 Retention of the Candidate List

5.12.7 Collusion Between Mix Tellers and Auditors

5.12.8 Ballot Stuffing

5.13 Enhancements and Counter-Measures

5.13.1 On-Demand Generation of Prêt à Voter BallotForms

5.13.2 Distributed Generation of Paillier Encrypted Ballot Forms

5.14 Auditing ``On-Demand' Ballot Forms

5.15 Checking the Construction of the Ballot Forms

5.16 Re-Encryption/Tabulation Mixes

5.17 Handling Full Permutations and STV Style Elections

5.18 Conclusions

5.19 Future Work

References

6 Formal Methods for Biochemical Signalling Pathways

6.1 Introduction

6.2 Preliminaries

6.2.1 Continuous Time Markov Chains

6.2.2 Continuous Stochastic Logic

6.3 Modelling Biochemical Pathways

6.4 Modelling Pathways in PEPA

6.4.1 Syntax of the Language

6.4.2 Semantics of the Language

6.4.3 Reactions

6.4.4 Pathways and Discretisation

6.5 An Example: ERK Signalling Pathway

6.5.1 PEPA Model

6.5.2 Analysis

6.6 Modelling Pathways with Differential Equations

6.7 Modelling Pathways in PRISM

6.7.1 Reactions

6.7.2 Reaction Kinetics

Comparison of ODE and CTMC Models

6.7.3 Analysis of Example Pathway Using the PRISM Model Checker

Protein Stability

Activation Sequence

6.7.4 Further Properties

6.8 Discussion

6.8.1 Scalability

6.8.2 Relationship Between PEPA and PRISM

6.9 Related and Further Work

6.10 Conclusions

References

7 Separation Logic and Concurrency

7.1 Introduction

7.2 Background

7.2.1 Related Work

7.3 Hoare Logic

7.4 A Resource Logic for the Heap

7.5 A Resource Logic for Concurrency

7.5.1 Dealing with Semaphores

7.6 Permissions

7.7 A Resource Logic for Variables

7.7.1 Readers and Writers

7.8 Nonblocking Concurrency

7.8.1 What has Been Proved?

7.9 Conclusion

References

8 Programming Language Description Languages

8.1 Introduction

8.2 Programming Language Descriptions

8.2.1 Syntax

8.2.2 Semantics

8.3 Denotational Semantics

8.3.1 Towards a Formal Semantics

8.3.2 Mathematical Foundations

8.3.3 Development

8.3.4 Applications

8.4 Pragmatic Aspects

8.4.1 Scott–Strachey Semantics

8.4.2 Monadic Semantics

8.4.3 Action Semantics

8.4.4 Structural Operational Semantics

8.4.5 Modular SOS

8.5 Constructive Semantics

8.5.1 Modular Structure

8.5.2 Notation for Syntax

8.5.3 Tool Support

8.6 Future Directions: Semantics Online

8.7 Conclusion

References