The technology now exists to construct physical models of proteins based on atomic coordinates of solved structures. We review here our recent experiences in using physical models to teach concepts of protein structure and function at both the high school and the undergraduate levels. At the high school level, physical models are used in a professional development program targeted to biology and chemistry teachers. This program has recently been expanded to include two student enrichment programs in which high school students participate in physical protein modeling activities. At the undergraduate level, we are currently exploring the usefulness of physical models in communicating concepts of protein structure and function that have been traditionally difficult to teach. We discuss our recent experience with two such examples: the close-packed nature of an enzyme active site and the pH-induced conformational change of the influenza hemagglutinin protein during virus infection.

The technology now exists to construct physical models of proteins based on atomic coordinates of solved structures. We review here our recent experiences in using physical models to teach concepts of protein structure and function at both the high school and the undergraduate levels. At the high school level, physical models are used in a professional development program targeted to biology and chemistry teachers. This program has recently been expanded to include two student enrichment programs in which high school students participate in physical protein modeling activities. At the undergraduate level, we are currently exploring the usefulness of physical models in communicating concepts of protein structure and function that have been traditionally difficult to teach. We discuss our recent experience with two such examples: the close-packed nature of an enzyme active site and the pH-induced conformational change of the influenza hemagglutinin protein during virus infection.

We are developing a control program for a unique radiation therapy machine. The program is safety-critical, executes several concurrent tasks, and must meet real-time deadlines. Development employs both formal and traditional methods: we produce an informal specification in prose (supplemented by tables, diagrams and a few formulas) and a formal description in Z. The Z description includes an abstract level that expresses overall safety requirements and a concrete level that serves as a detailed design, where Z paragraphs correspond to data structures, functions and procedures in the code. We validate the Z texts against the prose specification by inspection. We derive most of the code from the Z texts by intuition and verify it by inspection but a small amount of code is derived and verified more formally. We have produced about 250 pages of informal specification and design description, about 1200 lines of Z and about 6000 lines of code. Experiences developing a large Z specification and writing the program are reported, and some errors we discovered and corrected are described.

This reportdescribesa new computercontrolsystemfor a radiationtherapy machinewith an isocentricgantryanda multileaf collimator. It discussesthe motivation andrationalefor someof the featuresanddevelopmentactivities, andreportsseveralmeasuresof development effort, performance, andquality, determinedafteralmosttwo yearsof operatingexperience. Notable featuresof the control systeminclude constructionbasedon standard(vendorindependent) hardwareandsoftwarecomponentsconnectedbyanetwork,asimpleandefficient userinterface,closeintegrationwith thetreatmentplanningsystem,automatedrecordkeeping for patientqualityassuranceandmachinemaintenance, andeaseof maintenanceandupgrading. Separationof control functionsfrom datamanagement functionsresultsin a control program which is small,fast,andfeasibleto analyzethoroughly. Choiceof featuresandinternaldesign wereinformedby fifteenyearsexperienceusingandmaintainingcomputercontrolledtherapy machines. Thedevelopmentmethodwaschosento ensureexceptionalsafety, reliability, andclinical acceptability. Much of thedetailedspecificationwasexpressedin formal (mathematical)notation. This formal specification(not theprosedescription)servedasthebasisfor mostcoding, testplanning,andsafetyanalysis.Testingandreviews weresupplementedby new automated analysesmethodsincluding theoremprovingandmodelchecking.