Validation and automatic test generation on UML models:
the AGATHA approach
David Lugato, C´eline Bigot, Yannick Valot, Jean-Pierre Gallois, S´ebastien G´erard, Fran¸cois Terrier
DTSI/SLA/LLSP – CEA Saclay-Bat. 451, F-91191, Gif sur Yvette Cedex, France
Published online: 19 February 2004 – © Springer-Verlag 2004
Abstract. UML-based methodologies take more and
more space in the software development domain. In add- ition, the need to validate applications as early as possible in the development cycle is now mandatory tosatisfy cost and time-to-market constraints. In this context, this paper describes, ﬁrst, how to bridge the gap between semiformal UML models and a formal technology ensur- ing test case generation. Second, the formal tool used to automatically generate test sequences, named AGATHA, is described in minute detail. Finally, this approach is illustrated throughout by a toy exampleof an elevator system.
Keywords: Automated test generation – Symbolic cal- culus – UML speciﬁcation
The economic goals of test generation are quite import- ant for the software industry. Manufacturers, ever seeking to increase productivity, need to avoid malfunctions as early as possible, that is, at the system speciﬁcation level. Indeed, thelater the defaults are detected, the greater the cost. Consequently, the development of techniques and tools able to eﬃciently help engineers who are in charge of elaborating the speciﬁcation constitutes a ma- jor challenge whose fallout concerns not only sectors of critical applications but also all those where poor concep- tion could be extremely harmful to the brandimage of
To take into account these observations, our labora- tory, the LLSP (Software for Process Safety Laboratory) of the CEA/LIST (Atomic Energy research Center / Sys- tems and Technologies Integration Laboratory), decided to implement formal techniques dedicated to test case
generation as early as possible in the development cycle
of software products: thisallows one to minimize costs. Moreover, automatization of test sequence synthesis be- comes mandatory to reduce test time and, consequently, development time.
The use of formal techniques within industrial pro jects remains limited to very speciﬁc pro jects and high-level experts. Two ma jor reasons that might explain these limitations are the lack of maturity of tools andthe relative intricacy of modeling languages that are often mathematics-based.
It is also well known that the diﬃculty of analyzing
a system depends on the “quality” of the speciﬁcation. That is why it is crucial to observe a few rules while specifying a system. Because general UML models still have several variations and open or undeﬁned semantic points, formal analysis requires respecting modeling rules and some UML specialization. Deﬁning these spe- cializations is one of the aims of the European pro ject AIT-WOODDES.1
Methods and tools have been developed to analyze systems using their speciﬁcations in order to:
– Prevent unexpected behaviors,
– Generate tests,
– Guarantee the ﬁtness of the implementation withre- gard to the model.
Tools such as AGATHA – “Atelier de G´en´eration Au- tomatique de Tests Holistiques pour Automates”, auto- matic holistic test generation studio for automata – [7,
20, 21, 25] generate test sets allowing one to validate that the software implementation conforms to its speciﬁcation
(black box testing). As it also generates a symbolic execu- tion tree,...