269 research outputs found
Behavioral automata composition for automatic topology independent verification of parameterized systems
No full textVerifying correctness properties of parameterized systems is a long-standing problem. The challenge lies in the lack of guarantee that the property is satisfied for all instances of the parameterized system. Existing work on addressing this challenge aims to reduce this problem to checking the properties on smaller systems with a bound on the parameter referred to as the cut-off. A property satisfied on the system with the cut-off ensures that it is satisfied for systems with any larger parameter. The major problem with these techniques is that they only work for certain classes of systems with specific communication topology such as ring topology, thus leaving other interesting classes of systems unverified. We contribute an automated technique for finding the cut-off of the parameterized system that works for systems defined with any topology. Given the specification and the topology of the system, our technique is able to automatically generate the cut-off specific to this system. We prove the soundness of our technique and demonstrate its effectiveness and practicality by applying it to several canonical examples where in some cases, our technique obtains smaller cut-off values than those presented in the existing literature.This is a manuscript of a proceeding published as Hanna, Youssef, Samik Basu, and Hridesh Rajan. "Behavioral automata composition for automatic topology independent verification of parameterized systems." In Proceedings of the the 7th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, pp. 325-334. ACM, 2009. 10.1145/1595696.1595758. Posted with permission.</p
Golok: Push-button Verification of Parameterized Systems
No full textParameterized systems verification is a long-standing problem, where the challenge is to verify that a property holds for all (infinite) instances of the parameterized system. Existing techniques aim to reduce this problem to checking the properties on smaller systems with a bound on the parameter referred to as the "cut-off" such that if the property holds for system instances of size cut-off that implies that it holds for larger system instances. In most existing techniques, human guidance is required to deduce the invariants for the system's behavior, which are then used to compute cut-off. In contrast, we present an fully automatic sound method (but necessarily incomplete) for generating the cut-off that works for synchronous parameterized systems with heterogeneous processes communicating via single-cast and/or broadcast. Our technique is independent of the system topology and the property to be verified. Given the specification and the topology of the system, our technique generates the system-specific cut-off. We have realized our technique in a tool, Golok, which shows that it can be automated. We present the results of running Golok on 15 parameterized systems where we obtain smaller cut-offs than those presented in the existing literature for 14 cases.Copyright © 2011, Youssef Hanna, David Samuelson, Samik Basu, Hridesh Rajan. All rights reserved.</p
Measuring the Impact of Influence on Individuals: Roadmap to Quantifying Attitude
No full textInfluence diffusion has been central to the study of propagation of
information in social networks, where influence is typically modeled as a
binary property of entities: influenced or not influenced. We introduce the
notion of attitude, which, as described in social psychology, is the degree by
which an entity is influenced by the information. We present an information
diffusion model that quantifies the degree of influence, i.e., attitude of
individuals, in a social network. With this model, we formulate and study
attitude maximization problem. We prove that the function for computing
attitude is monotonic and sub-modular, and the attitude maximization problem is
NP-Hard. We present a greedy algorithm for maximization with an approximation
guarantee of . Using the same model, we also introduce the notion of
"actionable" attitude with the aim to study the scenarios where attaining
individuals with high attitude is objectively more important than maximizing
the attitude of the entire network. We show that the function for computing
actionable attitude, unlike that for computing attitude, is non-submodular and
however is \emph{approximately submodular}. We present approximation algorithm
for maximizing actionable attitude in a network. We experimentally evaluated
our algorithms and study empirical properties of the attitude of nodes in
network such as spatial and value distribution of high attitude nodes.The following is a manuscript of an article published as Fu, Xiaoyun, Madhavan Padmanabhan, Raj Gaurav Kumar, Samik Basu, Shawn Dorius, and A. Pavan. "Measuring the Impact of Influence on Individuals: Roadmap to Quantifying Attitude." In 2020 IEEE/ACM International Conference on Advances in Social Networks Analysis and Mining (ASONAM), pp. 227-231. IEEE Computer Society, 2020. Copyright 2020 IEEE. Posted with permission
SMT-based formal verification of safety properties in neural networks
No full textThough they have been around since the late 1950s, artificial neural networks, or just neural networks (NNs), were not commonly considered as a potential (practical to implement) solution to real-world problems until the last couple of decades, when the dive into deep learning and big data started to produce significant benefits. In this case, a real-world problem refers to one that is common outside the realm of scientific exploration and research. Applications of NNs continue to increase in number and variety. As implementations of these ideas become more practical, their applications reach safety-critical systems (e.g., autonomous vehicles), making the verification of their conformity to safety requirements more critical. One of the benefits of a NN is that its internals need not be explicitly coded in order to produce reasonable outputs, demonstrating the ``learning'' aspect of machine learning. However, this creates new issues with verification. There are many established formal methods of software verification, such as bounded model checking and counterexample guided abstraction refinement (CEGAR), but these do not directly translate to NN verification. When the behavior of a machine cannot be stored explicitly as every possible path from input to output, it is not trivial to ensure it functions properly. Enumeration of NN behavior is prohibitively expensive because of the nature and number of computations it performs. This is largely because NNs typically cannot be exhaustively tested in a practical, efficient, computation-friendly way. Fortunately, in recent years, scholars have found ways to bring traditional verification techniques into the world of NNs. This paper reviews three such methods, compares them, and analyzes their potential for future use. These methods are: abstraction refinement due to Pulina and Tacchella, pure-SMT solving due to Huang et al., and Reluplex due to Katz et al.</p
A model checking approach for analyzing and identifying intervention policies to counter infection propagation over networks
No full textThe spread of infections (disease, ideas, fires, etc.) in a network (group of people, electronic network, forest, etc.) can be modeled by the evolution of states of nodes in a graph defined as a function of the states of the other nodes in the graph. Given an initial configuration of the graph with a subset of the nodes infected, a propagation function that specifies how the states of the nodes change over time, and a quarantine function that specifies the generation of regions centered on the infected nodes, from which the infection cannot spread; we identify and verify intervention policies designed to contain the propagation of the infection over the network. The approach can be used to determine an effective policy in such a scenario
Extending substitutability in composite services by allowing asynchronous communication
No full textWeb services are programs that are self-contained, self-describing, interoperable, platform-independent, and accessible over a network. These properties allow several Web services to be combined together to form a Web service composition. However, when a component service within a Web service composition becomes unavailable or unusable, it is necessary to identify a substitute service that can replace the failed component while preserving the original functionality of the composition. This is the problem of Web service substitution.
Most existing work that addresses this problem requires strict functional equivalence between the original component and its substitute. In contrast, Pathak et al. have shown in 2007 that it is sufficient for a substitute service to provide the same functionality with respect to the rest of the composition as the component it is replacing. Pathak et al. apply a technique called quotienting to determine the portion of the composition's overall functionality that is satisfied by the original component. The quotienting operation yields the property that must be satisfied by a substitute for that component.
While the use of quotienting allows more possible substitute services to be accepted, it is possible to relax the substitutability condition even further by considering asynchronous communication between component services within the Web service composition model. Our work accomplishes this task by providing a formal framework for representing asynchronous communication within a Web service composition. In our framework, the asynchronous communication is encapsulated in a buffer process, which stores each message until a component is ready to consume it. We prove the correctness of our solution, describe our implementation, and discuss some directions for future research.</p
Reconstructing material microstructures using deep learning
No full textComputational materials design integrates targeted materials process-structure and structure-property models in systems frameworks to meet specific engineering needs. The microstructure representations have to satisfy certain statistical parameters to be considered acceptable for further design processes. So, representation of microstructures have to be accurately identified to be considered for materials design. Current techniques have certain limitations in the characterization and reconstruction of these microstructures. The current state-of-the art model-based approaches do not have sufficient parameters that can serve as design variables. The high dimensional nature of this problem relies on dimension reduction that tends to lose important microstructural information. So, in the proposed project we want to design a methodology based on deep adversarial networks to produce these microstructures. The whole framework will be based on generative adversarial networks (GAN) and use them to learn the mapping between latent variables and microstructures. The idea is to train the GAN network to obtain microstructures that are statistically accurate and satisfy certain predefined properties.</p
Model checking techniques for vulnerability analysis of Web applications
No full textInjection Attacks exploit vulnerabilities of Web pages by inserting and executing malicious code (e.g., database query, Javascript functions) in unsuspecting users' computing environment or on a Web server. Such attacks compromise users' information and system resources, and pose a serious threat to personal and business assets. Methods have been devised to counter attacks and/or detect vulnerabilities to injection attacks in queries and/or in application source code. We define a classification for these query and application level methods and use this to classify a representative body of works that address injection attacks. We investigate and develop a framework where queries and vulnerable fragments of applications (written in query and application languages) are identified and analyzed offline (statically), and at runtime the vulnerable fragments are monitored to detect possible injection attacks. At its core, our framework leverages model checking, program analysis and concolic testing. Results show the effectiveness of our framework compared to the existing ones in three dimensions: first, our framework can detect vulnerabilities that go undetected when existing methods are used; second, our framework makes offline analysis of applications time efficient; and finally, our framework reduces the runtime monitoring overhead by focusing only on query conditions and application fragments that are vulnerable to injection attacks.</p
Spreading information in social networks containing adversarial users
No full textIn the modern day, social networks have become an integral part of how people communicate information and ideas. Consequently, leveraging the network to maximize information spread is a science that is applied in viral marketing, political propaganda. In social networks, an idea/information starts from a small group of users (known as seed users) and is propagated through the network via connections of the seed users. There are limitations on the number of seed users that can be convinced to adopt a certain idea. Therefore, the problem exists in finding a small set of users who can maximally spread an idea/information. This is known as the influence maximization problem. While this problem has been studied extensively, the presence of potential adversarial users and their impact on the information spread, has not been considered in existing solutions.In this thesis, we study the problem of spreading information to Target users while limiting the spread from reaching adversarial(Non Target) users. To this end, we consider a hard constraint - the objective is to maximize the information spread among the Target users while the number of Non-Target users to whom the information reaches is limited by a hard constraint. We design two algorithms - Natural Greedy and Multi Greedy with efficient RIS based implementations. We run our solutions on real world social networks to study the information spread. Finally, we evaluate the quality of our solutions on different models of diffusion and network settings.</p
Disrupting diffusion: Critical nodes in network
No full textWith the advent and proliferation of connected entities such as social, marketing, scientific and computer networks, it has become immensely important to understand and analyze the impact of one entity's influence on another in the network. In this context, our objective is to identify a set of entities, which when made ineffective (quarantined or protected) will maximally disrupt the spread of influence in the network. We formulate and study the problem of identifying nodes whose absence can maximally disrupt propagation of information in the independent cascade model of diffusion. We present the notion of impact and characterize critical nodes based on this notion. Informally, impact of a set of nodes quantifies the necessity of the nodes in the diffusion process. We prove that the impact is monotonic. Interestingly, unlike similar formulation of critical edges in the context of Linear Threshold diffusion model, impact is neither submodular nor supermodular. Hence, we develop heuristics that rely on greedy strategy and modular or submodular approximations of impact function. We empirically evaluate our heuristics by comparing the level of disruption achieved by identifying and removing critical nodes as opposed to that achieved by removing the most influential nodes.</p
- …
