We have made extremely significant contributions in several safety critical domains. Some of these contributions are extremely significant for the nation.
Formal Methods for Verification of Railway Signaling and Interlocking
- Formal Methods for Validation and Test Point Prioritization in Railway Signaling Logic. Shiladitya Ghosh, Arindam Das, Nirvik Basak, Pallab Dasgupta, Alok Katiyar. Accepted for publication in IEEE Transactions on Intelligent Transportation Systems, 2016.
Formal Methods for Verification of Automotive Control
- Automated Planning as an Early Verification Tool for Distributed Control. Kamalesh Ghosh, Pallab Dasgupta and S. Ramesh. Journal of Automated Reasoning, 54 (1), 31-68, 2015.
Formal Methods for Verification of Real Time Operating Systems
Formal Methods for Verification of Access Control in Corporate Networks
- Policy Based Security Analysis in Enterprise Networks - A Formal Approach. Padmalochan Bera, S K Ghosh and Pallab Dasgupta. IEEE Transactions on Network and Service Management, 7(4), Dec 2010, 231-243
We have been engaged by Indian Railways to examine the best practices in development of the yard-specific logic for electronic interlocking equipment being deployed for signaling and interlocking. Our prescription for formally validating the signaling logic as per the recommendation of the EN50128 railway safety standards was articulated by Dr Dasgupta jointly with Mr Mahesh Mangal of the Railway Board in a book chapter, Formal Assurance of Signaling Safety: A Railways Perspective in Handbook of Research on Emerging Innovations in Rail Transportation Engineering. We developed the notion of perfect invariants for proving signaling logic to be strongly safe. Based on this new technology, the group developed the first of its kind formal tool flow for formally proving the safety of signaling logic for Indian Railways. The tool has been successfully used in several stations in India. We have also helped IRISET (Signaling Institute of Indian Railways) in preparing a blueprint for a Center for Safety Critical Software.
In a very significant project called AUTOSAFE with the Technical University of Munich, Germany and two industry partners, we have jointly developed a platform for formal analysis of timing closure for control loop executions in software controlled automotive features. In a previous collaboration with General Motors, we introduced a theory that relates AI planning techniques with the verification of possible scenarios revealing contradictions between the formal specifications of multiple features. We shall lead the verification tasks in an Uchhatar Aviskar Yojana (UAY) project where Tata Motors and IIT Kharagpur have joined hands to develop their first plug-in hybrid electric vehicle.
We have been engaged by Hindustan Aeronautics Ltd for formally verifying an indigenous real time operating system for avionic applications. The safety of this RTOS is of extremely high significance to the nation.
We have developed formal methods for proving the security of access control configurations in enterprise networks. We have developed formal methods that can be used to prove the non-existence of hidden access paths that may be enabled by composition of multiple network services.