Using UML Models and Formal Verification in Model-Based Testing

2010 ◽  
Author(s):  
Qaisar A. Malik ◽  
Dragos Truscan ◽  
Johan Lilius
Keyword(s):  
Formal Verification ◽  
Model Based ◽  
Model Based Testing ◽  
Uml Models

scholarly journals Automatic Generation of Test Cases from UML Models

2018 ◽  
Vol 21 (1) ◽  
Author(s):  
Constanza Pérez ◽  
Beatriz Marín
Keyword(s):  
Conceptual Models ◽  
State Transition ◽  
Automatic Generation ◽  
Test Cases ◽  
Design And Implementation ◽  
Model Based ◽  
Model Based Testing ◽  
The Cost ◽  
Early Phases ◽  
Uml Models

[Context] The growing demand for high-quality software has caused the industry to incorporate processes to enable them to comply with these standards, but increasing the cost of development. A strategy to reduce this cost is to incorporate quality evaluations from early stages of software development. A technique that facilitates this evaluation is the model-based testing, which allows to generate test cases at early phases using as input the conceptual models of the system. [Objective] In this paper, we introduce TCGen, a tool that enables the automatic generation of abstract test cases starting from UML conceptual models. [Method] The design and implementation of TCGen, a technique that applies different testing criteria to class diagrams and state transition diagrams to generates test cases, is presented as a model-based testing approach. To do that, TCGen uses UML models, which are widely used at industry and a set of algorithms that recognize the concepts in the models in order to generate abstract test cases. [Results] An exploratory experimental evaluation has been performed to compare the TCGen tool with traditional testing. [Conclusions] Even though the exploratory evaluation shows promising results, it is necessary to perform more empirical evaluations in order to generalize the results. Abstract (in Spanish): [Contexto] La creciente demanda de software de alta calidad ha provocado que la industria incorpore procesos para permitirles cumplir con estos estándares, pero aumentando el costo del desarrollo. Una estrategia para reducir este costo es incorporar evaluaciones de calidad desde las primeras etapas del desarrollo del software. Una técnica que facilita esta evaluación es la prueba basada en modelos, que permite generar casos de prueba en fases tempranas utilizando como entrada los modelos conceptuales del sistema. [Objetivo] En este artículo, presentamos TCGen, una herramienta que permite la generación automática de casos de pruebas abstractas a partir de modelos conceptuales UML. [Método] El diseño e implementación de TCGen, una técnica que aplica diferentes criterios de prueba a los diagramas de clases y diagramas de transición de estados para generar casos de prueba, se presenta como un enfoque de prueba basado en modelos. Para hacer eso, TCGen utiliza modelos UML, que son ampliamente utilizados en la industria y un conjunto de algoritmos que reconocen los conceptos en los modelos para generar casos de prueba abstractos. [Resultados] Se realizó una evaluación experimental exploratoria para comparar la herramienta TCGen con las pruebas tradicionales. [Conclusiones] Aunque la evaluación exploratoria muestra resultados prometedores, es necesario realizar más evaluaciones empíricas para generalizar los resultados.  

scholarly journals Verification and testing of safety-critical airborne systems: A model-based methodology

2020 ◽  
Vol 17 (1) ◽  
pp. 271-292 ◽  
Author(s):  
Mounia Elqortobi ◽  
Warda El-Khouly ◽  
Amine Rahj ◽  
Jamal Bentahar ◽  
Rachida Dssouli
Keyword(s):  
Formal Verification ◽  
Software Verification ◽  
Regulatory Compliance ◽  
Integrate Model ◽  
Safety Critical ◽  
Model Based ◽  
Development Cycle ◽  
Model Based Testing ◽  
Implementation Level ◽  
Cross Fertilization

In this paper, we address the issues of safety-critical software verification and testing that are key requirements for achieving DO-178C and DO- 331 regulatory compliance for airborne systems. Formal verification and testing are considered two different activities within airborne standards and they belong to two different levels in the avionics software development cycle. The objective is to integrate model-based verification and model-based testing within a single framework and to capture the benefits of their cross-fertilization. This is achieved by proposing a new methodology for the verification and testing of parallel communicating agents based on formal models. In this work, properties are extracted from requirements and formally verified at the design level, while the verified properties are propagated to the implementation level and checked via testing. The contributions of this paper are a methodology that integrates verification and testing, formal verification of some safety critical software properties, and a testing method for Modified Condition/Decision Coverage (MC/DC). The results of formal verification and testing can be used as evidence for avionics software certification.

scholarly journals A Comparative Evaluation of approaches for Model Testability

2013 ◽  
Vol 9 (1) ◽  
pp. 948-955
Author(s):  
Pourya Nikfard ◽  
Suhaimi Bin Ibrahim ◽  
Babak Darvish Rohani ◽  
Harihodin Bin Selamat ◽  
Mohd Nazri Mahrin
Keyword(s):  
Software Engineering ◽  
Software Design ◽  
Comparative Evaluation ◽  
Design For Testability ◽  
Test Coverage ◽  
Design Models ◽  
Model Based ◽  
Model Based Testing ◽  
Uml Models

Design for testability is a very importantissue in software engineering. It becomes crucial in the case of Model Based Testing where models are generally not tested before using as input of Model Based Testing. The quality of design models (e.g.; UML models), has received less attention, which are main artifacts of any software design. Testability tends to make the validation phase more efficient in exposing faults during testing, and consequently to increase quality of the end-product to meet required specifications. Testability modeling has been researched for many years. Unfortunately, the modeling of a design for testability is often performed after the design is complete. This limits the functional use of the testability model to determining what level of test coverage is available in the design. This information may be useful to help assess whether a product meets the target requirement to achieve a desired level of test coverage, but has little pro-active effect on making the design more testable.

scholarly journals An Evaluation for Model Testability approaches

2013 ◽  
Vol 9 (1) ◽  
pp. 938-947 ◽  
Author(s):  
Pourya Nikfard ◽  
Suhaimi Bin Ibrahim ◽  
Babak Darvish Rohani ◽  
Harihodin Bin Selamat ◽  
Mohd Nazri Mahrin
Keyword(s):  
Software Engineering ◽  
Software Design ◽  
Design For Testability ◽  
Test Coverage ◽  
Design Models ◽  
Validation Phase ◽  
Model Based ◽  
Model Based Testing ◽  
Uml Models

Design for testability is a very important issue in software engineering. It becomes crucial in the case of Model Based Testing where models are generally not tested before using as input of Model Based Testing. The quality of design models (e.g.; UML models), has received less attention, which are main artifacts of any software design. Testability tends to make the validation phase more efficient in exposing faults during testing, and consequently to increase quality of the end-product to meet required specifications. Testability modeling has been researched for many years. Unfortunately, the modeling of a design for testability is often performed after the design is complete. This limits the functional use of the testability model to determining what level of test coverage is available in the design. This information may be useful to help assess whether a product meets the target requirement to achieve a desired level of test coverage, but has little proactive effect on making the design more testable.

Model-Based Testing for Web Applications

2011 ◽  
Vol 34 (6) ◽  
pp. 1012-1028 ◽  
Author(s):  
Huai-Kou MIAO ◽  
Sheng-Bo CHEN ◽  
Hong-Wei ZENG
Keyword(s):  
Web Applications ◽  
Model Based ◽  
Model Based Testing
Sign in / Sign up

Export Citation Format

Share Document