@TechReport{	  it:2006-029,
  author	= {Lars-Henrik Eriksson},
  title		= {Use of Domain Theories in Applied Formal Methods},
  institution	= {Department of Information Technology, Uppsala University},
  department	= {Computing Science Division},
  year		= {2006},
  number	= {2006-029},
  month		= jun,
  abstract	= {A formal theory of an application domain can serve a key
		  role in formal specification and verification of systems
		  operating in that domain. This is particularly relevant
		  when working with families of similar systems intended to
		  control some kind of industrial process or function where
		  the control principles are general while the specifics of
		  the system depend on the particular installation the system
		  is intended to control. In such situations a domain theory
		  can facilitate writing generic specifications or
		  implementations for the entire family of systems which can
		  then be configured for each particular installation. Use of
		  concepts defined in the domain theory can also facilitate
		  communication with domain experts without knowledge in
		  formal methods.
		  
		  An example of such a family is railway signalling systems
		  which all implement the same general signalling principles
		  of ensuring safe train operation, while the exact function
		  of a particular signalling system depends on the railway
		  track layout under its control.
		  
		  We will give concrete examples from industrial practise in
		  the railway domain, showing how domain theories can help in
		  the formal verification process. The examples include
		  writing and validating formal specifications, formally
		  verifying implementations and analysing and communicating
		  the results of failed verifications.}
}