Este artículo presenta una extensión de AspectZ con el objetivo de modelar los requerimientos del software que administra un sistema de fichas electrónicas de salud en Chile: SYSFIC 1.0. AspectZ es un lenguaje de especificación formal orientado a aspectos que preserva las características bases del lenguaje Z y que ayuda a encapsular incumbencias transversales del sistema en entidades separadas e independientes. La aplicación incluye el uso de diagramas con Lenguaje Unificado de Modelado (LUM) y un modelado formal del sistema con AspectZ. Se discuten, además, las principales características del paradigma de modelado orientado a aspectos, como la separación incumbencias y la solución de los problemas del código disperso y enmarañado. Los resultados de este trabajo muestran que la unión del modelado orientado a aspectos y de un método formal de desarrollo de software permite obtener soluciones más confiables para sistemas de información críticos como SYSFIC.