Dynamic Data-Driven Formal Progress Envelopes for Distributed Algorithms

This work presents formal progress envelopes applied to flight systems for distinctly classifying a system’s state space into regions where a formal proof of progress for a distributed algorithm holds or does not hold. It also presents an approach for runtime integration of formal methods in the dynamic data-driven applications systems (DDDAS) architecture using parameterized proofs. Finally, it showcases the development of reusable parameterized proof libraries for high-level statistical and stochastic reasoning in the Athena proof assistant and demonstrates their use with a progress proof for the Paxos distributed consensus protocol.

Reference

Paul S., Kopsaftopoulos F.P., Patterson S., Varela C., "Dynamic Data-Driven Formal Progress Envelopes for Distributed Algorithms ,"

International Conference on Dynamic Data Driven Application Systems (pp. 245-252), Springer, Cham, November 2020.

View Publication

Bibtex

@inproceedings{paul2020dynamic,
  title={Dynamic data-driven formal progress envelopes for distributed algorithms},
  author={Paul, Saswata and Kopsaftopoulos, Fotis and Patterson, Stacy and Varela, Carlos A},
  booktitle={International Conference on Dynamic Data Driven Application Systems},
  pages={245--252},
  year={2020},
  organization={Springer}
}