2012 Seventh International Conference on Availability, Reliability and Security (2008)
Mar. 4, 2008 to Mar. 7, 2008
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ARES.2008.194
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.
Model Checking, Spin, Static Verification, UML
Igor Siveroni, Andrea Zisman, George Spanoudakis, "Property Specification and Static Verification of UML Models", 2012 Seventh International Conference on Availability, Reliability and Security, vol. 00, no. , pp. 96-103, 2008, doi:10.1109/ARES.2008.194