Event Details
PVS Proof Patterns on UML Based Verification
Presenter: Yanguo Liu
Supervisor:
Date: Fri, September 13, 2002
Time: 13:00:00 - 14:00:00
Place: EOW 430
ABSTRACT
Abstract:
UML has been established as a practical notation to specify complex software systems and has been adopted by the OMG as an industry standard for object-oriented analysis and design. However, UML lacks of rigor and precision, UML specifications are often incomplete, inconsistent and ambiguous. For critical software systems, the inconsistencies and misconceptions arising from the inherent ambiguities of UML specifications are not only difficult and expensive to correct in the further phases of the software development, but also often lead to safety related failures. Therefore, the early checking of the UML specifications is crucial. In general, validation and Verification of UML diagram are hard to establish. Informal and semi-formal notations such as UML only support a very basic level of assurance, which just impose a structure on the specification that facilitates inspection by domain experts. The work carried in this thesis is part of ongoing effort to develop an automated reasoning framework for rigorous validation and verification of UML specifications. More specifically, we develop in this thesis some formal proof patterns that can be used to automatically verify a subset of UML specifications, which can lead to early detection of misconceptions and inconsistencies in the software development process; meanwhile, we present the implementation of the patterns in the Precise UML Development tool (PrUDE).
Free and open to the public