@InProceedings{	  hallerstede.ea:qualitative:2007,
  abstract	= {Event-B is a notation and method for discrete systems
		  modelling by refinement. We introduce a small but very
		  useful construction: qualitative probabilistic choice. It
		  extends the expressiveness of Event-B allowing us to prove
		  properties of systems that could not be formalised in
		  Event-B before. We demonstrate this by means of a small
		  example, part of a larger Event-B development that could
		  not be fully proved before. An important feature of the
		  introduced construction is that it does not complicate the
		  existing Event-B notation or method, and can be explained
		  without referring to the underlying more complicated
		  probabilistic theory. The necessary theory [18] itself is
		  briefly outlined in this article to justify the soundness
		  of the proof obligations given. We also give a short
		  account of alternative constructions that we explored, and
		  rejected.},
  author	= {Stefan Hallerstede and Thai Son Hoang},
  booktitle	= {Integrated Formal Methods, 6th International Conference,
		  IFM 2007},
  copyright	= 2007,
  copyrighturl	= {http://www.springer.com/rights?SGWID=0-122-0-0-0},
  isbn		= {978-3-540-73209-9},
  language	= {USenglish},
  note		= {This research was carried out as part of the EU research
		  project IST 511599 RODIN (Rigorous Open Development
		  Environment for Complex Systems)
		  http://rodin.cs.ncl.ac.uk.},
  pages		= {293--312},
  pdf		= {papers/2007/evtbprob.pdf},
  publisher	= {Springer},
  series	= {Lecture Notes in Computer Science},
  title		= {Qualitative Probabilistic Modelling in Event-B},
  url		= {http://dx.doi.org/10.1007/978-3-540-73210-5_16},
  volume	= 4591,
  year		= 2007,
  user		= {htson}
}