Model-checking bisimulation-based information flow properties for infinite state sstems

Bisimulation-based information flow properties were introduced by Focardi and Gorrieri [1] as a way of specifying security properties for transition system models. These properties were shown to be decidable for finite-state systems. In this paper, we study the problem of verifying these properties for some well-known classes of infinite state systems. We show that all the properties are undecidable for each of these classes of systems.

A fuzzy logic based dynamic wave model inversion algorithm for canal regulation

A fuzzy logic based centralized control algorithm for irrigation canals is presented. Purpose of the algorithm is to control downstream discharge and water level of pools in the canal, by adjusting discharge release from the upstream end and gates settings. The algorithm is based on the dynamic wave model (Saint-Venant equations) inversion in space, wherein the momentum equation is replaced by a fuzzy rule based model, while retaining the continuity equation in its complete form. The fuzzy rule based model is developed on fuzzification of a new mathematical model for wave velocity, the derivational details of which are given. The advantages of the fuzzy control algorithm, over other conventional control algorithms, are described. It is transparent and intuitive, and no linearizations of the governing equations are involved. Timing of the algorithm and method of computation are explained. It is shown that the tuning is easy and the computations are straightforward. The algorithm provides stable, realistic and robust outputs. The disadvantage of the algorithm is reduced precision in its outputs due to the approximation inherent in the fuzzy logic. Feed back control logic is adopted to eliminate error caused by the system disturbances as well as error caused by the reduced precision in the outputs. The algorithm is tested by applying it to water level control problem in a fictitious canal with a single pool and also in a real canal with a series of pools. It is found that results obtained from the algorithm are comparable to those obtained from conventional control algorithms.

Glass transition. A new approach based on cluster model of glasses

The structure of real glasses has been considered to be microheterogeneous, composed of clusters and connective tissue. Particles in the cluster are assumed to be highly correlated in positions. The tissue is considered to have a truly amorphous structure with its particles vibrating in highly anharmonic potentials. Glass transition is recognized as corresponding to the melting of clusters. A simple mathematical model has been developed which accounts for various known features associated with glass transition, such as range of glass transition temperature,T g, variation ofT g with pressure, etc. Expressions for configurational thermodynamic properties and transport properties of glass forming systems are derived from the model. The relevence and limitations of the model are also discussed.

Physics-Based Thermal Conductivity Model for Metallic Single-Walled Carbon Nanotube Interconnects

In this letter, a closed-form analytical model for temperature-dependent longitudinal diffusive lattice thermal conductivity (kappa) of a metallic single-walled carbon nanotube (SWCNT) has been addressed. Based on the Debye theory, the second-order three-phonon Umklapp, mass difference (MD), and boundary scatterings have been incorporated to formulate. in both low-and high-temperature regimes. It is proposed that. at low temperature (T) follows the T-3 law and is independent of the second-order three-phonon Umklapp and MD scatterings. The form factor due to MD scattering also plays a key role in the significant variation of. in addition to the SWCNT length. The present diameter-independent model of. agrees well with the available experimental data on suspended intrinsic metallic SWCNTs over a wide range of temperature and can be carried forward for electrothermal analyses of CNT-based interconnects.

Compiler-Directed Frequency and Voltage Scaling for a Multiple Clock Domain

Multiple Clock Domain processors provide an attractive solution to the increasingly challenging problems of clock distribution and power dissipation. They allow their chips to be partitioned into different clock domains, and each domain’s frequency (voltage) to be independently configured. This flexibility adds new dimensions to the Dynamic Voltage and Frequency Scaling problem, while providing better scope for saving energy and meeting performance demands. In this paper, we propose a compiler directed approach for MCD-DVFS. We build a formal petri net based program performance model, parameterized by settings of microarchitectural components and resource configurations, and integrate it with our compiler passes for frequency selection.Our model estimates the performance impact of a frequency setting, unlike the existing best techniques which rely on weaker indicators of domain performance such as queue occupancies(used by online methods) and slack manifestation for a particular frequency setting (software based methods).We evaluate our method with subsets of SPECFP2000,Mediabench and Mibench benchmarks. Our mean energy savings is 60.39% (versus 33.91% of the best software technique)in a memory constrained system for cache miss dominated benchmarks, and we meet the performance demands.Our ED2 improves by 22.11% (versus 18.34%) for other benchmarks. For a CPU with restricted frequency settings, our energy consumption is within 4.69% of the optimal.

On the Decidability of Model-Checking Information Flow Properties

Current standard security practices do not provide substantial assurance about information flow security: the end-to-end behavior of a computing system. Noninterference is the basic semantical condition used to account for information flow security. In the literature, there are many definitions of noninterference: Non-inference, Separability and so on. Mantel presented a framework of Basic Security Predicates (BSPs) for characterizing the definitions of noninterference in the literature. Model-checking these BSPs for finite state systems was shown to be decidable in [8]. In this paper, we show that verifying these BSPs for the more expressive system model of pushdown systems is undecidable. We also give an example of a simple security property which is undecidable even for finite-state systems: the property is a weak form of non-inference called WNI, which is not expressible in Mantel’s BSP framework.

A resource based game theoretical model for military conflicts

A resource interaction based game theoretical model for military conflicts is presented in this paper. The model includes both the spatial decision capability of adversaries (decision regarding movement and subsequent distribution of resources) as well as their temporal decision capability (decision regarding level of allocation of resources for conflict with adversary’s resources). Attrition is decided at present by simple deterministic models. An additional feature of this model is the inclusion of the possibility of a given resource interacting with several resources of the adversary.The decisions of the adversaries is determined by solving for the equilibrium Nash strategies given that the objectives of the adversaries may not be in direct conflict. Examples are given to show the applicability of these models and solution concepts.

Physics-Based Band Gap Model for Relaxed and Strained 100] Silicon Nanowires

In this paper, we propose a physics-based simplified analytical model of the energy band gap and electron effective mass in a relaxed and strained rectangular 100] silicon nanowires (SiNWs). Our proposed formulation is based on the effective mass approximation for the nondegenerate two-band model and 4 x 4 Luttinger Hamiltonian for energy dispersion relation of conduction band electrons and the valence band heavy and light holes, respectively. Using this, we demonstrate the effect of the uniaxial strain applied along 100]-direction and a biaxial strain, which is assumed to be decomposed from a hydrostatic deformation along 001] followed by a uniaxial one along the 100]-direction, respectively, on both the band gap and the transport and subband electron effective masses in SiNW. Our analytical model is in good agreement with the extracted data using the extended-Huckel-method-based numerical simulations over a wide range of device dimensions and applied strain.

A Comparative Kinetic and Thermodynamic Perspective of the sigma-Competition Model in Escherichia coli

Transcription is the most fundamental step in gene expression in any living organism. Various environmental cues help in the maturation of core RNA polymerase (RNAP; alpha(2)beta beta'omega) with different sigma-factors, leading to the directed recruitment of RNAP to different promoter DNA sequences. Thus it is essential to determine the sigma-factors that affect the preferential partitioning of core RNAP among various a-actors, and the role of sigma-switching in transcriptional gene regulation. Further, the macromolecular assembly of holo RNAP takes place in an extremely crowded environment within a cell, and thus far the kinetics and thermodynamics of this molecular recognition process have not been well addressed. In this study we used a site-directed bioaffinity immobilization method to evaluate the relative binding affinities of three different Escherichia coli sigma-factors to the same core RNAP with variations in temperature and ionic strength while emulating the crowded cellular milieu. Our data indicate that the interaction of core RNAP-sigma is susceptible to changes in external stimuli such as osmolytic and thermal stress, and the degree of susceptibility varies among different sigma-factors. This allows for a reversible sigma-switching from housekeeping factors to alternate sigma-factors when the organism senses a change in its physiological conditions.

Petri net based performance modeling for effective DVFS for multithreaded programs

Dynamic Voltage and Frequency Scaling (DVFS) is a very effective tool for designing trade-offs between energy and performance. In this paper, we use a formal Petri net based program performance model that directly captures both the application and system properties, to find energy efficient DVFS settings for CMP systems, that satisfy a given performance constraint, for SPMD multithreaded programs. Experimental evaluation shows that we achieve significant energy savings, while meeting the performance constraints.

Edge-based connected component approach for skew correction of complex document images

Skew correction of complex document images is a difficult task. We propose an edge-based connected component approach for robust skew correction of documents with complex layout and content. The algorithm essentially consists of two steps - an 'initialization' step to determine the image orientation from the centroids of the connected components and a 'search' step to find the actual skew of the image. During initialization, we choose two different sets of points regularly spaced across the the image, one from the left to right and the other from top to bottom. The image orientation is determined from the slope between the two succesive nearest neighbors of each of the points in the chosen set. The search step finds succesive nearest neighbors that satisfy the parameters obtained in the initialization step. The final skew is determined from the slopes obtained in the 'search' step. Unlike other connected component based methods, the proposed method does not require any binarization step that generally precedes connected component analysis. The method works well for scanned documents with complex layout of any skew with a precision of 0.5 degrees.

A denotational semantics for the generalized ER model and a simple ER algebra

The recent spurt of research activities in Entity-Relationship Approach to databases calls for a close scrutiny of the semantics of the underlying Entity-Relationship models, data manipulation languages, data definition languages, etc. For reasons well known, it is very desirable and sometimes imperative to give formal description of the semantics. In this paper, we consider a specific ER model, the generalized Entity-Relationship model (without attributes on relationships) and give denotational semantics for the model as well as a simple ER algebra based on the model. Our formalism is based on the Vienna Development Method—the meta language (VDM). We also discuss the salient features of the given semantics in detail and suggest directions for further work.

Recovery from DoS Attacks in MIPv6: Modelling and Validation

Denial-of-service (DoS) attacks form a very important category of security threats that are prevalent in MIPv6 (mobile internet protocol version 6) today. Many schemes have been proposed to alleviate such threats, including one of our own [9]. However, reasoning about the correctness of such protocols is not trivial. In addition, new solutions to mitigate attacks may need to be deployed in the network on a frequent basis as and when attacks are detected, as it is practically impossible to anticipate all attacks and provide solutions in advance. This makes it necessary to validate the solutions in a timely manner before deployment in the real network. However, threshold schemes needed in group protocols make analysis complex. Model checking threshold-based group protocols that employ cryptography have not been successful so far. Here, we propose a new simulation based approach for validation using a tool called FRAMOGR that supports executable specification of group protocols that use cryptography. FRAMOGR allows one to specify attackers and track probability distributions of values or paths. We believe that infrastructure such as FRAMOGR would be required in future for validating new group based threshold protocols that may be needed for making MIPv6 more robust.