ECE ILLINOIS Facebook ECE ILLINOIS on Twitter ECE ILLINOIS Alumni and Friends on LinkedIn ECE ILLINOIS Instagram

Contact Info

Brad Petersen
Director of
Communications
2052 ECE Building
306 N. Wright Street
Urbana, IL 61801
Phone: (217) 244-6376
bradp@illinois.edu

Contact Info

Meg Dickinson
Communications Specialist
2016 ECE Building
306 N. Wright Street
Urbana, IL 61801
Phone: (217) 300-6664
megd@illinois.edu

Subscribe to ECE ILLINOIS News

Recent News

New ECE class gives students an in-depth look at the engineering process

New ECE class gives students an in-depth look at the engineering process

Starting this semester, ECE ILLINOIS will offer students an opportunity to study the engineering design process and possibly get a head start on their Senior Design projects with a new class called ECE 398, Special Topics in ECE.

Mitra and Johnson win award for research on machine models

 Subscribe to ECE ILLINOIS News

By Elise King, Coordinated Science Lab
October 10, 2012

  • ECE Assistant Professor Sayan Mitra and his graduate student Taylor Johnson recently won the best paper award at the IFIP International Conference on Formal Techniques for Distributed Systems.
  • Their paper examined the problem of verifying invariant properties of infinite collections of interacting state machine models called rectangular hybrid automata (RHA).
  • Their software, Passel, automatically checks invariants of RHA networks modeling an air traffic control landing protocol.

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.

Editor's note: media inquiries should be directed to Brad Petersen, Director of Communications, at bradp@illinois.edu or (217) 244-6376.

 Subscribe to ECE ILLINOIS News