Hubert Garavel, Frédéric Lang, Radu Mateescu et al.
CADP is a comprehensive toolbox implementing results of concurrency theory. This paper addresses the question, whether CADP qualifies as an applicable formal method, based on the experience of the authors and feedback reported by users.
Radu Mateescu, Wendelin Serwe, Aymane Bouzafour et al.
Asynchronous circuits have several advantages for security applications, in particular their good resistance to attacks. In this paper, we report on experiments with modeling, at various abstraction levels, a patented asynchronous circuit for detecting physical attacks, such as cutting wires or producing short-circuits.
Josip Bozic, Lina Marsso, Radu Mateescu et al.
Testing of network services represents one of the biggest challenges in cyber security. Because new vulnerabilities are detected on a regular basis, more research is needed. These faults have their roots in the software development cycle or because of intrinsic leaks in the system specification. Conformance testing checks whether a system behaves according to its specification. Here model-based testing provides several methods for automated detection of shortcomings. The formal specification of a system behavior represents the starting point of the testing process. In this paper, a widely used cryptographic protocol is specified and tested for conformance with a test execution framework. The first empirical results are presented and discussed.