Measurement of AC conductivity and dielectric properties of flexible conductive styrene–butadiene rubber‐carbon black composites

Flexible conductive polymer composites were prepared using styrene–butadiene rubber (SBR) as a matrix and conductive carbon black as filler. The filler loading was varied from 10 to 60 phr. The effect of frequency, filler loading, temperature, and applied pressure on the AC conductivity, permittivity, and loss factor of the composites was studied. The AC conductivity of low and high loaded composites was found to be frequency dependent and independent respectively. The permittivity and the loss factor were continuously decreasing with increasing frequency. The increase in filler loading increased the AC conductivity, dielectric constant, and loss factor of the composites. Increase in temperature imposed increase in conductivity and permittivity of the composites. With increasing applied pressure the properties showed exponential increase. The effect of time under a constant compressive stress was studied and dielectric relaxation times were evaluated. © 2007 Wiley Periodicals, Inc. J Appl Polym Sci 104: 986–995, 2007     

Requirement-oriented risk management for incremental software development

In incremental software development (ISD) functionalities are delivered incrementally and requirements keep on evolving across iterations. The requirements evolution involves the addition of new dependencies and conflicts among functional and non-functional requirements along with changes in priorities and dependency weights. This, in turn, demands refactoring the order of development of system components to minimize the impact of these changes. Neglecting the non-functional constraints in the software development process exposes it to risks that may accumulate across several iterations. In this research work, we propose a risk management framework for ISD processes that provides an estimate of risk exposure for the project when functional features are frozen while ignoring the associations with non-functional requirements. Our framework proposes suitable risk reduction strategies that work in tandem with the risk assessment module. We also provide a tool interface for our risk management framework.

     

Verification of evolving software via component substitutability analysis

This paper presents an automated and compositional procedure to solve the substitutability problem in the context of evolving software systems. Our solution contributes two techniques for checking correctness of software upgrades: (1) a technique based on simultaneous use of over-and under-approximations obtained via existential and universal abstractions; (2) a dynamic assume-guarantee reasoning algorithm—previously generated component assumptions are reused and altered on-the-fly to prove or disprove the global safety properties on the updated system. When upgrades are found to be non-substitutable, our solution generates constructive feedback to developers showing how to improve the components. The substitutability approach has been implemented and validated in the ComFoRT reasoning framework, and we report encouraging results on an industrial benchmark. This is an extended version of a paper, Dynamic Component Substitutability Analysis, published in the Proceedings of the Formal Methods 2005 Conference, Lecture Notes in Computer Science, vol. 3582, by the same authors. This research was sponsored by the National Science Foundation under grant nos. CNS-0411152, CCF-0429120, CCR-0121547, and CCR-0098072, the Semiconductor Research Corporation under grant no. TJ-1366, the US Army Research Office under grant no. DAAD19-01-1-0485, the Office of Naval Research under grant no. N00014-01-1-0796, the ICAST project and the Predictable Assembly from Certifiable Components (PACC) initiative at the Software Engineering Institute, Carnegie Mellon University. The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of any sponsoring institution, the US government or any other entity.     

Software model checking without source code

We present a framework, called air, for verifying safety properties of assembly language programs via software model checking. air extends the applicability of predicate abstraction and counterexample guided abstraction refinement to the automated verification of low-level software. By working at the assembly level, air allows verification of programs for which source code is unavailable—such as legacy and COTS software—and programs that use features—such as pointers, structures, and object-orientation—that are problematic for source-level software verification tools. In addition, air makes no assumptions about the underlying compiler technology. We have implemented a prototype of air and present encouraging results on several non-trivial examples.     

Automated Compositional Abstraction Refinement for Concurrent C Programs: A Two-Level Approach

The state space explosion problem in model checking remains the chief obstacle to the practical verification of real-world distributed systems. We attempt to address this problem in the context of verifying concurrent (message-passing) C programs against safety specifications. More specifically, we present a fully automated compositional framework which combines two orthogonal abstraction techniques (operating respectively on data and events) within a counterexample-guided abstraction refinement (CEGAR) scheme. In this way, our algorithm incrementally increases the granularity of the abstractions until the specification is either established or refuted. Our explicit use of compositionality delays the onset of state space explosion for as long as possible. To our knowledge, this is the first compositional use of CEGAR in the context of model checking concurrent C programs. We describe our approach in detail, and report on some very encouraging preliminary experimental results obtained with our tool MAGIC.     

A New Link Failure Resilient Priority Based Fair Mutual Exclusion Algorithm for Distributed Systems

This paper aims towards designing a new token-based mutual exclusion algorithm for distributed systems. In some of the earlier work, token based algorithms for mutual exclusion are proposed for the distributed environment assuming inverted tree topology. In a wireless setup, such a stable, hierarchical topology is quite unrealistic due to frequent link failures. The proposed token-based algorithm works for processes with assigned priorities on any directed graph topology with or without cycles. The proposed algorithm, in spite of considering priorities of processes, ensures liveness in terms of token requests from low priority processes. Moreover, the algorithm keeps control message traffic reasonably low. The simulation results exhibit the performance of the proposed algorithm under varied contexts besides presenting a comparative performance with other recent algorithms for mutual exclusion like FAPP (Fairness Algorithm for Priority Process).     

Exploring the simultaneous effect of nano‐silica reinforcement and electron‐beam irradiation on a model LDPE/EVA‐based TPE system

BACKGROUND: The technical properties of polyolefinic thermoplastic elastomer (TPE) systems can be modified significantly using fillers like nano‐silica. Controlled irradiation can potentially be an effective way of tailoring the technical properties of such nano‐silica‐filled TPE systems. RESULTS: The effect of controlled electron‐beam irradiation on the properties of a pristine silica nanoparticle‐filled model low‐density polyethylene/ethylene–(vinyl acetate) (LDPE/EVA) TPE system is explored in this paper. The morphology of such a filled system was investigated using scanning electron microscopy (SEM) and field‐emission SEM. The dispersion of silica particles was analysed using transmission electron microscopy which clearly indicates that at low loading a fine dispersion of silica occurs in the polymer matrix. Swelling studies and Fourier transform infrared analyses indicate the occurrence of a favourable EVA–silica interaction. On the whole, it is observed that electron‐beam irradiation induces a high degree of reinforcement in all the silica‐filled samples through interfacial crosslinking as well as controlled crosslinking in the two polymer phases. In a few samples the processing characteristics are remarkably preserved following concurrent nano‐silica reinforcement and irradiation, while the technical properties of TPE systems, including set, solvent swelling and mechanical properties, are improved. However, the improvement in properties is a strong function of sequence of addition of filler in the LDPE/EVA blends. CONCLUSION: The green technique studied can be potentially extended for the improvement of the technical properties of conventional TPE systems. Copyright © 2009 Society of Chemical Industry     

Concurrent software verification with states, events, and deadlocks

We present a framework for model checking concurrent software systems which incorporates both states and events. Contrary to other state/event approaches, our work also integrates two powerful verification techniques, counterexample-guided abstraction refinement and compositional reasoning. Our specification language is a state/event extension of linear temporal logic, and allows us to express many properties of software in a concise and intuitive manner. We show how standard automata-theoretic LTL model checking algorithms can be ported to our framework at no extra cost, enabling us to directly benefit from the large body of research on efficient LTL verification. We also present an algorithm to detect deadlocks in concurrent message-passing programs. Deadlock- freedom is not only an important and desirable property in its own right, but is also a prerequisite for the soundness of our model checking algorithm. Even though deadlock is inherently non-compositional and is not preserved by classical abstractions, our iterative algorithm employs both (non-standard) abstractions and compositional reasoning to alleviate the state-space explosion problem. The resulting framework differs in key respects from other instances of the counterexample-guided abstraction refinement paradigm found in the literature. We have implemented this work in the magic verification tool for concurrent C programs and performed tests on a broad set of benchmarks. Our experiments show that this new approach not only eases the writing of specifications, but also yields important gains both in space and in time during verification. In certain cases, we even encountered specifications that could not be verified using traditional pure event-based or state-based approaches, but became tractable within our state/event framework. We also recorded substantial reductions in time and memory consumption when performing deadlock-freedom checks with our new abstractions. Finally, we report two bugs (including a deadlock) in the source code of Micro-C/OS versions 2.0 and 2.7, which we discovered during our experiments. This research was sponsored by the National Science Foundation (NSF) under grants no. CCR-9803774 and CCR-0121547, the Office of Naval Research (ONR) and the Naval Research Laboratory (NRL) under contract no. N00014-01-1-0796, the Army Research Office (ARO) under contract no. DAAD19-01-1-0485, and was conducted as part of the Predictable Assembly from Certifiable Components (PACC) project at the Software Engineering Institute (SEI). This article combines and builds upon the papers (CCO⁺04) and (CCOS04). Received December 2004 Revised July 2005 Accepted July 2005 by Eerke A. Boiten, John Derrick, Graeme Smith and Ian Hayes     

Parallel Assignments in Software Model Checking

In this paper we investigate how formal software verification systems can be improved by utilising parallel assignment in weakest precondition computations.We begin with an introduction to modern software verification systems. Specifically, we review the method in which software abstractions are built using counterexample-guided abstraction refinement (CEGAR). The classical NP-complete parallel assignment problem is first posed, and then an additional restriction is added to create a special case in which the problem is tractable with an O(n²) algorithm. The parallel assignment problem is then discussed in the context of weakest precondition computations. In this special situation where statements can be assumed to execute truly concurrently, we show that any sequence of simple assignment statements without function calls can be transformed into an equivalent parallel assignment block.Results of compressing assignment statements into a parallel form with this algorithm are presented for a wide variety of software applications. The proposed algorithms were implemented in the ComFoRT reasoning framework [J. Ivers and N. Sharygina. Overview of ComFoRT: A model checking reasoning framework. Technical Report CMU/SEI-2004-TN-018, Carnegie Mellon Software Engineering Institute, 2004] and used to measure the improvement in the verification of real software systems. This improvement in time proved to be significant for many classes of software.     

MWCNT reinforced Polyamide-6,6 films: preparation,characterization and properties

Composite films of Polyamide-6,6 (PA66) and multi-walled carbon nanotubes (MWCNTs) were prepared by a combination of solution casting followed by compression molding techniques. Both unfunctionalized (u-MWCNTs) and functionalized nanotubes (f-MWCNTs) were used in this study. The functionalization involved direct solvent-free amination of MWCNTs with hexamethylenediamine. Thermogravimetric analysis was used to observe the changes in the nanotubes upon functionalization and morphological features of the resulting composite films were studied using scanning electron microscopy, transmission electron microscopy, and atomic force microscopy. The crystallinity changes by incorporation of the u-MWCNTs and f-MWCNTs in the PA66 matrix were studied by wide angle X-ray scattering and differential scanning calorimetry. The f-MWCNT/PA66 film showed an improvement of ∼43% in maximum tensile stress (MTS) and ∼32% in Young’s modulus over pristine PA66 film, while at a similar loading of 0.5 wt%, the f-MWCNT/PA66 film showed ∼15% increase in MTS and ∼16% increase in modulus over the u-MWCNT/PA66 film. Dynamic mechanical analysis indicated significant difference in the small-strain mechanical properties between the MWCNT-filled and unfilled PA66 at the very low MWNT loadings that were tested and supported the tensile results. The water absorption trend of the composite films showed dramatic improvement over the neat film.