City Research Online

Abstract

We present a static verification tool (SVT), a system that performs static verification on UML models composed of UML class and state machine diagrams. Additionally, the SVT allows the user to add extra behavior specification in the form of guards and effects by defining a small action language. UML models are checked against properties written in a special-purpose property language that allows the user to specify linear temporal logic formulas that explicitly reason about UML components. Thus, the SVT provides a strong foundation for the design of reliable systems and a step towards model-driven security.

Publication Type:	Conference or Workshop Item (Paper)
Additional Information:	© 2008 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other users, including reprinting/ republishing this material for advertising or promotional purposes, creating new collective works for resale or redistribution to servers or lists, or reuse of any copyrighted components of this work in other works.
Subjects:	Q Science > QA Mathematics > QA75 Electronic computers. Computer science
Departments:	School of Science & Technology > Computer Science

Export

Downloads