El lenguaje de modelado unificado (UML) es un estándar industrial de facto para el modelado de sistemas. Consiste en un conjunto de notaciones gráficas (también conocidas como diagramas) y se ha utilizado ampliamente en muchas aplicaciones industriales. Aunque la naturaleza gráfica de UML es atractiva para los desarrolladores de sistemas, la documentación oficial de UML no proporciona semántica formal para los diagramas UML. Esto hace que UML no sea adecuado para la verificación formal y, por lo tanto, limitado cuando se trata del desarrollo de sistemas críticos para la seguridad donde los fallos pueden causar daños a personas, propiedades o al medio ambiente. El diagrama de actividad UML es una notación gráfica UML importante, que es efectiva para modelar los aspectos dinámicos de un sistema. Este documento propone una semántica formal para los diagramas de actividad UML basada en el cálculo de ambientes conscientes del contexto (CCA). Se propone un algoritmo (función semántica) que mapea cualquier diagrama de actividad a un proceso en CCA, que describe los comportamientos del diagrama de actividad UML. Este proceso puede ser ejecutado y verificado formalmente utilizando la herramienta de simulación CCA ccaPL y la herramienta de verificación en tiempo de ejecución CCA ccaRV. Por lo tanto, se pueden detectar y corregir fallos de diseño temprano durante el ciclo de vida del desarrollo del sistema. La pragmática del enfoque propuesto se demuestra utilizando un estudio de caso en comercio electrónico.