Towards formal specification of a distributed computing system

Onboard spacecraft computing system is a case of a functionally distributed system that requires continuous interaction among the nodes to control the operations at different nodes. A simple and reliable protocol is desired for such an application. This paper discusses a formal approach to specify the computing system with respect to some important issues encountered in the design and development of a protocol for the onboard distributed system. The issues considered in this paper are concurrency, exclusiveness and sequencing relationships among the various processes at different nodes. A 6-tuple model is developed for the precise specification of the system. The model also enables us to check the consistency of specification and deadlock caused due to improper specification. An example is given to illustrate the use of the proposed methodology for a typical spacecraft configuration. Although the theory is motivated by a specific application the same may be applied to other distributed computing system such as those encountered in process control industries, power plant control and other similar environments.

Optimal maintenance policy for equipment subject to random deterioration and random failure A modern control theory approach.

The stochastic version of Pontryagin's maximum principle is applied to determine an optimal maintenance policy of equipment subject to random deterioration. The deterioration of the equipment with age is modelled as a random process. Next the model is generalized to include random catastrophic failure of the equipment. The optimal maintenance policy is derived for two special probability distributions of time to failure of the equipment, namely, exponential and Weibull distributions Both the salvage value and deterioration rate of the equipment are treated as state variables and the maintenance as a control variable. The result is illustrated by an example

Adsorption of Nitrogen on Activated Carbon-Refit of Experimental Data and Derivation of Properties Required for Design of Equipment

Volumetric method based adsorption measurements of nitrogen on two specimens of activated carbon (Fluka and Sarabhai) reported by us are refitted to two popular isotherms, namely, Dubunin−Astakhov (D−A) and Toth, in light of improved fitting methods derived recently. Those isotherms have been used to derive other data of relevance in design of engineering equipment such as the concentration dependence of heat of adsorption and Henry’s law coefficients. The present fits provide a better representation of experimental measurements than before because the temperature dependence of adsorbed phase volume and structural heterogeneity of micropore distribution have been accounted for in the D−A equation. A new correlation to the Toth equation is a further contribution. The heat of adsorption in the limiting uptake condition is correlated with the Henry’s law coefficients at the near zero uptake condition.

Specification-driven approach for protocol design of distributed computing systems

An important issue in the design of a distributed computing system (DCS) is the development of a suitable protocol. This paper presents an effort to systematize the protocol design procedure for a DCS. Protocol design and development can be divided into six phases: specification of the DCS, specification of protocol requirements, protocol design, specification and validation of the designed protocol, performance evaluation, and hardware/software implementation. This paper describes techniques for the second and third phases, while the first phase has been considered by the authors in their earlier work. Matrix and set theoretic based approaches are used for specification of a DCS and for specification of the protocol requirements. These two formal specification techniques form the basis of the development of a simple and straightforward procedure for the design of the protocol. The applicability of the above design procedure has been illustrated by considering an example of a computing system encountered on board a spacecraft. A Petri-net based approach has been adopted to model the protocol. The methodology developed in this paper can be used in other DCS applications.

Specification of Real-Time Systems

Inspite of numerous research advancements made in recent years in the area of formal techniques, specification of real-time systems is still proving to be a very challenging and difficult problem. In this context, this paper critically examines state-of-the-art specification techniques for real-time systems and analyzes the emerging trends.

Specification Based Regression Testing Using Explicit State Space Enumeration

This paper presents a method of partial automation of specification based regression testing, which we call ESSE (Explicit State Space Enumeration). The first step in ESSE method is the extraction of a finite state model of the system making use of an already tested version of the system under test (SUT). Thereafter, the finite state model thus obtained is used to compute good test sequences that can be used to regression test subsequent versions of the system. We present two new algorithms for test sequence computation - both based on our finite state model generated by the above method. We also provide the details and results of the experimental evaluation of ESSE method. Comparison with a practically used random-testing algorithm has shown substantial improvements.

Rice LHS1/OsMADS1 Controls Floret Meristem Specification by Coordinated Regulation of Transcription Factors and Hormone Signaling Pathways

SEPALLATA (SEP) MADS box transcription factors mediate floral development in association with other regulators. Mutants in five rice (Oryza sativa) SEP genes suggest both redundant and unique functions in panicle branching and floret development. LEAFY HULL STERILE1/OsMADS1, from a grass-specific subgroup of LOFSEP genes, is required for specifying a single floret on the spikelet meristem and for floret organ development, but its downstream mechanisms are unknown. Here, key pathways and directly modulated targets of OsMADS1 were deduced from expression analysis after its knockdown and induction in developing florets and by studying its chromatin occupancy at downstream genes. The negative regulation of OsMADS34, another LOFSEP gene, and activation of OsMADS55, a SHORT VEGETATIVE PHASE-like floret meristem identity gene, show its role in facilitating the spikelet-to-floret meristem transition. Direct regulation of other transcription factor genes like OsHB4 (a class III homeodomain Leu zipper member), OsBLH1 (a BEL1-like homeodomain member), OsKANADI2, OsKANADI4, and OsETTIN2 show its role in meristem maintenance, determinacy, and lateral organ development. We found that the OsMADS1 targets OsETTIN1 and OsETTIN2 redundantly ensure carpel differentiation. The multiple effects of OsMADS1 in promoting auxin transport, signaling, and auxin-dependent expression and its direct repression of three cytokinin A-type response regulators show its role in balancing meristem growth, lateral organ differentiation, and determinacy. Overall, we show that OsMADS1 integrates transcriptional and signaling pathways to promote rice floret specification and development.

Functions for rice RFL in vegetative axillary meristem specification and outgrowth

Roles for the transcription factor RFL in rice axillary meristem development were studied. Its regulatory effects on LAX1, CUC1, and OsPIN3 reveal its functions in axillary meristem specification and outgrowth.Axillary meristems (AMs) are secondary shoot meristems whose outgrowth determines plant architecture. In rice, AMs form tillers, and tillering mutants reveal an interplay between transcription factors and the phytohormones auxin and strigolactone as some factors that underpin this developmental process. Previous studies showed that knockdown of the transcription factor gene RFL reduced tillering and caused a very large decrease in panicle branching. Here, the relationship between RFL, AM initiation, and outgrowth was examined. We show that RFL promotes AM specification through its effects on LAX1 and CUC genes, as their expression was modulated on RFL knockdown, on induction of RFL:GR fusion protein, and by a repressive RFL-EAR fusion protein. Further, we report reduced expression of auxin transporter genes OsPIN1 and OsPIN3 in the culm of RFL knockdown transgenic plants. Additionally, subtle change in the spatial pattern of IR4 DR5:GFP auxin reporter was observed, which hints at compromised auxin transport on RFL knockdown. The relationship between RFL, strigolactone signalling, and bud outgrowth was studied by transcript analyses and by the tillering phenotype of transgenic plants knocked down for both RFL and D3. These data suggest indirect RFL-strigolactone links that may affect tillering. Further, we show expression modulation of the auxin transporter gene OsPIN3 upon RFL:GR protein induction and by the repressive RFL-EAR protein. These modified forms of RFL had only indirect effects on OsPIN1. Together, we have found that RFL regulates the LAX1 and CUC genes during AM specification, and positively influences the outgrowth of AMs though its effects on auxin transport.

Co-Exploration of NLA Kernels and Specification of Compute Elements in Distributed Memory CGRAs

Coarse Grained Reconfigurable Architectures (CGRA) are emerging as embedded application processing units in computing platforms for Exascale computing. Such CGRAs are distributed memory multi- core compute elements on a chip that communicate over a Network-on-chip (NoC). Numerical Linear Algebra (NLA) kernels are key to several high performance computing applications. In this paper we propose a systematic methodology to obtain the specification of Compute Elements (CE) for such CGRAs. We analyze block Matrix Multiplication and block LU Decomposition algorithms in the context of a CGRA, and obtain theoretical bounds on communication requirements, and memory sizes for a CE. Support for high performance custom computations common to NLA kernels are met through custom function units (CFUs) in the CEs. We present results to justify the merits of such CFUs.