Generalising Feature Interactions in Email
Muffy CALDER and Alice MILLER
Department of Computing Science
University of Glasgow
Glasgow, Scotland.
muffy,alice@dcs.gla.ac.uk
Abstract. We report on a property-based approach to feature interaction
analysis for a client-server email system. The model is based upon Hall’s
email model presented at FIW’00, but the implementation is at a lower
level of abstraction, employing non-determinism and asynchronous communication;
it is a challenge to avoid deadlock and race conditions. Our analysis differs
in two ways: interaction analysis is fully automated, based on model-checking
the entire state-space, and the results are scalable, that is they generalise
to email systems consisting of any number of email clients.
Abstraction techniques are used to prove the general results. The key idea
is to model-check a system consisting of a constant number (m)of client
processes, in
parallel with a mailer process and an “abstract” process which represents
the product of any number of other (possibly featured) client processes. We
give a lower bound for the value of m.
All of the models – for any specified set of client processes and selected
features – are generated automatically using Perl scripts.