Li Tan, Zongyuan Yang, and Jinkui Xie
UML, situation calculus, Prolog, formal verification, automatic generation
From the viewpoint of software life cycle in Software Engineering, software architecture is the core of the structure and behavior of software. As software architecture design itself is a kind of modeling activity, how to verify the correctness of the standard modeling language of software architecture design, UML, is one big problem. This paper used an implementation of situation calculus, Prolog, as an underlying logic framework to formally describe a subset of UML diagrams, a graphic notation, and assign it an equivalent formal semantics automatically via our prototype tool, USCVSC. Then we verified possible syntax and semantic errors in UML in a Prolog interpreter, SWI-Prolog, after a definition of error types in UML. Finally, a goal was achieved that software designers could correct the design of UML diagrams prior to fixing bugs in code in the phase of test, which avoided unnecessary system overhead in the following phases of Software Engineering with the hope of enhancing the overall efficiency of the process of Software Engineering.
Important Links:
Go Back
