February 23, 2010
School of Engineering, Amritapuri
 

The Chennai Mathematical Institute (CMI) is a premier research institute that attracts substantial funding from both industry and government agencies. Its research finds applications in the fields of mathematics, theoretical physics, and theoretical computer science.
 

Recently CMI organized a very exclusive workshop on “Automata, Concurrency and Timed Systems (ACTS)” during February 1-3, 2010. Amrita’s Jayaraj Poroor was invited to attend, together with nearly forty scientists from the best research organizations world-wide.
 

Indian educational institutions such as IISc Bangalore, IIT Bombay, IIT Delhi, IIT Kanpur and TIFR, Mumbai were represented as were some premier international universities such as INRIA Rocquencourt, Oxford, NUS, Singapore and LIAFA, Paris.
 

Automata (plural for automaton) are theoretical computers that are constructed in certain well-defined ways to perform limited tasks, and can be subjected to rigorous mathematical analysis. One may think of robots as an example.
 

Concurrency is the study of systems that perform many simultaneous interacting tasks. “One of themes of the workshop was the use of logic and automata for modeling and verifying distributed, open and timed systems,” explained Jayaraj,
 

Jayaraj has completed funded research projects in the areas of secure distributed systems and real-time embedded systems. He is currently working on formal specification and verification of these systems and as such, had much to gain from the workshop.
 

“The theoretical knowledge underlying such systems is important in order to construct safety-critical systems such as industrial control systems,” he stated. “The workshop covered some of the theoretical foundations for formal specification and verification methods as well.”
 

What are these formal specification and verification methods and why are these useful?
 

Formal specifications describe what a system should do using the language of mathematics and logic. Given such specifications, it is possible to do formal verification, i.e., prove that the system performs all its functions correctly.
 

Jayaraj’s doctoral research work is on formal specification and verification of embedded systems. He recently published a journal paper DoS Attacks on Real Time Media through Indirect Contention-In-Hosts in the Nov/Dec 2009 issue of IEEE Internet Computing.
 

“We are finding methods to build software without any vulnerabilities, so as to ensure hundred percent safety and security of embedded and internet-connected devices,” he shared, when asked about his doctoral research work.