432 research outputs found
A Model to Determine Thermal Performance of a Non-ventilated Double Glazing Unit with PCM and Experimental Validation
No full textAbstractPhase change material (PCM) applied in the double glazing unit can decrease energy consumption and improve indoor thermal comfort by improving its thermal energy storage capacity. In the present work, a model to determine thermal performance of a non-ventilated double glazing unit with PCM and experimental validation was developed. The result shows that the developed model in present work can solve the coupled heat transfer problem between phase change and solar heat transfer in the double glazing unit filled with PCM
Optimal Control Problems with State Constraint Governed by Magnetohydrodynamic Equations
No full text
Recommended from our members
Formal specification and verification of a JVM and its bytecode verifier
No full texttextHow do we know that a bytecode-verified Java program will run safely?
This dissertation addresses the question by building a precise model of the
JVM and its bytecode verifier. We also built a “small” machine and its bytecode
verifier to demonstrate an approach to solving this problem. We proved
that for any program on the small machine that has been vetted by the small
bytecode verifier, then that program will run safely on the small machine. We
created substantial libraries of ACL2 definitions and lemmas towards specifying
and proving that the JVM safely executes verified programs.
The fundamental problem is to connect the abstract execution of the
bytecode verifier with the concrete execution of the JVM. These diverge in two
ways: (1) the bytecode verifier executes on more abstract states and (2) its
execution of INVOKE-family and BRANCH-family instructions differs from
their execution by the JVM.
Our contribution was identification of a critical “on-track” property
that, despite these divergences between the bytecode verifier and the JVM,
enables one to use the success of bytecode verification to predict the safety of
concrete execution.
The second difficulty is that the official specification describes many
“procedural” aspects of the bytecode verification process. These aspects obscure
the checks conducted by the bytecode verifier.
We introduce an alternative bytecode verifier without such “procedural”
aspects. We use the new bytecode verifier as a stepping stone for proving that
the official bytecode verifier is effective.
Following this methodology allowed us to prove, on our ”small”
machine, that executions of bytecode-verified programs never overflow the
operand stack.
We note that significant effort is required in order to extend this result
from our “small” machine to the full JVM. We have formulated appropriate
stronger notions of “safe” execution for programs on the full JVM. We introduced
an alternative bytecode verifier. We proved the “reduction theorem”
that relates the official bytecode verifier with the alternative bytecode veri-
fier. We completed proofs of several thousand lemmas towards proving the
“safe” execution of bytecode-verified programs on the full JVM. Our results
are organized into supporting lemma libraries.Computer Scienc
An Analysis on Development Predicaments of Privately-owned Small & Medium Enterprises and Countermeasures
No full textThrough field survey on 100 privately-owned small and medium enterprises in Shijiazhuang of He bei province and relevant data collection, the author finds that their development has been severely impeded by such phenomena as financing dilemma, retention difficulty and chaotic management. On the basis of theories of management and social development, reasons for development predicaments are systematically analyzed by means of combining qualitative and quantitative studies. In the meantime, based on relevant economic theories and reference to advanced experience and theories at home and abroad, the author proposes countermeasures and suggestions for development predicament of SMEs, which are relatively suitable for Shijiazhuang City
- …
