SuCCeSS

Security, Adaptability and time in Communication Centric Software Systems

Projet cooperative PICS 07313 France - Pays Bas

This project concerns formal approaches to reliable distributed communication-centric software systems (CCSSs). To detect costly software bugs we study validation techniques based on BEHAVIORAL TYPES (BTs), which enforce safety and liveness properties of structured communications (e.g. protocol conformance).

Ensuring correct and reliable CCSSs is hard because they are:

1. Heterogeneous: they mix known, checkable components (e.g. Web services) with interacting artifacts available only as black-boxes (e.g. legacy systems).
2. Dynamic: components’ behavior may change in reaction to, e.g. errors or varying requirements.

To tackle this challenge, we will develop programming models and validation techniques based on BTs, building on our previous works. As a distinctive feature, we will comprehensively address the subtle interplay of protocol conformance properties with security, adaptability, and timing requirements. Connections with actual programming languages will also be pursued.