As the complexity of software systems increases, so does the necessity to properly verify that safe behaviour will be observed. Testing is an essential, and often the only, strategy deployed for that purpose, but the complexity of modern systems renders the manual encoding of test cases impractical. As a consequence, several automated approaches to test generation have emerged, such as model-based (MBT), property-based (PBT), and specification-based testing (SBT).
These challenges are exacerbated when targeting distributed systems where components communicate asynchronously through message-passing, such as those complying to the OMG’s DDS standard (OMG, 2015). These systems are typically heterogeneous and built from third-party components, so system-level testing should act at the message-passing level, treating components as black-boxes. In this context, the behaviour to be analysed is of a dynamic nature, and testing procedures must take into consideration full traces of messages as inputs and outputs. This limits the feasibility of using unit tests beyond specific corner cases. PBT approaches are also ill-suited since they either focus on execution safety properties (such as null references or buffer overflows) or require the expected behaviour to be specified operationally. MBT approaches require modelling the system behaviour, which is often infeasible in systems of this nature.
SBT approaches can be used to tackle these issues. Here, the user is only expected to provide a single artefact, a high-level declarative specification of the expected behaviour of the system. In a dynamic context, these take the shape of temporal specifications, allowing the encoding of functional safety properties. Relevant trace inputs are automatically generated by inspecting the specifications, while validity is automatically tested by evaluating the specification against the output traces. However, previously proposed techniques of this nature are still affected by some issues. First, they are often based on logics with abstract time, such as linear temporal logic (LTL) (Tan et al., 2004; Michlmayr et al., 2006; Arcaini et al., 2013; Bloem et al., 2019; Narizzano et al., 2020), but most systems are expected to be tested for some timing constraints. Moreover, they often fail to provide a proper high-level interface that spares the developer from having to understand the underlying formalisms. Lastly, due to the extent of the search-space for timed trace test cases, such techniques must provide some kind of mechanisms to guide the input generation. Some techniques have been proposed in PBT, such as target-oriented (Löscher and Sagonas, 2017) and coverage-guided (Padhye et al., 2019) approaches, but they are ill-suited for heterogeneous and distributed systems.
In this paper we propose a novel SBT approach, depicted in Figure 1, based on trace schemas for message-oriented systems whose expected behaviour is specified in a high-level specification language. The users are only required to specify the architecture and the expected behaviour of the system under test (SUT), from which the input generator and the property monitors are derived. The language is based on well-known specification patterns (Dwyer et al., 1999), so that knowledge about the underlying formalisms or the implementation details of the SUT is not required. A trace schema is a sequence of message-passing conditions that are expanded by the trace generators into concrete message traces, which are automatically derived from the specified properties based on the used pattern. To restrict the search-space of the trace generator, the developer can specify additional properties over the communication channels using the same specification language, which the testing procedure uses to refine the schemas derived from the specification.
We evaluated our technique by implementing it over the most popular robotic middleware, the Robot Operating System (ROS) (Quigley et al., 2009). ROS provides a communication layer that allows robotic systems to be built from components communicating through a publisher-subscriber paradigm. This instantiation comprised the implementation of the specification language for ROS messages, a test generator for trace schemas, and the deployment of runtime monitors. It was integrated into HAROS (Santos et al., 2016; Santos et al., 2021), a framework for the development of high-assurance ROS software, which automates several tasks required for analysis and reporting. Evaluation shows that schemas automatically derived from specifications are effective in finding bugs related to message interleaving, and that providing additional assumptions further improves the results.
The rest of this paper is organized as follows. Section 2 presents an overview of the proposed approach. Section 3 presents the proposed property specification language, followed by the formalization of trace schemas, their derivation and associated trace generator in Section 4. Section 5 and Section 6 present the instantiation of the approach for ROS and the evaluation results. Section 7 presents and discusses related work. Lastly, Section 8 concludes the paper.
