Estudos empíricos sobre a aplicabilidade de especificação formal de requisitos em projetos ágeis

Abstract

One of the characteristics of agile approaches is to use informal techniques for specifying requirements. The exclusive use of these techniques can cause some problems, such as ambiguous specifications, omission of information and interpretation mistakes. These problems are faced by a particular software development company, in Rio Grande do Sul, resulting in the unproductiveness of an agile team. A possible alternative is to adopt Formal Methods, which are, in resume, methods that use mathematical logic to formally specify requirements. It is possible find some papers in the literature that proposes the use of formal methods for requirements specification, as the Z notation and Vienna Development Method (VDM) with agile approach, as Extreme Programming (XP) and Scrum. Even identifying such initiatives, we realize the lack of papers that empirically evaluate the use of formal methods in agile projects. In this way, in this paper, we seek to investigate formal specification methods as an alternative to specify requirements in agile projects, providing evidence of this application to the partner company of this study. For that, different empirical studies were applied. Initially, we performed a systematic mapping to identify formal specification methods that are commonly used for developing systems in agile environments. Subsequently, we performed different empirical strategies to empirically evaluate the applicability of Formal Methods as a specification technique. The first empirical strategy consisted in conducting an opinion survey with acting agile software developers. In the second empirical strategy, we carried out an exploratory embedded case study in two software development companies to evaluate the applicability of Z notation for requirements specification. Finally, in the third strategy, we carried a controlled experiment in partner company of this study, where the productivity and quality impacts of the specifications were analyzed using the formal notation Z and Descriptive Use Case. The results of the first two strategies pointed out that the professionals’ perceptions tended to agree on some benefits in the use of formal specification in agile projects, for example: formal specification helps to make the requirements clearer and more complete. However, the main limiting factor in using these techniques is related to the developers’ preconceptions. The experiment results indicated that the use of Z notation improved the elicitation process, impacting on team productivity, as the use of Z notation resulted in the delivery of more software functionalities and software with better specification coverage by the agile team.