LED bulbs technical specification and testing procedure for solar home systems

The definition of technical specifications and the corresponding laboratory procedures are necessary steps in order to assure the quality of the devices prior to be installed in Solar Home Systems (SHS). To clarify and unify criteria a European project supported the development of the Universal Technical Standard for Solar Home Systems (UTSfSHS). Its principles were to generate simple and affordable technical requirements to be optimized in order to facilitate the implementation of tests with basic and simple laboratory tools even on the same SHS electrification program countries. These requirements cover the main aspects of this type of installations and its lighting chapter was developed based on the most used technology at that time: fluorescent tubes and CFLs. However, with the consolidation of the new LED solid state lighting devices, particular attention is being given to this matter and new procedures are required. In this work we develop a complete set of technical specifications and test procedures that have been designed within the frame of the UTSfSHS, based on an intense review of the scientific and technical publications related to LED lighting and their practical application. They apply to lamp reliability, performance and safety under normal, extreme and abnormal operating conditions as a simple but complete quality meter tool for any LED bulb.

An intrinsic genetic program for autonomous differentiation of muscle cells in the ascidian embryo.

The B-line presumptive muscle cells of ascidian embryos have extensive potential for self-differentiation dependent on determinants prelocalized in the myoplasm of fertilized eggs. Ascidian larval muscle cells therefore provide an experimental system with which to explore an intrinsic genetic program for autonomous specification of embryonic cells. Experiments with egg fragments suggested that maternal mRNAs are one of the components of muscle determinants. Expression of larval muscle actin genes begins as early as the 32-cell stage, prior to the developmental fate restriction of the cells. The timing of initiation of the actin gene expression proceeds the expression of an ascidian homologue of vertebrate MyoD by a few hours. Mutations in the proximal E-box of the 5' flanking region of the actin genes did not alter the promoter activity for muscle-specific expression of reporter gene. These results, together with results of deletion constructs of fusion genes, suggest that muscle determinants regulate directly, or indirectly via regulatory factors other than MyoD, the transcription of muscle-specific structural genes leading to the terminal differentiation.

Evidence for a Myotomal Hox/Myf Cascade Governing Nonautonomous Control of Rib Specification within Global Vertebral Domains

Hox genes are essential for the patterning of the axial skeleton. Hox group 10 has been shown to specify the lumbar domain by setting a rib-inhibiting program in the presomitic mesoderm (PSM). We have now produced mice with ribs in every vertebra by ectopically expressing Hox group 6 in the PSM, indicating that Hox genes are also able to specify the thoracic domain. We show that the information provided by Hox genes to specify rib-containing and rib-less areas is first interpreted in the myotome through the regional-specific control of Myf5 and Myf6 expression. This information is then transmitted to the sclerotome by a system that includes FGF and PDGF signaling to produce vertebrae with or without ribs at different axial levels. Our findings offer a new perspective of how Hox genes produce global patterns in the axial skeleton and support a redundant nonmyogenic role of Myf5 and Myf6 in rib formation.

Procedures and parameters in the real-time program refinement calculus

The real-time refinement calculus is a formal method for the systematic derivation of real-time programs from real-time specifications in a style similar to the non-real-time refinement calculi of Back and Morgan. In this paper we extend the real-time refinement calculus with procedures and provide refinement rules for refining real-time specifications to procedure calls. A real-time specification can include constraints on, not only what outputs are produced, but also when they are produced. The derived programs can also include time constraints oil when certain points in the program must be reached; these are expressed in the form of deadline commands. Such programs are machine independent. An important consequence of the approach taken is that, not only are the specifications machine independent, but the whole refinement process is machine independent. To implement the machine independent code on a target machine one has a separate task of showing that the compiled machine code will reach all its deadlines before they expire. For real-time programs, externally observable input and output variables are essential. These differ from local variables in that their values are observable over the duration of the execution of the program. Hence procedures require input and output parameter mechanisms that are references to the actual parameters so that changes to external inputs are observable within the procedure and changes to output parameters are externally observable. In addition, we allow value and result parameters. These may be auxiliary parameters, which are used for reasoning about the correctness of real-time programs as well as in the expression of timing deadlines, but do not lead to any code being generated for them by a compiler. (c) 2006 Elsevier B.V. All rights reserved.

A technique for modular logic program refinement

A refinement calculus provides a method for transforming specifications to executable code, maintaining the correctness of the code with respect to its specification. In this paper we introduce modules into a logic programming refinement calculus. Modules allow data types to be grouped together with sets of procedures that manipulate the data types. By placing restrictions on the way a program uses a module, we develop a technique for refining the module so that it uses a more efficient representation of the data type.

Supporting the software testing process through specification animation

Achieving consistency between a specification and its implementation is an important part of software development. In this paper, we present a method for generating passive test oracles that act as self-checking implementations. The implementation is verified using an animation tool to check that the behavior of the implementation matches the behavior of the specification. We discuss how to integrate this method into a framework developed for systematically animating specifications, which means a tester can significantly reduce testing time and effort by reusing work products from the animation. One such work product is a testgraph: a directed graph that partially models the states and transitions of the specification. Testgraphs are used to generate sequences for animation, and during testing, to execute these same sequences on the implementation.

Integrating runtime assertions with dynamic types: Structuring a derivation from an incomputable specification

An inherent incomputability in the specification of a functional language extension that combines assertions with dynamic type checking is isolated in an explicit derivation from mathematical specifications. The combination of types and assertions (into "dynamic assertion-types" - DATs) is a significant issue since, because the two are congruent means for program correctness, benefit arises from their better integration in contrast to the harm resulting from their unnecessary separation. However, projecting the "set membership" view of assertion-checking into dynamic types results in some incomputable combinations. Refinement of the specification of DAT checking into an implementation by rigorous application of mathematical identities becomes feasible through the addition of a "best-approximate" pseudo-equality that isolates the incomputable component of the specification. This formal treatment leads to an improved, more maintainable outcome with further development potential.