Improving software development efficiency within the W-CDMA application area by use of formal methods for verification

Ericsson Erisoft has recently started up a new department for the development of the software for a W-CDMA Base Station Transceiver. They would like to make the development process more efficient, and especially in the verification area. This is supposed to be done with the help of formal methods. TTCN is the testing language used, and first an inventory is made of the available tools on the market for TTCN. This to find out if there exists a better tool than the one used today. Some tool for different usages are recommended. The main goal of this master thesis is to evaluate and perhaps construct methods and tools, especially for verification, and to try a selected method together with the other development methods and tools that are used today. Then a comparison of the new method with the current method will be done. The method selected in this master thesis is to make the test specifications in MSCs and SDL diagrams. Some comparisons are made with another examined method, to write the test specifications directly in TTCN. The tool Autolink from Telelogic is used to transform the test specifications in MSC and SDL into TTCN test cases. The TTCN test cases is executed successfully on a hardware card of the base station. Some advantages and disadvantages are pointed out. The new method is more efficient and is therefore recommended.Validerat; 20101217 (root