Leeme

Int J Softw Tools Technol Transfer (2004) 5: 124–139 / Digital Object Identifier (DOI) 10.1007/s10009-003-0133-6

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
e-mail:{david.lugato,celine.bigot,jean-pierre.gallois,sebastien.gerard,francois.terrier}@cea.fr, yannick.valot@wanadoo.fr

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, first, 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 specification

[pic]

1 Introduction

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 specification level. Indeed, thelater the defaults are detected, the greater the cost. Consequently, the development of techniques and tools able to efficiently help engineers who are in charge of elaborating the specification 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
a product.
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 specific 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 difficulty of analyzing
a system depends on the “quality” of the specification. 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 undefined semantic points[27], formal analysis requires respecting modeling rules and some UML specialization. Defining 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 specifications in order to:
– Prevent unexpected behaviors,
– Generate tests,
– Guarantee the fitness 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 specification
(black box testing). As it also generates a symbolic execu- tion tree,...