We present our preliminary work towards a comprehensive solution for the hybrid (static + dynamic) verification of open distributed systems, using session types. We automate a solution for binary sessions where one endpoint is statically checked, and the other endpoint is dynamically checked by a monitor acting as an intermediary between typed and untyped components. We outline our theory, and illustrate a tool that automatically synthesises type-checked session monitors, based on the Scala language and its session programming library (lchannels).
CITATION STYLE
Bartolo Burlò, C., Francalanza, A., & Scalas, A. (2020). Towards a hybrid verification methodology for communication protocols (short paper). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 12136 LNCS, pp. 227–235). Springer. https://doi.org/10.1007/978-3-030-50086-3_13
Mendeley helps you to discover research relevant for your work.