A field model interpretation of crack initiation and growth behavior in ferroelectric ceramics: change of poling direction and boundary condition

Strain energy density expressions are obtained from a field model that can qualitatively exhibit how the electrical and mechanical disturbances would affect the crack growth behavior in ferroelectric ceramics. Simplification is achieved by considering only three material constants to account for elastic, piezoelectric and dielectric effects. Cross interaction of electric field (or displacement) with mechanical stress (or strain) is identified with the piezoelectric effect; it occurs only when the pole is aligned normal to the crack. Switching of the pole axis by 90degrees and 180degrees is examined for possible connection with domain switching. Opposing crack growth behavior can be obtained when the specification of mechanical stress sigma(infinity) and electric field E-infinity or (sigma(infinity), E-infinity) is replaced by strain e and electric displacement D-infinity or (epsilon(infinity), D-infinity). Mixed conditions (sigma(infinity),D-infinity) and (epsilon(infinity),E-infinity) are also considered. In general, crack growth is found to be larger when compared to that without the application of electric disturbances. This includes both the electric field and displacement. For the eight possible boundary conditions, crack growth retardation is identified only with (E-y(infinity),sigma(y)(infinity)) for negative E-y(infinity) and (D-y(infinity), epsilon(y)(infinity)) for positive D-y(infinity) while the mechanical conditions sigma(y)(infinity) or epsilon(y)infinity are not changed. Suitable combinations of the elastic, piezoelectric and dielectric material constants could also be made to suppress crack growth. (C) 2002 Published by Elsevier Science Ltd.

Formal specification and refinement of a safe train control function

Motivated by the design and development challenges of the BART case study, an approach for developing and analyzing a formal model for reactive systems is presented. The approach makes use of a domain specific language for specifying control algorithms able to satisfy competing properties such as safety and optimality. The domain language, called SPC, offers several key abstractions such as the state, the profile, and the constraint to facilitate problem specification. Using a high-level program transformation system such as HATS being developed at the University of Nebraska at Omaha, specifications in this modelling language can be transformed to ML code. The resulting executable specification can be further refined by applying generic transformations to the abstractions provided by the domain language. Problem dependent transformations utilizing the domain specific knowledge and properties may also be applied. The result is a significantly more efficient implementation which can be used for simulation and gaining deeper insight into design decisions and various control policies. The correctness of transformations can be established using a rewrite-rule based induction theorem prover Rewrite Rule Laboratory developed at the University of New Mexico.