Description: The safety of remotely operated vehicles depends on the correctness of the distributed protocol that facilitates the communication between the vehicle and the operator. A failure in this communication can result in catastrophic loss of the vehicle. To complicate matters, the communication system may be required to satisfy several, possibly conflicting, requirements. The design of protocols is typically an informal process based on successive iterations of a prototype implementation. Yet distributed protocols are notoriously difficult to get correct using such informal techniques. We present a formal specification of the design of a distributed protocol intended for use in a remotely operated vehicle, which is built from the composition of several simpler protocols. We demonstrate proof strategies that allow us to prove properties of each component protocol individually while ensuring that the property is preserved in the composition forming the entire system. Given that designs are likely to evolve as additional requirements emerge, we show how we have automated most of the repetitive proof steps to enable verification of rapidly changing designs.

Description: An investigation is made of the mutual interference of the wings of a biplane under the general assumption that each wing may be replaced by a vortex system of the type given by the Prandtl wing theory. The additional velocities induced at each wing by the presence of the other are determined by the Biot-Savart law and converted into an equivalent change in the angle of attack, the effect being that of an additional twist given to the wings in changing their lift distributions. The lift distributions computed in this manner for several airplane types are compared with the results of measurement.

Description: None

Description: The effect of the existing turbulence in the full scale tunnel was determined from measurements of the profile drag of an N-22 section by the momentum method under corresponding conditions in flight and the tunnel. The transition-point location on the upper surface of the air-foil was also determined from velocity surveys in the boundary layer. The measurements were made at section lift coefficients from 0.480 to 0.635 with a range of Reynolds Numbers from 4,600,000 to 3,900,000. The results show that the end of transition occurs at approximately the same point on the airfoil in flight and in the tunnel. The transition region was somewhat broader in the tunnel and started farther forward than in flight. The laminar profiles in the tunnel had some characteristics of transition profiles in the tunnel and had a much steeper slope near the surface than did the laminar profiles obtained in flight. These differences, however, caused an increase of only 0.0001 in the profile-drag coefficients, as determined by the momentum method.

Description: Torsion tests were made on 51ST aluminum-alloy seamless tubes having diameter-to-thickness ratios of from 77 to 139 and length-to-diameter ratios of from 1 to 60. The torsional strengths developed in the tubes which failed elastically (all tubes having lengths greater than 2 to 6 times the diameter) were in most cases within 10 percent of the value indicated by the theories of Donnel, Timoshenko, and Sturm, assuming a condition of simply supported ends.