The application of abstract state machines in software engineering

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.