FMWS 2008
Formal Methods for Wireless Systems

Aims and scope

The FMWS workshop aims at bringing together researchers interested in formal methods for wireless systems. More specifically, it puts focus on theories for semantics, logics, and verification techniques for wireless systems. Wireless systems are rapidly increasing their success in real-world applications while formal methods for modelling, analysing, and verifying the systems are lacking behind. Recently however much attention has been carried out to model, analyse and verify Sensor Networks and, more generally, Ad Hoc Networks.

Submissions are solicited in all areas of semantics, logics, and verification techniques for concurrent wireless systems. The principal topics include (but are not limited to):

• Algebraic models
• Behavioural semantics
• Probabilistic models
• Broadcast communication
• Mobility
• Model checking
• Abstract interpretation
• Security
• Coordination languages
• Security issues
• Protocols

Workshop Proceedings

Program

• 08.50-09.00: Opening
• 09.00-10.00: Invited talk: A. Fehnker. Formal Methods in the Wireless Network Domain
• 10.00-10.30: Break
• 10.30-11.00: O. Hasan and S. Tahar. Probabilistic Analysis of Wireless Systems using Theorem Proving
• 11.00-11.30: A. Masri, T. Bourdeaud'huy and A. Toguyeni. Performance Analysis of IEEE 802.11b Wireless Networks with Object Oriented Petri Nets
• 11.30-12.00: H. Ehrig, K. Hoffmann, K. Gabriel, and J. Padberg Composition and Independence of High-Level Net Processes
• 12.00-12.30: A.N.M. Abdullah, B. Akbarpour, and S. Tahar. Error Analysis and Verification of an IEEE 802.11 OFDM Modem using Theorem Proving
• 12.30-14.00: Lunch
• 14.00-15.00: Invited talk: H. Hermanns. The Impact of Drifting Clocks on ZigBee's Energy Efficiency -- and why formal methods are pivotal to assess that
• 15.00-15.30: Jens Chr. Godskesen. A Calculus for Mobile Ad-hoc Networks with Static Location Binding (joint with EXPRESS)
• 15.30-16.00: Break
• 16.00-16.30: M. A. Azgomi and A. Khalili. Performance Evaluation of Sensor Medium Access Control Protocol Using Coloured Petri Nets.
• 16.30-16.45: J. Bendisposto, M. Jastram, M. Leuschel, C. Lochert, B. Scheuermann, I. Weigelt Validating Wireless Congestion Control and Reliability Protocols using ProB and Rodin
• 16.45-17.30: Plenary discussion.

Registration

Submissions

We solicit contributions to this workshop in the form of work-in-progress descriptions (up to 4 pages) or full papers (up to 12 pages) in any of the above fields or on related topics. Please use the ENTCS format and submit your contribution in PDF. The submission is done by email to fmws[at]itu.dk and works in two stages:

1. Register your paper with title, authors, abstract, etc. by June 12, 2008
   
2. Submit the final version until June 15, 2008

After the workshop, authors of full papers will be asked to prepare a final version of their paper in the ENTCS-style format to be published in the Electronic Notes in Theoretical Computer Science. A special issue in a journal is under consideration.

Important Dates

Invited Speaker

• Ansgar Fehnker, National ICT Australia, Formal Methods in the Wireless Network Domain (abstract)
• Holger Hermanns, Saarland University and INRIA, Grenoble, The Impact of Drifting Clocks on ZigBee's Energy Efficiency -- and why formal methods are pivotal to assess that (abstract)

Program Committee

• Jens Chr. Godskesen, IT University of Copenhagen, Denmark
• Andrew D. Gordon, Microsoft Research, Cambridge, UK
• Radha Jagadeesan, DePaul University, Chicago, USA
• Kim G. Larsen, Aalborg University, Denmark
• Massimo Merro, University of Verona, Italy
• Sebastian Nanz, Technical University of Denmark
• Catuscia Palamidessi, INRIA Futurs and LIX, France
• Davide Sangiorgi, University of Bologna, Italy
• Scott A. Smolka, Stony Brook, USA
• Luca Vigaṇ, University of Verona, Italy

Organizers

• Co-chair: Jens Chr. Godskesen, IT University of Copenhagen, Denmark
• Co-chair: Massimo Merro, University of Verona, Italy