Recently, transducers with high resolution are required in the fields of ultrasonic imaging and non-destructive testing. The plano-convex and plano-concave transducers treated in this paper are suitable for these purposes. These transducers show the focusing effect and broad frequency bandwidth for the radiation of ultrasonic pulses. These two features show the high lateral-distance and time resolutions respectively. However, the principle of the focusing effect on these transducers has been vague until now. This focusing effect will be discussed in this paper. The mechanisms of the focusing effect for ultrasonic pulses radiated from the plano-convex and plano-concave transducers are cleared through two experiments using a wedged transducer and a semi-cylindrical transducer. Also, the formulas for the geometrical focal points of pulses radiated from each transducer are derived, and its calculations are compared with the measurements.

Refinement-based formal specification is a promising approach to the increasing complexity of software systems, as demonstrated in the formal method Event-B. It allows stepwise modeling and verifying of complex systems with multiple steps at different abstraction levels. However, making changes is more difficult, as caution is necessary to avoid breaking the consistency between the steps. Judging whether a change is valid or not is a non-trivial task, as the logical dependency relationships between the modeling elements (predicates) are implicit and complex. In this paper, we propose a method for analyzing the impact of the changes of Event-B. By attaching labels to modeling elements (predicates), the method helps engineers understand how a model is structured and what needs to be modified to accomplish a change.