Blogs (1) >>
ICSE 2019
Sat 25 - Fri 31 May 2019 Montreal, QC, Canada
Mon 27 May 2019 08:50 - 09:15 at Sainte-Catherine - Session 1 Chair(s): Matteo Rossi

The notion of knowledge-based program introduced by Halpern and Fagin provides a useful formalism for designing, analysing, and optimising distributed systems. This paper formulates the two phase commit protocol as a knowledge-based program and then an iterative process of model checking and counter-example guided refinement is followed to find concrete implementations of the program for the case of perfect recall semantic in the Byzantine failures context with synchronous reliable communication. We model several different kinds of Byzantine failures and verify different strategies to fight and mitigate them. We address a number of questions that have not been considered in the prior literature, viz., under what circumstances a sender can know that its transmission has been successful, and under what circumstances an agent can know that the coordinator is cheating, and find concrete answers to these questions. The paper describes also a methodology based on temporal-epistemic model checking technology that can be followed to verify the shortest and longest execution time of a distributed protocol and the scenarios that lead to them.

Mon 27 May
Times are displayed in time zone: (GMT-04:00) Eastern Time (US & Canada) change

Formalise-2019-papers
08:40 - 10:30: FormaliSE 2019 - Session 1 at Sainte-Catherine
Chair(s): Matteo RossiPolitecnico di Milano
Formalise-2019-papers08:40 - 08:50
Day opening
Stefania GnesiIstituto di Scienza e Tecnologie dell'Informazione "Alessandro Faedo"
Formalise-2019-papers08:50 - 09:15
Full-paper
Omar BatainehNTU, Mark ReynoldsThe Univeristy of Western Australia
Formalise-2019-papers09:15 - 09:40
Full-paper
Beyazit YalcinkayaMiddle East Technical University, Ebru Aydin GolMiddle East Technical University
Formalise-2019-papers09:40 - 10:05
Full-paper
Ajay KrishnaInria Grenoble, France, Michel Le PallecNokia Bell Labs, Radu MateescuINRIA, Ludovic NoirieNokia Bell Labs, Gwen SalaünUniversity of Grenoble Alpes
Formalise-2019-papers10:05 - 10:30
Full-paper