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.
After the proper presentation, I will discuss some ideas about how to use parameterised model checking such as regular model checking for solving verification and validation problems involving domain theories.
- L.-H. Eriksson, Use of Domain Theories in Applied Formal Methods, Technical Report 2006-029, Uppsala University, Dept. of Information Technology, 2006.
- L.-H. Eriksson, Verification and Generation of Geographical Data Using a Domain Theory (extended abstract), TRain Workshop at the 3rd IEEE International Conference on Software Engineering and Formal Methods (SEFM'05), 2005.