Ansuman Banerjee

Soumik Guha Roy, Sumana Ghosh, Ansuman Banerjee et al.

Formal verification of designs with multiple properties has been a long-standing challenge for the verification research community. The task of coming up with an effective strategy that can efficiently cluster properties to be solved together has inspired a number of proposals, ranging from structural clustering based on the property cone of influence (COI) to leverage runtime design and verification statistics. In this paper, we present an attempt towards functional clustering of properties utilizing graph neural network (GNN) embeddings for creating effective property clusters. We propose a hybrid approach that can exploit neural functional representations of hardware circuits and runtime design statistics to speed up the performance of Bounded Model Checking (BMC) in the context of multi-property verification (MPV). Our method intelligently groups properties based on their functional embedding and design statistics, resulting in speedup in verification results. Experimental results on the HWMCC benchmarks show the efficacy of our proposal with respect to the state-of-the-art.

Moumita Das, Rajarshi Ray, Swarup Kumar Mohalik et al.

Neural networks are now extensively used in perception, prediction and control of autonomous systems. Their deployment in safety-critical systems brings forth the need for verification techniques for such networks. As an alternative to exhaustive and costly verification algorithms, lightweight falsification algorithms have been heavily used to search for an input to the system that produces an unsafe output, i.e., a counterexample to the safety of the system. In this work, we propose a falsification algorithm for neural networks that directs the search for a counterexample, guided by a safety property specification. Our algorithm uses a derivative-free sampling-based optimization method. We evaluate our algorithm on 45 trained neural network benchmarks of the ACAS Xu system against 10 safety properties. We show that our falsification procedure detects all the unsafe instances that other verification tools also report as unsafe. Moreover, in terms of performance, our falsification procedure identifies most of the unsafe instances faster, in comparison to the state-of-the-art verification tools for feed-forward neural networks such as NNENUM and Neurify and in many instances, by orders of magnitude.

Soumi Chattopadhyay, Ansuman Banerjee

The semantic information regulates the expressiveness of a web service. State-of-the-art approaches in web services research have used the semantics of a web service for different purposes, mainly for service discovery, composition, execution etc. In this paper, our main focus is on semantic driven Quality of Service (QoS) aware service composition. Most of the contemporary approaches on service composition have used the semantic information to combine the services appropriately to generate the composition solution. However, in this paper, our intention is to use the semantic information to expedite the service composition algorithm. Here, we present a service composition framework that uses semantic information of a web service to generate different clusters, where the services are semantically related within a cluster. Our final aim is to construct a composition solution using these clusters that can efficiently scale to large service spaces, while ensuring solution quality. Experimental results show the efficiency of our proposed method.

Soumi Chattopadhyay, Ansuman Banerjee

With an increasing number of web services, providing an end-to-end Quality of Service (QoS) guarantee in responding to user queries is becoming an important concern. Multiple QoS parameters (e.g., response time, latency, throughput, reliability, availability, success rate) are associated with a service, thereby, service composition with a large number of candidate services is a challenging multi-objective optimization problem. In this paper, we study the multi-constrained multi-objective QoS aware web service composition problem and propose three different approaches to solve the same, one optimal, based on Pareto front construction and two other based on heuristically traversing the solution space. We compare the performance of the heuristics against the optimal, and show the effectiveness of our proposals over other classical approaches for the same problem setting, with experiments on WSC-2009 and ICEBE-2005 datasets.

Soumi Chattopadhyay, Ansuman Banerjee

Efficient service composition in real time while providing necessary Quality of Service (QoS) guarantees has been a challenging research problem with ever growing complexity. Several heuristic based approaches with diverse proposals for taming the scale and complexity of web service composition, have been proposed in literature. In this paper, we present a new approach for efficient service composition based on abstraction refinement. Instead of considering individual services during composition, we propose several abstractions to form service groups and the composition is done on these abstract services. Abstraction reduces the search space significantly and thereby can be done reasonably fast. While this can expedite solution construction to a great extent, this also entails a possibility that it may fail to generate any solution satisfying the QoS constraints, though the individual services construct a valid solution. Hence, we propose to refine an abstraction to generate the composite solution with desired QoS values. A QoS satisfying solution, if one exists, can be constructed with multiple iterations of abstraction refinement. While in the worst case, this approach may end up exploring the complete composition graph constructed on individual services, on an average, the solution can be achieved on the abstract graph. The abstraction refinement techniques give a significant speed-up compared to the traditional composition techniques. Experimental results on real benchmarks show the efficiency of our proposed mechanism in terms of time and the number of services considered for composition.

Partha Pratim Ray, Ansuman Banerjee

Debugging denotes the process of detecting root causes of unexpected observable behaviors in programs, such as a program crash, an unexpected output value being produced or an assertion violation. Debugging of program errors is a difficult task and often takes a significant amount of time in the software development life cycle. In the context of embedded software, the probability of bugs is quite high. Due to requirements of low code size and less resource consumption, embedded softwares typically do away with a lot of sanity checks during development time. This leads to high chance of errors being uncovered in the production code at run time. In this paper we propose a methodology for debugging errors in BusyBox, a de-facto standard for Linux in embedded systems. Our methodology works on top of Valgrind, a popular memory error detector and Daikon, an invariant analyzer. We have experimented with two published errors in BusyBox and report our findings in this paper.

Partha Pratim Ray, Ansuman Banerjee, Banibrata Bag

Debugging is an unavoidable and most crucial aspect of software development life cycle. Especially when it comes the turn of embedded one. Due to the requirements of low code size and less resource consumption, the embedded softwares need to be upgraded all the time involving obvious change of code during development phase. This leads the huge risk of intrusion of bugs into the code at production time. In this paper we propose an approach of debugging embedded program in pseudo format, incorporating invariant analysis. Our methodology works on top of Daikon, a popular invariant analyzer. We have experimented with a simplified code snippet [1], used during debugging a reported error in BusyBox which is a de-facto standard for Linux in embedded systems.