Formal validation and verification of atomic resolution microscope controland topography

This article presents a real case study in which both the control and topog raphic activities of a scanning tunnelling microscope (STM) are formally sp ecified. A method to obtain the executable formal specification is describe d, which implies the following tasks: 1) obtention of a functional model of the selected STM experiences; 2) discussion of the specification formalism and formal language to be used; 3) establishment of certain rules to conve rt the functional model to the chosen formal language; and 4) construction of the formal specification. The final specification has been used to valid ate the functional requirements against the behavior of the system. Previou sly, the internal consistency of the model had also been formally verified. Much has been learned through this project about the potential of formal t echniques to be accepted as a viable way of improving requirements analysis in electronic instrument systems and in related software development. This experience shows how starting from both a formal basis and a set of formal ly verified functional requirements is critical in producing a high-quality system design.