Download The Development of a Probabilistic B-Method and a Supporting Toolkit PDF

TitleThe Development of a Probabilistic B-Method and a Supporting Toolkit
LanguageEnglish
File Size1.2 MB
Total Pages228
Table of Contents
                            Abstract
Statement
Acknowledgements
Dedication
List of Figures
List of Tables
Introduction
	Motivation
	Aims and Contributions
	Dissertation Organisation
Background and Related Work
	The Generalised Substitution Language
		Meaning of Programs
		GSL Syntax
		GSL Semantics
	The Abstract Machine Notation
	Software Development Using the B-Method
	The B-Toolkit
	The Probabilistic GSL
		Elementary Probability Theory
		pGSL Syntax
		pGSL Semantics
	Summary
Almost-certain Termination
	Demonic- versus Probabilistic Termination
	A Probabilistic Zero-one Law for Loops
		Almost-Certain Correctness
		The Failure of the Standard Variant Rule
		Termination of Probabilistic Loops
		Probabilistic Variant Rule for Probabilistic Loops
		Proof Obligation Rules for Probabilistic Loops
	Implementation of Almost-certain Termination
	Modifying the B-Toolkit for qB
		System Library for Abstract Probabilistic Choice
		Syntactic and Other Changes
	Applications of qB
		Root Contention of the FireWire Protocol
		Rabin's Choice Coordination
	Conclusions and Related Work
Probabilistic Machines
	Numerical Reasoning
	Probabilistic Invariant
		A Simple Library in B
		Adding Probabilistic Properties to the Library
		The EXPECTATIONS Clause
		What Do Probabilistic Invariants Guarantee?
		A Probabilistic Invariant for the Library
		Proof Obligations
		Proving the Obligations
		What the Invariant Means
	Mixing Demonic and Probabilistic Choice
		StockTake Breaks the Probabilistic Invariant
		Interaction of Demonic and Probabilistic Choice
		Capturing Long-term Behaviour
	Actual Changes to the B-Toolkit
	Conclusions and Future Work
Probabilistic Specification Substitutions
	Refinement of Probabilistic Systems
	Probabilistic Specification Substitutions
		Standard Specification Substitutions
		Probabilistic Specification Substitutions
	The Fundamental Theorem
		The Standard Fundamental Theorem
		The Probabilistic Fundamental Theorem
	Probabilistic Loops
		Proof Obligations for Standard Loops
		Proof Obligations for Probabilistic Loops
	Actual Changes to the B-Toolkit
	The Min-Cut Algorithm
		Informal Description of the Min-Cut Algorithm
		Probabilistic Amplification
		Formal Development of Contraction
		Formal Development of Probabilistic Amplification
	Terminating Substitutions
	Specification Frame
	Conclusions and Future Work
Multiple Expectation Systems
	Completeness of Probabilistic SpecificationSubstitutions
	Multiple Probabilistic Specification Substitutions
		Definition
		Examples
	The Multiple Probabilistic Fundamental Theorem
		The Fundamental Theorem
		Examples
	Case Study: The Duelling Cowboys
		Example of Two Duelling Cowboys
		Example of Three Duelling Cowboys
	Proposed Changes to the B-Toolkit
	Conclusions and Future Work
Conclusions and Future Work
	Conclusions
	Future work
		Tool Support for Multiple Expectation Systems
		Completeness of Probabilistic Specification Substitutions
		Composition of Probabilistic Machines
		Data Refinement
		Probabilistic Event-B
		Animation
Root Contention
	Specification: FirewireResolve.mch
	Implementation: FirewireResolveI.imp
Choice Coordination Algorithm
	Finite Bag: FBag.mch
	Context of Finite Bag: FBag_ctx.mch
	Specification: Rabin.mch
	Refinement: RabinR.ref
	Implementation: RabinRI.imp
	Support the Implementation: RabinState.mch
Special Fundamental Theorem
Duelling Cowboys Case Study
	Two Duelling Cowboys
	Three Duelling Cowboys
List of publications
                        
Document Text Contents
Page 1

School of Computer Science and Engineering
The University of New South Wales

The Development of a Probabilistic B-Method
and a Supporting Toolkit

Thai Son Hoang
Bachelor of Engineering, UNSW

A thesis submitted for the degree of
Doctor of Philosophy

July 2005

Supervisor: Associate Professor Ken Robinson
Co-supervisor: Professor Carroll Morgan

Page 114

100 CHAPTER 5. PROBABILISTIC SPECIFICATION SUBSTITUTIONS

• Hoare triples [26]:
{P} S {Q} (5.2)

where P and Q are predicates over the program state, and S is program

statement. If P holds in the initial state and S is executed and terminates,

then Q is guaranteed to hold in the final state.

• Dijkstra’s weakest precondition [16]:

P ⇒ wp(S ,Q) (5.3)

where P and Q are predicates over the program state, and S is program state-

ment. The notation wp(S ,Q) denotes the weakest precondition of S with

respect to Q , i.e. the weakest precondition, under which Q is guaranteed to

be established after the execution of S .

• Morgan’s specification statements [43]:

v : [P ,Q ] (5.4)

where v is the frame, a sub-vector of the program variables whose values

may change. P and Q are predicates describing the initial state and the final

state, respectively.

Other notations also include Morris’s prescription [52] and Back’s pre/post-

condition specifications [8].

In B (or more precisely, GSL) [4], the same idea is presented with a different

syntax:

P | v : Q , (5.5)

with the meaning that the substitution will establish Q under the precondition P ,

and change only the variables in v . In this form, we will always assume that P

and Q are predicates over x and over x0, v , respectively. The variables v (sub-set

of the variables x ) are those that can be possibly changed by the substitution. The

variables x0 are distinct from x and represent their original values. Intuitively, the

meaning of (5.5) can be derived from the semantics presented Fig. 2.2 on page 12

by decomposing it into an unbounded choice substitution and a precondition sub-

stitution as follows:

P | @ v ′ ·
([

x0, v : = x , v
′]Q =⇒ v : = v ′) .

Page 115

5.2. PROBABILISTIC SPECIFICATION SUBSTITUTIONS 101

In fact, this is the form, into which the B-Toolkit will de-sugar the substitution.

It is common in B to get the meaning of a substitution by decomposing it in this

way. When this is done, it can be easily seen that specification (5.5) is just another

presentation of those illustrated in (5.2), (5.3) or (5.4).

5.2.2 Probabilistic Specification Substitutions

The ideas in Sec. 5.2.1 can be generalised to the probabilistic context. In this

section, we propose a probabilistic version of (5.5) which has the same role in the

probabilistic world as the original standard specification substitution does in the

standard world.

Recall that in the expectation logic, we write

A V [S ]B , (5.6)

to mean that the execution of S guarantees to establish that the expected value of

B over the final state distributions is bounded below by the value of A in the initial

state. By analogy with the connection between Dijkstra-style wp-specification and

Morgan’s specification statement, we propose a probabilistic specification substi-

tution written as in the standard case, that is

A | v : B , (5.7)

except that now A is an expectation defined over the program variables, B is an

expectation that may additionally refer to x0 and v . The variables v (which we also

call the frame of the substitution) are a sub-vector of program variables x , which

the substitution “constrains” to change only those variables (we will address what

we mean by constrains later).

As the first example, if we want to specify a coin that comes up heads with

probability at least one-half, then in the style of (5.6) we would write

1
2

V [Flip]〈coin = Head〉 ,

where coin is the state variable with possible values {Head ,Tail}. In the style of
(5.7), we would instead specify the substitution Flip as

1
2
| coin : 〈coin = Head〉 , (5.8)

Page 227

Appendix E

List of publications

Below are list of publications related to this dissertation.

1. Thai Son Hoang, Zhendong Jin, Ken Robinson, Annabelle McIver, and Car-

roll Morgan. Probabilistic Invariants for Probabilistic Machines. In D. Bert,

J. P. Bowen, S. King, and M. Waldén, editors, ZB2003: Formal Specification

and Development in Z and B, Proceedings of the 3rd International Confer-

ence of B and Z Users, volume 2651 of Lecture Notes in Computer Science,

Turku, Finland, June 2003. Springer Verlag.

2. Thai Son Hoang, Zhendong Jin, Ken Robinson, Annabelle McIver, and Car-

roll Morgan. Development via Refinement in Probabilistic B — Foundation

and Case Study. In Helen Treharne, Steve King, Martin Henson, and Steve

Schneider, editors, ZB2005: Formal Specification and Development in Z and

B, Proceedings of the 4th International Conference of B and Z Users, vol-

ume 3455 of Lecture Notes in Computer Science, pages 355–373, Guildford,

United Kingdom, April 2005. Springer Verlag.

3. Annabelle McIver, Carroll Morgan, and Thai Son Hoang. Probabilistic ter-

mination in B. In D. Bert, J. P. Bowen, S. King, and M. Waldén, editors,

ZB2003: Formal Specification and Development in Z and B, Proceedings of

the 3rd International Conference of B and Z Users, volume 2651 of Lecture

Notes in Computer Science, Turku, Finland, June 2003. Springer Verlag.

4. Carroll Morgan, Thai Son Hoang, and Jean-Raymond Abrial. The Challenge

of Probabilistic Event-B. In Helen Treharne, Steve King, Martin Henson, and

213

Page 228

214 APPENDIX E. LIST OF PUBLICATIONS

Steve Schneider, editors, ZB2005: Formal Specification and Development

in Z and B, Proceedings of the 4th International Conference of B and Z

Users, volume 3455 of Lecture Notes in Computer Science, pages 162–171,

Guildford, United Kingdom, April 2005. Springer Verlag.

5. Steve Schneider, Thai Son Hoang, Ken Robinson, and Helen Treharne. Tank

Monitoring: A Case Study in pAMN. Technical report, Royal Holloway, the

University of London, 2003. CSD-TR-03-17.

6. Steve Schneider, Thai Son Hoang, Ken Robinson, and Helen Treharne. Tank

Monitoring: A pAMN Case Study. Electronic Notes in Theoretical Com-

puter Science (ENTCS), April 2005.

7. Steve Schneider, Thai Son Hoang, Ken Robinson, and Helen Treharne. Tank

Monitoring: A pAMN Case Study. Formal Aspects of Computing, 2005.

Submitted for publication.

Similer Documents