Considering predominant aspect-oriented software development (asymmetric AOSD), this paper discusses the application of aspect-oriented UML use case diagrams and formal language AspectZ to part of a classic AOSD case study, the Health-Watcher software system. In addition, this article proposes an extension of AspectZ to reach a new property for asymmetric AOSD which reacts after a schema successfully finishes, or not, showing messages for that situation, with an implicit join point; and a way for generalizing similar operations in a system using AspectZ. Thus, the main goal of this article is to show the application of and differences between asymmetric aspect-oriented formal and non-formal modeling, and to highlight potential advantages of aspect-oriented formal modeling over aspect-oriented non-formal modeling. First, this article describes the main concepts of the classic AOSD paradigm focusing on problems unsolved by previous forms of software development and resolved by AOSD. Second, by applying aspect-oriented UML use case diagrams, this paper highlights the use of dominion classes and extend-relationships. Considering the Health-Watcher case study and an asymmetric AOSD approach, this study found that using extend-relationships in UML use cases does not completely follow the basic principles of the prevailing AOSD approach in which a base element does not know about aspects, whereas an extending use case must explicitly know its extension points. Third, this article shows a formal modeling of the case study using AspectZ. Moreover, extensions of this aspect-oriented formal language are proposed and applied to the same case study to show their practical properties for modeling. These extensions allow showing success or error messages, and inserting or not a new item in a set of elements to take care of invalid situations.