Mitra and Johnson win award for research on machine models

10/10/2012 Elise King, Coordinated Science Lab

ECE Assistant Professor Sayan Mitra and ECE graduate student Taylor Johnson recently won the best paper award at the IFIP International Conference on Formal Techniques for Distributed Systems.

Written by Elise King, Coordinated Science Lab

Sayan Mitra
Sayan Mitra

ECE Assistant Professor Sayan Mitra and ECE graduate student Taylor Johnson recently won the best paper award at the IFIP International Conference on Formal Techniques for Distributed Systems (FMOODS/FORTE ’12). The paper was chosen out of three collocated conferences in Stockholm under the umbrella of the International Federated Conference on Distributed Computing Techniques.

Taylor Johnson
Taylor Johnson

In the winning paper, titled, “A Small Model Theorem for Rectangular Hybrid Automata Networks,” Mitra, a researcher in the Coordinated Science Lab (CSL), and Johnson looked at the problem of verifying invariant properties of infinite collections of interacting state machine models called rectangular hybrid automata (RHA). RHA networks can model, for example, timing-based network protocols, traffic control protocols and robotic swarms.

Mitra and Johnson show that the problem of verifying an invariant for an arbitrarily large collection of automata can be reduced to checking a finite collection, for some restricted classes of RHAs. The size of the finite collection that has to be checked depends on the syntactic structure of the automaton and the invariant. This "small model" result relies on demonstrating that any violation of the invariant by a larger system can be mimicked by a violation in a smaller system.

The paper also discusses the implementation of a software prototype, called Passel, which Mitra and Johnson created for automatically checking invariants of RHA networks modeling an air traffic control landing protocol, as well as several distributed mutual exclusion algorithms. Moving forward, Mitra and Johnson plan to continue to develop Passel and investigate methods for finding invariant properties for RHA networks.

Mitra and Johnson are in the Reliable and High Performance Computing group at CSL.


Share this story

This story was published October 10, 2012.