TABLE OF CONTENTS REBECA P.D AZ REDONDO, JOS J.PAZOS ARIAS and ANA FERN NDEZ VILAS
Departamento de Enxe er a Telem tica, Universidade de Vigo, Spain
{rebeca,jose,avilas}@det.uvigo.es
Abstract. In a totally formalized, iterative and incremental software process, each iteration usually implies identifying new requirements, adding them to the current model of the system, rechecking the consistency and, in many cases, modifying the model to satisfy all the functional requirements. In this context, the ARIFS (pronounced ah-reefs , A pproximate R etrieval of I ncomplete and F ormal S pecifications) methodology provides a suitable reuse environment to classify, retrieve and adapt formal and incomplete requirements specifications and to reuse the formal verification results linked to them. This chapter focuses on applying this methodology to a case study, where the main goal is developing the components involved in a communication protocol. In this example application, we are able to avoid formal proofs in the consistency checking process and synthesis tasks to model the components.
As the complexity of specifying the requirements of large and complex systems is usually excessive for a one-step design, current software engineering practice addresses this problem by the use of iterative and incremental development techniques. Besides that, it is possible to obtain the well-known advantages of formal methods by integrating different kinds of formal techniques in this style of life cycles. Finally, including software reuse in this type of totally formalized, iterative and incremental software process approaches can increase the efficiency of developing large and complex systems, specially...
