ABSTRACT. Timed automata (TA) are a widely used formalism to specify systems having temporal requirements. However, exactly specifying the system may be difficult, as the user may not know the exact clock constraints triggering state transitions. In this work, we assume the user already specified a TA, and (s)he wants to validate it against an oracle that can be queried for acceptance. Under the assumption that the user only wrote wrong guard transitions (i.e., the structure of the TA is correct), the search space for the correct TA can be represented by a Parametric Timed Automaton (PTA), i.e., a TA in which some constants are parametrized. The paper presents a process that (i) abstracts the initial (faulty) TA ta_init in a PTA pta; (ii) generates some test data (i.e., timed traces) from pta; (iii) assesses the correct evaluation of the traces with the oracle; (iv) uses the IMITATOR tool for synthesizing some constraints \phi on the the parameters of pta; (v) instantiate from \phi a TA ta_rep as final repaired model. Experiments show that the approach is able to partially repair the initial design of the user.

ABSTRACT. Shared-memory concurrent algorithms are well-known for being difficult to write, ill-adapted to test, and complex to prove. Wait-free concurrent objects are a subclass where a process is never prevented from progressing, whatever the other processes are doing (or not doing). Algorithms in this subclass are often non intuitive and among the most complex to prove. This paper presents the analysis and the proof of a wait-free concurrent algorithm that is used to rename processes. By its adaptive and non-blocking nature, the renaming algorithm exhibits a huge number of states and of transitions even with a small input set, and resists to test. Thus, a proof has been conducted in \TLA and verified with TLAPS, the \TLA Proof System. This algorithm is itself based on the assembly of wait-free concurrent objects, the splitters, that separate processes. With just two shared variables and three assignments, a splitter seems a simple object but it is not linearizable. To avoid explicitly in-lining it and dealing with its internal state, the proof of the renaming algorithm relies on replacing the splitter with a sequential specification that is proved correct with TLAPS and verified complete by model-checking on finite instances.

ABSTRACT. A common way to specify software properties is to associate a contract to each function, allowing the use of various techniques to assess (e.g. to prove or to test) that the implementation is valid with respect to these contracts. However, in practice, high-level properties are not always easily expressible through function contracts. Furthermore, such properties may span across multiple functions, making the specification task tedious, and its assessment difficult and error-prone, especially on large code bases. To address these issues, we propose a new specification mechanism called meta-properties. Meta-properties are enhanced global invariants specified for a set of functions, capable of expressing predicates on values of variables as well as memory related conditions (such as separation) and read or write access constraints. This paper gives a detailed presentation of meta-properties and their suport in a dedicated Frama-C plugin MetAcsl, and shows that they are automatically amenable to both deductive verification and testing. It is demonstrated by applying these techniques on two illustrative case studies.

ABSTRACT. Property-based testing requires the programmer to write suitable generators, i.e., programs that generate (possibly in a random way) input values for which the program under test should be run. However, the process of writing generators is quite a costly, error-prone activity. In the context of Property-Based Testing of Erlang programs, we propose an approach to relieve the programmer from the task of writing generators. Our approach allows the automatic generation of input values that satisfy a given specification. That generation is performed via the symbolic execution of the specification using constraint logic programming.