A formal support for incremental behavior specification in agile development
Anne-Lise Courbis, Thomas Lambolais, Hong-Viet Luong, Thanh-Liêm Phan, Christelle Urtado, Sylvain Vauttier · HAL (Le Centre pour la Communication Scientifique Directe) · 2012
Incremental development is now state of the practice. In-deed, it is promoted from the rational unified process to ag-ile development methods. Few methods however guide soft-ware developers and architects in doing so. For instance, no tool is proposed to verify the non-regression of function-alities, modeled as behavior specifications, between incre-ments. This work helps to incrementally specify software functionalities using UML state machines. It provides an on-the-fly evaluation of a specified behavior as compared to that of previous increments. The proposed contribution is based on two formally specified relations that are proved to preserve refinement when composed. Architects and de-velopers are free to choose their preferred behavior speci-fication strategy by iteratively applying them, so as to de-velop the required functionalities, having at each step the benefit of a formal non-regression checking to guide the global specification process. Our proposal is implemented in a proof-of-concept tool and illustrated by a didactic case-study.