Formal modeling and test generation automation with Use Case Maps and LOTOS

This thesis addresses the problem of formal modelling and test generation, from system requirements represented in the form of Use Case Maps. In the first part of our thesis, we present an existent development methodology based on Use Case Maps for the design of the requirements and on LOTOS and SDL for the formal modeling of telecommunication systems. We follow this methodology for the formal specification and validation of a telephony system using LOTOS. In the second part of the thesis, we develop a method for the automatic generation of LOTOS scenarios from Use Case Maps called Ucm2LotosTests. The obtained scenarios can be used for the verification of the LOTOS specification built from the same Use Case Maps and for conformance testing purposes at the implementation stage. Finally, we propose a development methodology based on Use Case Maps for the design of the requirements and on LOTOS for the formal modeling of the system. In addition, this methodology offers a fast test generation process; it proposes the use of Ucm2LotosTests for the automatic generation of LOTOS scenarios from requirements in UCM and of TGV for the automatic generation of TTCN test suites from LOTOS. The methodology is illustrated with a case study which is a telephony system providing the basic call feature.