<p> The Haskell programming language uses type classes to deal with overloading. Functions are overloaded by defining some types to be instances of a class. A meaningful instance should satisfy the invariants of the class.</p> <p> In this thesis we present one method to validate the type instances of classes informally, and another one to verify them in a formal way.</p> <p> The first method uses QuickCheck, which is an automatic testing tool for Haskell programs. We introduce how to specify the properties of type classes in QuickCheck by some examples, and I also present testing for Haskell standard types and classes.</p> <p> The second method I adopted uses the theorem prover Isabelle/HOL. To facilitate the usage of Isabelle/HOL for Haskell programmers, I define a set of translation rules from Haskell programs to Isabelle/HOL, and design a simple automatic translating tool based on those rules. Logical differences between Haskell and Isabelle/HOL need to be considered in the translation. For example Isabelle/HOL is not suitable to describe the semantics of lazy evaluation and of Haskell functions that are non-terminating. I also prove some type instances to illustrate how the properties are verified in Isabelle/HOL.</p> / Thesis / Master of Applied Science (MASc)

<p>Traffic and Feature SW is a department based in Kista. At this department the main processor software, or MPSW in short, in Ericssons Radio Base Stations is tested prior to integration of new releases. Traffic and Feature SW, also called MPSW in this thesis, works closely with another department of Ericsson called RBS System I&V which tests the same software but for complete RBS nodes. MPSW uses black- and greybox scripted testing in regression suites that are executed on a daily basis. These regression suites are separated into different subsets of functionality that maps to the capabilities of the Radio Base Station software. The authors of this thesis has performed an implementation of automated test cases for a subset of the Radio Base Station software using an automated software tool called QuickCheck. These test cases were successfully integrated into the test framework and were able to find several issues with the main processor software and its subsystems in the Radio Base Station. The commissioner of this thesis have plans to further integrate the QuickCheck tool into the test framework, possibly automating test cases for several subsets of the Radio Base Station software. The authors have therefore analysed and put forth metrics that compares the testing of the Radio Base Station software using QuickCheck with the conventional regression test cases. These metrics covers areas such as the cost related to and the inherent capabilities of QuickCheck. The evaluation of these metrics was performed by the authors to give the commissioner decisive information. These evaluations showed that QuickCheck was able to generate complex message stuctures in complex sequences. QuickCheck was also able to shrink both the content of these messages and the length of the sequences of messages to be able to provide a minimal counterexample when a fault was discovered. The only metric that QuickCheck failed to support was to inherit functionality to support the handling of statistics from executions.</p> / <p>Traffic and Feature SW is a department based in Kista. At this department the main processor software, or MPSW in short, in Ericssons Radio Base Stations is tested prior to integration of new releases. Traffic and Feature SW, also called MPSW in this thesis, works closely with another department of Ericsson called RBS System I&V which tests the same software but for complete RBS nodes. MPSW uses black- and greybox scripted testing in regression suites that are executed on a daily basis. These regression suites are separated into different subsets of functionality that maps to the capabilities of the Radio Base Station software. The authors of this thesis has performed an implementation of automated test cases for a subset of the Radio Base Station software using an automated software tool called QuickCheck. These test cases were successfully integrated into the test framework and were able to find several issues with the main processor software and its subsystems in the Radio Base Station. The commissioner of this thesis have plans to further integrate the QuickCheck tool into the test framework, possibly automating test cases for several subsets of the Radio Base Station software. The authors have therefore analysed and put forth metrics that compares the testing of the Radio Base Station software using QuickCheck with the conventional regression test cases. These metrics covers areas such as the cost related to and the inherent capabilities of QuickCheck. The evaluation of these metrics was performed by the authors to give the commissioner decisive information. These evaluations showed that QuickCheck was able to generate complex message stuctures in complex sequences. QuickCheck was also able to shrink both the content of these messages and the length of the sequences of messages to be able to provide a minimal counterexample when a fault was discovered. The only metric that QuickCheck failed to support was to inherit functionality to support the handling of statistics from executions.</p>

Traffic and Feature SW is a department based in Kista. At this department the main processor software, or MPSW in short, in Ericssons Radio Base Stations is tested prior to integration of new releases. Traffic and Feature SW, also called MPSW in this thesis, works closely with another department of Ericsson called RBS System I&amp;V which tests the same software but for complete RBS nodes. MPSW uses black- and greybox scripted testing in regression suites that are executed on a daily basis. These regression suites are separated into different subsets of functionality that maps to the capabilities of the Radio Base Station software. The authors of this thesis has performed an implementation of automated test cases for a subset of the Radio Base Station software using an automated software tool called QuickCheck. These test cases were successfully integrated into the test framework and were able to find several issues with the main processor software and its subsystems in the Radio Base Station. The commissioner of this thesis have plans to further integrate the QuickCheck tool into the test framework, possibly automating test cases for several subsets of the Radio Base Station software. The authors have therefore analysed and put forth metrics that compares the testing of the Radio Base Station software using QuickCheck with the conventional regression test cases. These metrics covers areas such as the cost related to and the inherent capabilities of QuickCheck. The evaluation of these metrics was performed by the authors to give the commissioner decisive information. These evaluations showed that QuickCheck was able to generate complex message stuctures in complex sequences. QuickCheck was also able to shrink both the content of these messages and the length of the sequences of messages to be able to provide a minimal counterexample when a fault was discovered. The only metric that QuickCheck failed to support was to inherit functionality to support the handling of statistics from executions. / Traffic and Feature SW is a department based in Kista. At this department the main processor software, or MPSW in short, in Ericssons Radio Base Stations is tested prior to integration of new releases. Traffic and Feature SW, also called MPSW in this thesis, works closely with another department of Ericsson called RBS System I&amp;V which tests the same software but for complete RBS nodes. MPSW uses black- and greybox scripted testing in regression suites that are executed on a daily basis. These regression suites are separated into different subsets of functionality that maps to the capabilities of the Radio Base Station software. The authors of this thesis has performed an implementation of automated test cases for a subset of the Radio Base Station software using an automated software tool called QuickCheck. These test cases were successfully integrated into the test framework and were able to find several issues with the main processor software and its subsystems in the Radio Base Station. The commissioner of this thesis have plans to further integrate the QuickCheck tool into the test framework, possibly automating test cases for several subsets of the Radio Base Station software. The authors have therefore analysed and put forth metrics that compares the testing of the Radio Base Station software using QuickCheck with the conventional regression test cases. These metrics covers areas such as the cost related to and the inherent capabilities of QuickCheck. The evaluation of these metrics was performed by the authors to give the commissioner decisive information. These evaluations showed that QuickCheck was able to generate complex message stuctures in complex sequences. QuickCheck was also able to shrink both the content of these messages and the length of the sequences of messages to be able to provide a minimal counterexample when a fault was discovered. The only metric that QuickCheck failed to support was to inherit functionality to support the handling of statistics from executions.

El testing del software es una tarea crucial y a la vez muy desafiante dentro del proceso de desarrollo de software. El testing permite encontrar errores y problemas del software contra la especificación del mismo y cumple un rol fundamental en el aseguramiento de la calidad del producto. Entre los tipos de pruebas que se pueden realizar al software están las pruebas de unidad, carga, integración y funcionales. Cada una de ellas tiene distintos objetivos y son realizadas en diferentes etapas del desarrollo del software. En el primer tipo mencionado, se desarrollan pruebas a componentes individuales de un sistema de software. Los desarrolladores especifican y codifican pruebas para cubrir todos o al menos una parte significativa de los posibles estados/configuraciones del artefacto o unidad de software, para simular el entorno del componente y descubrir la presencia de errores o “bugs”. Dado que escribir todas esas pruebas de forma manual es costoso, las pruebas de unidad son generalmente realizadas de manera ineficiente o simplemente dejadas de lado. El panorama es aún peor, más allá del esfuerzo, porque el testing no puede ser usado para probar la usencia de errores en el software sino tan solo la presencia. Por eso es necesario atacar el problema desde diferentes enfoques, cada uno teniendo sus fortalezas y ventajas. Actualmente existen muchas técnicas para hacer testing de software, y la mayoría de ellos se basan en la automatización de pasos o caminos de ejecución, con valores fijos o componentes predefinidos (hard-coded) o estáticos, y condiciones específicas. En este trabajo de maestría, se presenta un enfoque para pruebas de unidad en la programación orientada a objetos, basado en la generación de objetos de manera aleatoria. El fundamento básico de este enfoque propuesto es el testing aleatorio. También se presenta una herramienta de testing de unidad que usa el enfoque dicho, y que fue escrita en un lenguaje orientado a objetos de amplia difusión. El testing aleatorio (RT o random testing) como técnica no es nueva. Tampoco lo es la generación de valores aleatorios para pruebas. En el paradigma funcional, existe una herramienta muy conocida para probar especificaciones sobre funciones llamada QuickCheck. Ésta herramienta (escrita en Haskell) y sus ideas subyacentes son usadas como fundamento para la herramienta creada en este trabajo. La herramienta desarrollada en el presente trabajo cubre además características que existen en el paradigma orientado a objetos de manera inherente, tales como el estado de los objetos (en particular los objetos singleton con estado), clases abstractas e interfaces, que no existen en la programación funcional pura. La constribución de este trabajo de maestría es la presentación de una forma alternativa de realizar tests de unidad en la programación orientada a objetos (POO), basada en un trabajo anterior para el paradigma funcional. También se presenta una herramienta llamada YAQC4J que plasma esas ideas en un lenguaje orientado a objetos de amplia difusión. Finalmente se incluyen ejemplos que ilustran el uso de la herramienta, y se presenta una comparación con herramientas existentes que han intentado implementar el enfoque de testing. Este trabajo está dirigido a los desarrolladores de software interesados en conocer soluciones alternativas para el testing de unidad, y al mismo tiempo una forma complementaria a las ya existentes para pruebas de unidad.