Seminars

View all Seminars  |  Download ICal for this event

Enhancing Statistical Model Checking via Abstraction Techniques and Learning

Series: CSA Colloquium

Speaker: Balaji Raman

Date/Time: Feb 02 11:00:00

Location: CSA Seminar Hall (Room No. 254, First Floor)

Abstract:
We will explore a cutting-edge methodology that significantly accelerates Statistical Model Checking (SMC) by leveraging abstraction and learning. This approach is particularly useful in scenarios where comprehensive system models are unavailable. By extracting abstract models from a set of system execution traces??obtained directly from the system's black-box implementation??we streamline the verification process. The core of the technique lies in projecting a large stochastic system onto a trace set pertinent to the property under scrutiny. These projections, which retain only the labels critical to the property, facilitate the learning of a succinct abstract model. This resultant probabilistic model acts as an effective abstraction of the actual system, upholding the property's satisfaction criteria.

Our empirical results underscore the efficacy of our method, which not only shrinks the size of the model in comparison to its detailed counterpart but also broadens the applicability of SMC. This is achieved by circumventing the timing challenges associated with generating detailed traces via simulation and by providing precise probability estimates for properties articulated in Linear Temporal Logic.

Speaker Bio:
Balaji Raman is a Principal Software Engineer in Test at The MathWorks Inc., a position he has held since 2022. With a specialization in stochastic performance analysis of embedded systems, he formerly served as an Associate Professor at the Indian Institute of Information Technology, Sri City (IIITS), Andhra Pradesh. Dr. Balaji Raman completed his Masters (by research) and Ph.D. at the National University of Singapore's School of Computing. His academic journey also includes a six-month stint as a visiting scholar at the Ecole Polytechnique Fédérale de Lausanne (EPFL) in Switzerland, and a postdoctoral term at the VERIMAG laboratory in France. Balaji has published in leading conferences and journals such as CODES+ISSS, the DAC, and the ACM Transactions on Embedded Computing Systems. He has won a Best Paper Award Nomination at CODES+ISSS 2006 and the President’s Graduate Fellowship Award in 2007/08.

Host Faculty: K. V. Raghavan