El uso de diferentes métodos y herramientas que asistan en la organización y el control de procesos, ha tomado relevancia debido a la necesidad constante de eficiencia por parte de la industria y a la adecuación de sus prácticas a las emergentes y novedosas técnicas de desarrollo y producción. Como producto de estas necesidades, diversos lenguajes para la descripción de procesos de negocios capturaron el interés tanto del sector productivo, para su aplicación en sus actividades, como así también del sector académico, con el fin de aportar conocimiento y generar nuevas herramientas para tal fin. Si bien la mayor parte de los lenguajes para la especificación de procesos de negocios son informales, existen algunos fundados en formalismos matemáticos. Esto brinda a estos lenguajes formales para procesos de negocios la eliminación de ambigüedades en la interpretación de especificaciones, y la posibilidad de realizar diferentes análisis formales, como chequeos de sanidad. Sin embargo, las alternativas existentes poseen en general limitaciones, o bien en poder expresivo, o, para las alternativas más expresivas, la imposibilidad de realizar algunas tareas de análisis automáticamente. En este trabajo presentamos un enfoque formal para la especificación y el análisis de procesos de negocios, que permite dar semántica a construcciones complejas de procesos de negocios, a la vez que admite el análisis de chequeos de sanidad usuales de manera automática mediante model checking. Más aún, nuestra propuesta abarca la posibilidad de que el usuario especifique y analice propiedades de interés acerca de las especificaciones, mediante lógicas temporales, un mecanismo con frecuencia ausente en los lenguajes existentes. Además del desarrollo de una semántica formal para un lenguaje de proceso de negocios sumamente expresivo, nuestro trabajo toma como base para la especificación de propiedades de procesos de negocios el uso de lógicas temporales. Identificamos algunos elementos que hacen particularmente complicada la expresión de algunos tipos de propiedades, en particular cuando las mismas demandan expresar repeticiones de eventos o tareas, y proponemos una lógica temporal que permite describir tales propiedades con mayor facilidad. Con el fin de no perder capacidad de análisis, desarrollamos traducciones que nos permiten capturar los elementos novedosos de esta lógica en términos de otros elementos, soportados por lógicas temporales tradicionales, con soporte de herramientas. Por otra parte, observamos la tendencia de los lenguajes de descripción de procesos de negocios a no tratar formalmente la descripción de los productos que manipulan. Tomamos un formalismo excepcional en este sentido, PPML, y definimos a partir del mismo un lenguaje de especificaciones, una semántica simplificada para el mismo, y una técnica de análisis de especificaciones basada en una caracterización de sus modelos en UPPAAL. Nuestro enfoque está claramente orientado a la producción de herramientas de soporte al proceso de especificación. Para los lenguajes tratados brindamos herramientas de especificación y análisis de procesos de negocios, como así también la posibilidad de construir descripciones de procesos de negocios a partir de las propiedades que los mismos deben cumplir. Estas tareas son evaluadas en este trabajo a través del desarrollo de casos de estudio tomados de la literatura del área, en lo que respecta a descripción de procesos y chequeos de sanidad de los mismos, y en base a variantes de estos casos en las cuales se enfatiza la necesidad de contar con propiedades descriptas por el usuario, y de dar más relevancia a la descripción de los productos manipulados por los procesos de negocios.