2017/2018 Edition

Lightweight formal methods for the development of high-assurance network systems

Lecturer: Prof. Assaf Kfoury (Boston University, USA).

About the lecturer | Course Summary

About the lecturer: Assaf Kfoury is currently Professor of Computer Science at Boston University. He completed his graduate studies at the Massachusetts Institute of Technology, with a Master's degree in Aeronautics and Astronautics, and a PhD in Computer Science. In addition to his current appointment at Boston University, he has taught at universities in the Middle East (University of Jordan and the American University of Beirut) and has held several visiting appointments at universities in the United States and Europe. For many years his research has been in foundational aspects of computer science, more specifically related to mathematical logic and formal methods. His most recent interests have focused on adapting formal methods to the specification, analysis and verification of network systems.

Course summary:
Many networking problems naturally lend themselves to graph-theoretic formulations that are far more complex than classical problems of graph theory. The modeling graphs are typically large, with hundreds or thousands or more nodes, often placed on a fluctuating grid, e.g., paths between nodes may fail or degrade or reappear, slowly or abruptly, and parameters regulating flow along paths may be conflicting requirements or defined differently at different nodes, locally or globally.

We propose a methodology for the specification and analysis of network systems which attempts to support such uneven features in the large graphs modeling them. The proposed methodology would allow for a compositional (as opposed to whole-system) analysis which is additionally incremental (distributed in time) and modular (distributed in space). Towards this goal, we leverage concepts and techniques rooted in mathematical logic and the formal methods of computer science. Our methodology calls for the definition of a strongly-typed domain-specific language to specify network configurations and the properties we wish to enforce. We pay special attention to keeping these concepts and techniques lightweight. i.e., making the parts available to users "friendly" (relatively simple and easy to use) while the more complicated parts remain hidden "under the roof". We illustrate these ideas with a particular application: the specification and analysis of vehicular traffic networks.

The preceding is only one approach out of many that promote the use of formal methods for a rigorous analysis of properties of network systems. Such approaches have been introduced by many researchers, including ourselves, in recent years. We conclude with a brief overview of other formal methodologies we have developed, or refined from others, towards such a goal.

Slides and Exercises

Attention: daedline extended !