Conclusions

We have surveyed the formal methods used for communications services both in industry and academia and noted that only a few of the formal methods have attracted the attention of industry. We have listed and discussed major industrial concerns for the applicability of formal methods. These points, if seriously taken into consideration by the formal methods community, are likely to trigger some changes in the focus of formal methods research. While some peculiarities of communication services like concurrency and real-time are today well-understood, others, like the heterogeneous environment in which communication services run and the complexity of industrial communication services are addressed only inadequately. We believe that the integration of the impressive results of formal methods research of the past into industry will not be helped by yet another formal mechanism to model concurrency but by providing satisfying answers to the industrial concerns discussed in this paper. We have briefly reported on a collaborative project of the Swiss Federal Institute of Technology, Swisscom, Alcatel and Thomson. The proposed approach to service validation is currently being integrated into an industrial development platform. We have discussed how our approach addresses the industrial concerns.