Android enfrenta una creciente amenaza de ataques de malware. Los pocos métodos formales de detección existentes tienen inconvenientes como modelado de código complejo, expresión incompleta e inexacta de propiedades familiares, y participación manual excesiva. Con este fin, este documento propone un método formal de detección, llamado DroidFDR, para la clasificación de malware de Android basado en procesos secuenciales de comunicación (CSP). En este método, el archivo APK de una aplicación se convierte en una representación fácil de analizar, Jimple, para modelar el comportamiento del código con CSP. El proceso que describe el comportamiento de una muestra se introduce en un verificador de modelos FDR para ser simplificado y verificado contra un proceso que se abstrae automáticamente del malware para expresar la propiedad de una familia. La muestra se clasifica detectando si tiene el comportamiento típico de alguna propiedad familiar. DroidFDR puede capturar las características de comportamiento del código malicioso como flujo de control, flujo de datos, llamadas a procedimientos y llamadas a API. Los resultados experimentales muestran que el método automatizado puede caracterizar los patrones de comportamiento de aplicaciones desde el nivel de estructura, con una alta precisión de clasificación familiar del 99.06% en comparación con otro método formal de detección.