Extended Abstract - CTDSI/CTCCSI 2021 - Study and definition of project attributes for selection of testing techniques for concurrent software

[Context:] The choice of testing technique to be adopted in a software testing project persists based on the tester's knowledge and often does not consider all of the testing techniques available in the industry or academia. Therefore, a characterization scheme was proposed and implemented in the SeleCTT tool, which is composed of a set of attributes that considers characteristics of concurrent programs, and they are used to calculate which of these attributes are suitable to guide the selection of testing techniques for a particular software project. [Objective:] The selection of the testing technique at each stage of a software's life cycle depends on many factors. Our work aims to help testers to select a better testing technique according to the characteristics of a software project, contributing to the selection of the most suitable testing technique to increase the efficiency of the software test execution process, which in turn influences the development and delivery of a more robust and quality product. Considering that the testing techniques are complementary, another goal is to allow a set of testing techniques to be selected and not just one. [Methodology:] To achieve this goal, a systematic mapping study was conducted to identify and analyze papers that represent the current state of the literature about testing techniques selection. We surveyed software testing practices carried in Brazil software companies and identified the testing practices to know and have an overview on the latest testing techniques, tools, and metrics used, the challenges faced by testers, and the selection testing technique process. [Results and Conclusions:] With this study, it is expected to specify project attributes that can be used to improve the existing recommendation system in the SeleCTT tool and propose ways of combining testing techniques, contributing to industry and academia, and bring insights into the context of testing techniques selection.

DICER 2.0: A New Model Checker for Data-Flow Errors of Concurrent Software Systems

Petri nets are widely used to model concurrent software systems. Currently, there are many different kinds of Petri net tools that can analyze system properties such as deadlocks, reachability and liveness. However, most tools are not suitable to analyze data-flow errors of concurrent systems because they do not formalize data information and lack efficient computing methods for analyzing data-flows. Especially when a concurrent system has so many concurrent data operations, these Petri net tools easily suffer from the state–space explosion problem and pseudo-states. To alleviate these problems, we develop a new model checker DICER 2.0. By using this tool, we can model the control-flows and data-flows of concurrent software systems. Moreover, the errors of data inconsistency can be detected based on the unfolding techniques, and some model-checking can be done via the guard-driven reachability graph (GRG). Furthermore, some case studies and experiments are done to show the effectiveness and advantage of our tool.

Models of concurrent program running in resource constrained environment

The paper considers concurrent program modeling using resource constrained automatons. Several software samples are considered: real time operational systems, video processing including object recognition, neural network inference, common linear systems solving methods for physical processes modeling. The source code annotating and automatic extraction of program resource constraints with the help of profiling software are considered, this enables the modeling for concurrent software behavior with minimal user assistance.

Verification of Cyberphysical Systems

The value of verification of cyberphysical systems depends on the relationship between the state of the software and the state of the physical system. This relationship can be complex because of the real-time nature and different timelines of the physical plant, the sensors and actuators, and the software that is almost always concurrent and distributed. In this paper, we study different ways to construct a transition system model for the distributed and concurrent software components of a CPS. The purpose of the transition system model is to enable model checking, an established and widely used verification technique. We describe a logical-time-based transition system model, which is commonly used for verifying programs written in synchronous languages, and derive the conditions under which such a model faithfully reflects physical states. When these conditions are not met (a common situation), a finer-grained event-based transition system model may be required. We propose an approach for formal verification of cyberphysical systems using Lingua Franca, a language designed for programming cyberphysical systems, and Rebeca, an actor-based language designed for model checking distributed event-driven systems. We focus on the cyber part and model a faithful interface to the physical part. Our method relies on the assumption that the alignment of different timelines during the execution of the system is the responsibility of the underlying platforms. We make those assumptions explicit and clear.