A strategy for searching for exploitable races is derived, implemented and evaluated. It aims at the detection of inconsistent behaviour due to irregularly interleaved instructions of concurrent threads. The search for internal races focuses on particular data flow patterns targeting the occurrence of internal races by enforcing different orders of reading and writing operations; it is guided by symbolic expressions of interleaved paths and constraint solving. The possibility of propagating internal races to system races is subsequently considered. An exemplifying application of the approach proposed illustrates its practicality.

This article compares security fuzzing approaches with respect to different characteristics commenting on their pro and cons concerning both their potential for exposing vulnerabilities and the expected effort required to do so. These preliminary considerations based on abstract reasoning and engineering judgement are subsequently confronted with experimental evaluations based on the application of three different fuzzing tools characterized by diverse data generation strategies on examples known to contain exploitable buffer overflows. Finally, an example inspired by a real-world application illustrates the importance of combining different fuzzing concepts in order to generate data in case fuzzing requires the generation of a plausible sequence of meaningful messages to be sent over a network to a software-based controller as well as the exploitation of a hidden vulnerability by its execution.

This article proposes an approach for testing the validity of specific branching time logical properties in arbitrary Extended Finite State Machines not allowing for a systematic and complete analysis by conventional model checking. To do so, a structural testing strategy based on formula-specific coverage criteria is proposed; the generation of test cases achieving such criteria can provide sufficient evidence to derive the validity of existential properties resp. sufficient counter-evidence to derive the invalidity of universal properties expressed in temporal logic.

This article proposes two heuristic approaches targeted at the optimized generation of test cases capable of triggering buffer overflows resp. underflows. Both testing techniques are based on guiding conditions statically derived by Integer Constraint Analysis. First experimental evaluations confirmed the superiority of local optimization algorithms over global ones.

This article proposes approaches supporting the analysis of code vulnerabilities based on overlapping machine instructions of variable length. For the purpose of focusing the search for potential malicious code it is suggested to apply first disassembling techniques allowing for a restriction of potentially exploitable memory space. Successively, testing based on heuristic optimization may be applied in order to evaluate dynamically the practicality of vulnerability exploitation.

Der quantitative Nachweis hoher Software-Zuverlässigkeitskenngrößen stellt eine ernsthafte Herausforderung für Entwickler und Gutachter dar. Die Anwendung statistischer Stichprobentheorie ist oft infolge des damit verbundenen enormen Testaufwands zum Scheitern verurteilt. Um die Praktikabilität dieses fundierten Ansatzes durch erhöhte Kosteneffizienz zu unterstützen, untersucht dieser Beitrag die Nutzbarkeit von Betriebserfahrung als Ersatz für prohibitiv unfangreiche Testphasen und illustriert deren erfolgreiche Erprobung an einer realen Anwendung aus dem Automobilbereich.

This article proposes a model-based approach to structural and statistical testing of cooperating and reconfigurable autonomous robots. Based on Coloured Petri Net models of cooperative behaviour, it summarizes the main results achieved in the context of two European ARTEMIS projects. As an example, a CPN model of autonomous and reconfigurable trolleys moving within a common environment is considered. The results allow for both a qualitative and a quantitative reliability analysis.

Based on considerations about the knowledge required to carry out different types of network attacks, this article discusses the logical demands posed to the attacker in order to circumvent the most classical checks for message trustworthiness. In view of the limitations of existing avoidance and detection techniques, the article stresses the need for targeted testing strategies aimed at the identification of exploitable code vulnerabilities. For this purpose, it proposes a paradigm for the generation of intelligent test cases meant to maximize the chances of anticipating challenging scenarios during early verification phases.

This article proposes a systematic approach to statistical testing for cooperative systems consisting of autonomous mobile agents. Based on Coloured Petri Net models of cooperative behaviour, it analyses different sources of randomness and defines an automatic test case generation procedure to derive cooperative scenarios according to a given operational profile. As an example, the approach is applied to a model of trolleys moving within a common environment. The results allow for quantitative reliability estimations of cooperative behaviour on the basis of statistical sampling theory.

This article presents a study on the benefits offered by Coloured Petri Nets in capturing and separating permanent and temporary behavioural information and on the systematic support they hereby provide to model-based design and testing of cyber-physical systems. In particular, it illustrates the application of CPN modelling to capture the behaviour of cooperative mobile robots and highlights their benefits in terms of compactness and scalability. Finally, the article reports on the applicability of test case generation algorithms supporting the coverage of the underlying CPN models with respect to different testing criteria.

In order to verify reconfiguration of interacting autonomous agents to be exclusively beneficial and never hazardous to cyber-physical systems, this article suggests a systematic approach based on incremental model-based testing and illustrates its application to cooperating mobile robots.

This article considers different automatic control paradigms allowing for varying degrees of agent cooperation and autonomy. In order to support the automatic verification of safety-relevant software controllers, it proposes the use of a generic testing pattern which can be instantiated such as to allow to optimize automatic test data generation with respect to the specific targets of the application considered and of the testing phase involved. The article reports on successful case studies carried out in different real-world environments.

This article proposes an approach to testing the cooperative behaviour of autonomous software-based agents with safety-relevant tasks. It includes the definition of different model-based testing criteria based on the coverage of Coloured Petri Net entities as well as the automatic generation of appropriate test cases. The multi-objective optimization problem considered addresses both the maximization of interaction coverage and the minimization of the amount of test cases required. The approach developed for its solution makes use of genetic algorithms. The resulting automatic test case generation process is presented in this article together with the experiences gained by applying it to cooperating autonomous forklifts.

This article presents some approaches to software reliability testing supporting high coverage of component or (sub-)system interactions while enabling the selection of test cases according to target and scenario-specific criteria. On the one hand, in order to allow for reliability assessment, automatic test generation approaches must support the provision of stochastically independent and operationally representative test data. On the other hand, crucial sub-system interactions must be tested as intensely as possible, with particular concern for the even distribution of testing effort or for the prioritization of domain-critical data. Depending on such application-specific peculiarities, different multi-objective optimization problems are approached by novel genetic algorithms, successively applied to an interaction-intensive example in order to illustrate their practicality.

This article presents a refined approach to quantitative software reliability assessment taking into account coverage of interactions and relevance of variables. For this purpose, an automatic test generation procedure is presented, based on a multi-objective optimization problem to be solved by genetic algorithms. The applicability of the resulting approach is finally illustrated via an interaction-intensive component-based example.

This article proposes a model-based testing approach for cooperating robotic systems. Coloured Petri Nets are used for capturing the high behavioural multiplicity of such systems in a compact and scalable way. For the purpose of systematically extracting test cases from underlying models, a number of coverage criteria based on different model entities is introduced. Finally, in order to ensure practicality, an incremental testing procedure based on increasingly refined coverage concepts is proposed.

This article proposes a novel approach to quantitative software reliability assessment ensuring high interplay coverage for software components and decentralized (sub-)systems. The generation of adequate test cases is based on the measurement of their operational representativeness, stochastic independence and interaction coverage. The underlying multi-objective optimization problem is solved by genetic algorithms. The resulting automatic test case generation supports the derivation of conservative reliability measures as well as high interaction coverage. The practicability of the approach developed is finally demonstrated in the light of an interaction-intensive example.

The use of autonomous systems, including cooperating agents, is indispensable in certain fields of application. Nevertheless, the verification of autonomous systems still represents a challenge due to lack of suitable modelling languages and verification techniques. To address these difficulties, different modelling languages allowing concurrency are compared. Coloured Petri Nets (CPNs) are further analysed and illustrated by means of an example modelling autonomous systems. Finally, some existing structural coverage concepts for Petri Nets are presented and extended by further criteria tailored to the characteristics of CPNs.