Functional programming systems revisited

Functional Programming (FP) systems are modified and extended to form Nondeterministic Functional Programming (NFP) systems in which nondeterministic programs can be specified and both deterministic and nondeterministic programs can be verified essentially within the system. It is shown that the algebra of NFP programs has simpler laws in comparison with the algebra of FP programs. "Regular" forms are introduced to put forward a disciplined way of reasoning about programs. Finally, an alternative definition of "linear" forms is proposed for reasoning about recursively defined programs. This definition, when used to test the linearity of forms, results in simpler verification conditions than those generated by the original definition of linear forms.

A functional style of programming with CSP-like communication mechanisms

This paper introduces CSP-like communication mechanisms into Backus’ Functional Programming (FP) systems extended by nondeterministic constructs. Several new functionals are used to describe nondeterminism and communication in programs. The functionals union and restriction are introduced into FP systems to develop a simple algebra of programs with nondeterminism. The behaviour of other functionals proposed in this paper are characterized by the properties of union and restriction. The axiomatic semantics of communication constructs are presented. Examples show that it is possible to reason about a communicating program by first transforming it into a non-communicating program by using the axioms of communication, and then reasoning about the resulting non-communicating version of the program. It is also shown that communicating programs can be developed from non-communicating programs given as specifications by using a transformational approach.

Conflict-Tolerant Real-Time Specifications in Metric Temporal Logic

A framework based on the notion of "conflict-tolerance" was proposed in as a compositional methodology for developing and reasoning about systems that comprise multiple independent controllers. A central notion in this framework is that of a "conflict-tolerant" specification for a controller. In this work we propose a way of defining conflict-tolerant real-time specifications in Metric Interval Temporal Logic (MITL). We call our logic CT-MITL for Conflict-Tolerant MITL. We then give a clock optimal "delay-then-extend" construction for building a timed transition system for monitoring past-MITL formulas. We show how this monitoring transition system can be used to solve the associated verification and synthesis problems for CT-MITL.

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.

WCET Estimation for Executables in the Presence of Data Caches

This paper describes techniques to estimate the worst case execution time of executable code on architectures with data caches. The underlying mechanism is Abstract Interpretation, which is used for the dual purposes of tracking address computations and cache behavior. A simultaneous numeric and pointer analysis using an abstraction for discrete sets of values computes safe approximations of access addresses which are then used to predict cache behavior using Must Analysis. A heuristic is also proposed which generates likely worst case estimates. It can be used in soft real time systems and also for reasoning about the tightness of the safe estimate. The analysis methods can handle programs with non-affine access patterns, for which conventional Presburger Arithmetic formulations or Cache Miss Equations do not apply. The precision of the estimates is user-controlled and can be traded off against analysis time. Executables are analyzed directly, which, apart from enhancing precision, renders the method language independent.

Does lean imply green?: a study of the power performance implications of Java runtime bloat

The presence of software bloat in large flexible software systems can hurt energy efficiency. However, identifying and mitigating bloat is fairly effort intensive. To enable such efforts to be directed where there is a substantial potential for energy savings, we investigate the impact of bloat on power consumption under different situations. We conduct the first systematic experimental study of the joint power-performance implications of bloat across a range of hardware and software configurations on modern server platforms. The study employs controlled experiments to expose different effects of a common type of Java runtime bloat, excess temporary objects, in the context of the SPECPower_ssj2008 workload. We introduce the notion of equi-performance power reduction to characterize the impact, in addition to peak power comparisons. The results show a wide variation in energy savings from bloat reduction across these configurations. Energy efficiency benefits at peak performance tend to be most pronounced when bloat affects a performance bottleneck and non-bloated resources have low energy-proportionality. Equi-performance power savings are highest when bloated resources have a high degree of energy proportionality. We develop an analytical model that establishes a general relation between resource pressure caused by bloat and its energy efficiency impact under different conditions of resource bottlenecks and energy proportionality. Applying the model to different "what-if" scenarios, we predict the impact of bloat reduction and corroborate these predictions with empirical observations. Our work shows that the prevalent software-only view of bloat is inadequate for assessing its power-performance impact and instead provides a full systems approach for reasoning about its implications.

Conflict-tolerant specifications for hybrid systems

We propose a framework for developing and reasoning about hybrid systems that are comprised of a plant with multiple controllers, each of which controls the plant intermittently. The framework is based on the notion of a ``conflict tolerant'' specification for a controller, and provides a modular way of developing and reasoning about such systems. We propose a novel mechanism of defining conflict-tolerant specifications for general hybrid systems, using ``acceptor'' and ``advisor'' components. We also give a decision procedure for verifying whether a controller satisfies its conflict-tolerant specification, in the special case when the components are modeled using initialized rectangular hybrid automata.

Trace Driven Dynamic Deadlock Detection and Reproduction

Dynamic analysis techniques have been proposed to detect potential deadlocks. Analyzing and comprehending each potential deadlock to determine whether the deadlock is feasible in a real execution requires significant programmer effort. Moreover, empirical evidence shows that existing analyses are quite imprecise. This imprecision of the analyses further void the manual effort invested in reasoning about non-existent defects. In this paper, we address the problems of imprecision of existing analyses and the subsequent manual effort necessary to reason about deadlocks. We propose a novel approach for deadlock detection by designing a dynamic analysis that intelligently leverages execution traces. To reduce the manual effort, we replay the program by making the execution follow a schedule derived based on the observed trace. For a real deadlock, its feasibility is automatically verified if the replay causes the execution to deadlock. We have implemented our approach as part of WOLF and have analyzed many large (upto 160KLoC) Java programs. Our experimental results show that we are able to identify 74% of the reported defects as true (or false) positives automatically leaving very few defects for manual analysis. The overhead of our approach is negligible making it a compelling tool for practical adoption.

Cystine peptides. Disulfide conformations in fourteen membered loops investigated by Raman spectroscopy and circular dichroism

NHCH3 (X = Gly 1, Ala 2, Aib 3, Leu 4 and D-Ala 5), have been investigated by Raman and circular dichroism (CD) spectroscopy. Solid state Raman spectra are consistent with β-turn conformations in all five peptides. These peptides exhibit similar conformations of the disulfide segment in the solid state with a characteristic disulfide stretching frequency at 519 ± 3 cm-1, indicative of a trans-gauche-gauche arrangement about the Cα—Cβ—S—S—Cβ—Cα bonds. The results correlate well with the solid state conformations determined by X-ray diffraction for peptides 3 and 4. CD studies in chloroform and dimethylsulfoxide establish solvent dependent conformational changes for peptides 1, 3 and 5. Disulfide chirality has been derived using the quadrant rule. CD results together with previously reported nuclear magnetic resonance (n.m.r.) data suggest a conformational coupling between the peptide backbone and the disulfide segment

Assessment of luteal rescue and desensitization of macaque corpus luteum brought about by human chorionic gonadotrophin and deglycosylated human chorionic gonadotrophin treatment

The objective of the current study was to investigate the mechanism by which the corpus luteum (CL) of the monkey undergoes desensitization to luteinizing hormone following exposure to increasing concentration of human chorionic gonadotrophin (hCG) as it occurs in pregnancy. Female bonnet monkeys were injected (im) increasing doses of hCG or dghCG beginning from day 6 or 12 of the luteal phase for either 10 or 4 or 2 days. The day of oestrogen surge was considered as day '0' of luteal phase. Luteal cells obtained from CL of these animals were incubated with hCG (2 and 200 pg/ml) or dbcAMP (2.5, 25 and 100 mu M) for 3 h at 37 degrees C and progesterone secreted was estimated. Corpora lutea of normal cycling monkeys on day 10/16/22 of the luteal phase were used as controls, In addition the in vivo response to CG and deglycosylated hCG (dghCG) was assessed by determining serum steroid profiles following their administration. hCG (from 15-90 IU) but not dghCG (15-90 IU) treatment in vivo significantly (P < 0.05) elevated serum progesterone and oestradiol levels. Serum progesterone, however, could not be maintained at a elevated level by continuous treatment with hCG (from day 6-15), the progesterone level declining beyond day 13 of luteal phase. Administering low doses of hCG (15-90 IU/day) from day 6-9 or high doses (600 IU/day) on days 8 and 9 of the luteal phase resulted in significant increase (about 10-fold over corresponding control P < 0.005) in the ability of luteal cells to synthesize progesterone (incubated controls) in vitro. The luteal cells of the treated animals responded to dbcAMP (P < 0.05) but not to hCG added in vitro, The in vitro response of luteal cells to added hCG was inhibited by 0, 50 and 100% if the animals were injected with low (15-90 IU) or medium (100 IU) between day 6-9 of luteal phase and high (600 IU on day 8 and 9 of luteal phase) doses of dghCG respectively; such treatment had no effect on responsivity of the cells to dbcAMP, The luteal cell responsiveness to dbcAMP in vitro was also blocked if hCG was administered for 10 days beginning day 6 of the luteal phase. Though short term hCG treatment during late luteal phase (from days 12-15) had no effect on luteal function, 10 day treatment beginning day 12 of luteal phase resulted in regain of in vitro responsiveness to both hCG (P < 0.05) and dbcAMP (P < 0.05) suggesting that luteal rescue can occur even at this late stage. In conclusion, desensitization of the CL to hCG appears to be governed by the dose/period for which it is exposed to hCG/dghCG. That desensitization is due to receptor occupancy is brought out by the fact that (i) this can be achieved by giving a larger dose of hCG over a 2 day period instead of a lower dose of the hormone for a longer (4 to 10 days) period and (ii) the effect can largely be reproduced by using dghCG instead of hCG to block the receptor sites. It appears that to achieve desensitization to dbcAMP also it is necessary to expose the luteal cell to relatively high dose of hCG for more than 4 days.

Conformational analysis of small disulfide loops. Spectroscopic and theoretical studies on a synthetic cyclic tetrapeptide containing cystine

The conformational analysis of the synthetic peptide Boc-Cys-Pro-Val-Cys-NHMe has been carried out, as a model for small disulfide loops, in biologically active polypeptides. 'H NMR studies (270 MHz) establish that the Val(3) and Cys(4) NH groups are solvent shielded, while 13C studies establish an all-trans peptide backbone. Circular dichroism and Raman spectroscopy provide evidence for a right-handed twist of the disulfide bond. Analysis of the vicinal (JaB)c oupling constants for the two Cys residues establishes that XI - *60° for Cys(4), while some flexibility is suggested at Cys( 1). Conformational energy calculations, imposing intramolecular hydrogen bonding constraints, favor a P-turn (type I) structure with Pro(2)-Va1(3) as the corner residues. Theoretical and spectroscopic results are consistent with the presence of a transannular 4 - 1 hydrogen bond between Cys( 1) CO and Cys(4) NH groups, with the Val NH being sterically shielded from the solvent environment.

Flow between torsionally oscillating disks rotating about different axes at different speeds

The flow of an incompressible viscous fluid confined between two parallel infinite disks performing torsional oscillations with the same frequency, but rotating about different axes with different speeds has been studied. The solutions are presented for the symmetric and asymmetric first harmonic and steady streaming. The interesting features of the symmetric and asymmetric flow are discussed for the cases of small and large Womersley parameter at different ratios of the rotation speeds. The forces acting on one of the disks are also calculated.

How Good is the Assumption About Visible Surface Reflectance in MODIS Aerosol Retrieval Over Land? A Comparison With Aircraft Measurements Over an Urban Site in India

In this paper, we discuss the measurements of spectral surface reflectance (rho(s)(lambda)) in the wavelength range 350-2500 nm measured using a spectroradiometer onboard a low-flying aircraft over Bangalore (12.95 degrees N, 77.65 degrees E), an urban site in southern India. The large discrepancies in the retrieval of aerosol propertiesover land by the Moderate-Resolution Imaging Spectroradiometer (MODIS), which could be attributed to the inaccurate estimation of surface reflectance at many sites in India and elsewhere, provided motivation for this paper. The aim of this paper was to verify the surface reflectance relationships assumed by the MODIS aerosol algorithm for the estimation of surface reflectance in the visible channels (470 and 660 nm) from the surface reflectance at 2100 nm for aerosol retrieval over land. The variety of surfaces observed in this paper includes green and dry vegetations, bare land, and urban surfaces. The measuredreflectance data were first corrected for the radiative effects of atmosphere lying between the ground and aircraft using the Second Simulation of Satellite Signal in the Solar Spectrum (6S) radiative transfer code. The corrected surface reflectance in the MODIS's blue (rho(s)(470)), red (rho(s)(660)), and shortwave-infrared (SWIR) channel (rho(s)(2100)) was linearly correlated. We found that the slope of reflectance relationship between 660 and 2100 nm derived from the forward scattering data was 0.53 with an intercept of 0.07, whereas the slope for the relationship between the reflectance at 470 and 660 nm was 0.85. These values are much higher than the slope (similar to 0.49) for either wavelengths assumed by the MODIS aerosol algorithm over this region. The reflectance relationship for the backward scattering data has a slope of 0.39, with an intercept of 0.08 for 660 nm, and 0.65, with an intercept of 0.08 for 470 nm. The large values of the intercept (which is very small in the MODIS reflectance relationships) result in larger values of absolute surface reflectance in the visible channels. The discrepancy between the measured and assumed surface reflectances could lead to error in the aerosol retrieval. The reflectance ratio (rho(s)(660)/rho(s)(2100)) showed a clear dependence on the N D V I-SWIR where the ratio increased from 0.5 to 1 with an increase in N V I-SWIR from 0 to 0.5. The high correlation between the reflectance at SWIR wavelengths (2100, 1640, and 1240 nm) indicated an opportunity to derive the surface reflectance and, possibly, aerosol properties at these wavelengths. We need more experiments to characterize the surface reflectance and associated inhomogeneity of land surfaces, which play a critical role in the remote sensing of aerosols over land.

Is Human-X Chromosome Inactivation A Sex-Determining Device

The evolutionary function of X chromosome inactivation is thought to be dosage compensation. However, there is, at present, little evidence to suggest that most X chromosome-linked genes require such compensation. Another view--that X chromosome inactivation may be related to sex determination--is examined here. Consider a hypothetical DNA sequence regulating a major structural gene concerned with the determination of maleness. If this regulatory sequence occurs in both X and Y chromosomes and if its copy number in the Y chromosome is significantly greater than in the X chromosome, then the male-determining properties of the Y chromosome could be attributed to this higher copy number. On the other hand, if the Y chromosome has the same copy number of this sequence as the X chromosome, it is difficult to see how determination of two sexes would occur under such circumstances because XX and XY genomes would then be indistinguishable in this regard. Such a situation seems to occur in the human species with respect to the banded krait minor satellite, a repetitious DNA sequence associated with sex determination. This apparent difficulty may be resolved if X chromosome inactivation renders regulatory as well as structural genes nonfunctional and thereby brings about a significant reduction in the effective copy number of X chromosome-linked DNA sequences concerned with sex determination. It is suggested that X chromosome inactivation brings about, in this manner, a critical inequality between XX and XY embryos and that sex determination in humans is a consequence of this inequality. An analogous situation appears to exist in certain insects in which inactivation of a haploid set of chromosomes (and presumably, therefore, a 50% reduction in the effective copy number of most genes) is associated with maleness. If this line of reasoning is correct, it would suggest that sex determination may be the primary function of X chromosome inactivation.