31 datasets found

International audience

International audience

Information systems have become ubiquitous and are used to handle each day more and more data. This data is increasingly confidential: strategic military or financial...

To ensure that a program will respect all its timing constraints we must be able to compute a safe estimation of its worst case execution time (WCET). However with the...

Over the last two decades, free and open source software has grown considerably. Distributions that started out with a few hundred packages now contain tens of...

This report proposes a design methodology for embedded real-time systems using a synchronous multi-clocked framework, which provides a well-defined mathematical model...

International audience

We show how to model filter functions on the co-inductive types of infinite streams in type theory. These functions are partial but the theory imposes total functions....

In this paper we present the formalisation of the library which is an implementation of rational numbers as binary sequences for both lazy and strict computation. We...

International audience

Access control allows one to specify a part of the security Policy of an IS (information system). An AC (access control) policy defines which conditions must old for...

This thesis belongs to the domain of software verification. The goalof verifying software is to ensure that an implementation, a program,satisfies the requirements,...

Interactive music systems coordinate in real-time an artificial perception of dynamics of human musicians with timely execution of machine reactions. As every human...

International audience

We are interested in analyzing the performability requirements of mobile communication systems by using model checking techniques. We model these systems using a...

International audience

The purpose of this thesis is to specify and prove programs with pointers, such as C programs, using refinement techniques. The proposed approach allows a compromise...

Safety is an important requirement for many modern systems. To ensure safety of complex critical systems, well-known safety analysis methods have been formalized. This...

This thesis aimed at providing a method to model, verify, and generate allocations of embedded systems functions on avionics resources. This method is based on the use...

International audience