The application of abstract state machines in software engineering.
Wuwei Shen · Deep Blue (University of Michigan) · 2001
In this thesis we present two applications of Abstract State Machines in software engineering. As a formal method, Abstract State Machines have played an important role in software engineering. The first application of Abstract State Machines in this thesis is a static and dynamic semantics for C. Although ASMs have been used to give dynamic semantics for C, we present both static and dynamic semantics for C using an ASM tool called Montage. Because Montage supports ASM execution, any C program can be executed after we have given both static and dynamic semantics for C. As the second application of ASMs in software engineering, we apply ASMs to the Unified Modeling Language, which has become a standard language in software development. UML is a rich language which includes many diagrams to describe different aspects of a software system. In order to help UML users find errors in their early design, we present a semantic model for some several important diagrams in UML using ASMs. In order to help software designers find errors in the static aspect of a UML model, we present an ASM model for a class diagram, object diagram and the Object Constraint Language (OCL) in this thesis. A software designer can use this tool to find syntax errors in a UML model and check whether some important states are included in a UML model. On the other hand, an ASM model for a state machine in UML is also given in this thesis. Based on this ASM model, we can verify properties and find some errors in a UML model using the ASM model checker.