Specifying and verifying UML activity diagrams via graph transformations