I am a researcher working in the field of Formal Verification. My research interest lies in verifying complex hardware and software systems.
I have been working on various model checking techniques to verify and improve the functionality and performance of stochastic systems.
I am also interested in verification of security properties of cyber-physical systems and verifying software systems using program analysis.
Previously, I was a Postdoctoral Researcher working in the
Distributed, Embedded and Intelligent Systems (DEIS)
group at the Department of Computer Science, Aalborg University, Aalborg.
I completed my Masters and Ph.D. from the department of
Computer Science and Engineering at Indian Institute of Technology
Hyderabad under the guidance of Dr. M. V. Panduranga Rao.
My PhD thesis was titled "Functional and Performance Improvements for Probabilistic Model Checking".
Postdoctoral Researcher
DEIS, Aalborg University, Denmark
Ph.D in Computer Science & Engineering
Indian Institute of Technology Hyderabad
Thesis: Functional and Performance Improvements for Probabilistic Model Checking
M. Tech in Computer Science & Engineering
Indian Institute of Technology Hyderabad
CGPA : 9.05
B.Tech in Computer Science & Engineering
Shri Mata Vaishno Devi University, Katra
CGPA : 9.38
Hosted by Dr. Axel Legay, Inria, Rennes, France.
Hosted by Dr. Rodney Van Meter, Keio University, SFC, Japan.
Many security-related properties—such as non-interference—cannot be captured by traditional trace-based specification formalisms such as LTL. The reason is that they relate the events of two (or more) traces of the system, and LTL can only reason on one execution at a time. A number of hyper-property extensions of LTL have been proposed in the past few years, and case studies showing their ability to express interesting properties have also been shown. However, there has been less attention to hyper-properties for quantitative (timed) systems as well as very little work on developing a practically useful tool. Instead existing work focused on using ad-hoc implementations.
In this paper we present a probabilistic hyper-property logic HPSTL for stochastic hybrid and timed systems and we show how to integrate the logic into existing statistical model checking tools. To show the feasibility of our approach we integrate the technique into a prototype implementation inside UPPAAL SMC and apply it to the analysis of three side-channel attack examples. To our knowledge this is the first full implementation of a hyper logic inside a fully-fledged modelling environment.
In this work, we discuss a numerical model checking algorithm for analyzing incompletely specified models of stochastic systems, specifically, Discrete Time Markov Chains (DTMC). Models of a system could be incompletely specified for several reasons. For example, they could still be under development or, there could be some doubt about the correctness of some components. We restrict ourselves to cases where incompleteness can be captured by expanding the logic of atomic propositions to a three valued logic that includes an unknown truth value. We seek to answer meaningful model checking queries even in such circumstances.
The approach we adopt in this paper is to develop the model checking algorithm from first principles. We develop a tool based on the algorithm and compare the performance of this approach with the indirect approach of invoking a binary model checker.
In this work, we discuss a numerical model checking algorithm for analyzing incompletely specified models of stochastic systems, specifically, Discrete Time Markov Chains (DTMC). Models of a system could be incompletely specified for several reasons. For example, they could still be under development or, there could be some doubt about the correctness of some components. We restrict ourselves to cases where incompleteness can be captured by expanding the logic of atomic propositions to a three valued logic that includes an unknown truth value. We seek to answer meaningful model checking queries even in such circumstances.
The approach we adopt in this paper is to develop the model checking algorithm from first principles. We develop a tool based on the algorithm and compare the performance of this approach with the indirect approach of invoking a binary model checker.
We study a variant of the folklore Cops and Robbers (also known as pursuit evasion) problem on graphs. In this variant, there are different specializations of cops and a minimum number of each specialization are necessary to catch a robber. To the best of our knowledge, this variant has not been investigated so far. We believe that this problem will find relevance in several domains like biological systems and epidemic response strategies. We seek to compare the ease of catching robbers executing random walks on various graphs, especially complex networks. We use Statistical Model Checking for the analysis. In this initial work, we report experiments that yield interesting results. For example, we show empirically that it is easier to catch robbers on the Barabási-Albert model, than on the Erdős-Rényi model.
We study incomplete stochastic systems that are missing some parts of their design, or are lacking information about some components. It is interesting to get early analysis results of the requirements of these systems, in order to adequately refine their design. In previous works, models for incomplete systems are analysed using model checking techniques for three-valued temporal logics. In this paper, we propose statistical model checking algorithms for these logics. We illustrate our approach on a case-study of a network system that is refined after the analysis of early designs.
It is crucial for accurate model checking that the model be a complete and faithful representation of the system. Unfortunately, this is not always possible, mainly because of two reasons: (i) the model is still under development and (ii) the correctness of implementation of some modules is not established. In such circumstances, is it still possible to get correct answers for some model checking queries? This paper is a step towards answering this question. We formulate this problem for the Discrete Time Markov Chains (DTMC) modeling formalism and the Probabilistic Computation Tree Logic (PCTL) query language. We then propose a simple solution by modifying DTMC and PCTL to accommodate three valued logic. The technique builds on existing model checking algorithms and tools, obviating the need for new ones to account for three valued logic. One of the most useful and popular techniques for modeling complex systems is through discrete event simulation. Discrete event simulators are essentially code in some programming language. We show an application of our approach on a piece of code that contains a module of unknown correctness. A preliminary version of this paper appears in the proceedings of Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques (ISoLA 2016), LNCS 9952, Springer. Keywords: Probabilistic models, Probabilistic Model checking Three-valued Logic, Discrete Time Markov Chain, Probabilistic Computation Tree Logic.
It is crucial for accurate model checking that the model be a complete and faithful representation of the system. Unfortunately, this is not always possible, mainly because of two reasons: (i) the model is still under development and (ii) the correctness of implementation of some modules is not established. In such circumstances, is it still possible to get correct answers for some model checking queries?
This paper is a step towards answering this question. We formulate the problem for the Discrete Time Markov Chains (DTMC) modeling formalism and the Probabilistic Computation Tree Logic (PCTL) query language. We then propose a simple solution by modifying DTMC and PCTL to accommodate three valued logic. The technique builds on existing model checking algorithms and tools, obviating the need for new ones to account for three valued logic. Finally, we provide an experimental demonstration of our approach.
Simulations and test bed experiments have been the mainstay for analysis of routing algorithms in computer networks. In isolation, these approaches are not amenable to more detailed analyses. For example, it is difficult to check protocols against intricate properties specified as statements in a formal logic. It is therefore natural to turn to the rich and mature theory of model checking for the purpose. Indeed, model checking tools and techniques have been applied in the past for analyzing a variety of deterministic and stochastic systems.
In this paper, we use statistical model checking to analyze properties and performance of opportunistic network routing protocols. While previous works have largely focused on model checking specific protocols (e.g. in wireless mesh networks), we explore the possibility of generic analysis by linking a statistical model checker with a discrete event simulator for opportunistic networks. This allows statistical model checking of several opportunistic network protocols. We illustrate the approach through a comparison of various protocols against several model checking queries