Track papers across labs, topics, and trends.
Search papers, labs, and topics across Lattice.
This paper explores techniques for writing concise and readable formal models in the LNT language, a modern process calculus. They demonstrate how features like imperative programming, symmetric sequential composition, and explicit loops can be leveraged for model simplification. Using the Algorand consensus protocol as a case study, they achieve a 3x reduction in lines of code while enhancing readability, and validate properties of the model using visual, equivalence, and model checking.
Shrinking your formal models by 3x isn't just about fewer lines of code; it's about making them understandable and verifiable.
LNT is a modern language for the formal description of concurrent systems. It generalizes traditional process calculi and overcomes their known limitations by incorporating features such as an imperative programming style with direct assignments to variables, symmetric sequential composition, and explicit loop operators. The present article examines how these features can be taken advantage of to obtain LNT models as concise and readable as possible. The study is illustrated with a running example, the consensus protocol of the Algorand blockchain, a formal model of which was recently developed at the University of Urbino. It is shown that, using well-chosen transformations, the number of lines of LNT code can be divided by three, while improving readability. Also, various properties of the formal model are expressed and verified using visual checking, equivalence checking, and model checking.