Throughout the last few decades, researchers and practitioners are showing more and more interest in using formal methods in order to predict and prevent software failures in robotic and autonomous systems. However, the applicability of formal methods to such systems is limited due to several factors. For instance, robotic specifications are often non-formal which makes their formalization hard and error prone, and their translation into formal models ad-hoc and non automatic. Furthermore, the complexity and size of robotic applications lead most often to scalability issues with exhaustive techniques such as model checking. In this paper, we investigate the use of runtime verification as an alternative to model checking for the rigorous verification of large robotic systems. To do so, we first develop a sound and automatic translation from the robotic framework GenoM3 to the real-time version of the BIP formal language. Then, we apply the translation to a real-world case study the formal models of which do not scale with model checking, and use the BIP Engine to execute the generated BIP model, verify properties online, and adequately react to their possible violation. The experiments are carried out on a real Robotnik robot and show the efficiency of our approach in verifying timed properties, that is when the amount of time separating events is important.

The design and the implementation of distributed real-time systems has always been a challenging task. A central question being how to efficiently coordinate parallel activities by means of point-to-point communication so as to keep global consistency while meeting timing constraints. In the domain of safety critical applications, system predictability allows to pre-compute optimal scheduling policies. In this paper, we consider a larger class of systems represented as compositions of timed automata subject to multiparty interactions, for which an implementation method for distributed platforms and based on intermediate model transformation already exists. To improve this approach, we developed specific static analysis techniques that, combined with local and global knowledge of the system, checks particular conditions that enables to decrease the number of messages exchanged in the system for executing each interaction, as well as to remove unnecessary scheduling overhead in some cases.

Distributed implementation of real-time systems has always been a challenging task. The coordination of components executing on a distributed platform has to be ensured by complex communication protocols taking into account their timing constraints. We propose a novel method for distributed implementation of the application software formally expressed in Behavior, Interaction, Priority (BIP). A BIP model consists of a set of components, subject to timing constraints, and synchronizing through multiparty interactions. The proposed method transforms BIP models into Send/Receive BIP models that operate using asynchronous message passing. Send/Receive BIP models include additional components called schedulers that observe atomic components states. Based on these observations, the schedulers are required to plan as soon as possible the execution of interactions. We propose a method that optimizes the number of observed components, and thus reduces the number of exchanged messages.

The correct and efficient implementation of general real-time applications remains very much an open problem. A key issue is meeting timing constraints whose satisfaction depends on features of the execution platform, in particular its speed. Existing rigorous implementation techniques are applicable to specific classes of systems, for example, with periodic tasks or time-deterministic systems. We present a general model-based implementation method for real-time systems based on the use of two models: • An abstract model representing the behaviour of real-time software as a timed automaton, which describes user-defined platform-independent timing constraints. Its transitions are timeless and correspond to the execution of statements of the real-time software. • A physical model representing the behaviour of the real-time software running on a given platform. It is obtained by assigning execution times to the transitions of the abstract model. A necessary condition for implementability is time-safety, that is, any (timed) execution sequence of the physical model is also an execution sequence of the abstract model. Time-safety simply means that the platform is fast enough to meet the timing requirements. As execution times of actions are not known exactly, time-safety is checked for the worst-case execution times of actions by making an assumption of time-robustness: time-safety is preserved when the speed of the execution platform increases. We show that, as a rule, physical models are not time-robust, and that time-determinism is a sufficient condition for time-robustness. For a given piece of real-time software and an execution platform corresponding to a time-robust model, we define an execution engine that coordinates the execution of the application software so that it meets its timing constraints. Furthermore, in the case of non-robustness, the execution engine can detect violations of time-safety and stop execution. We have implemented the execution engine for BIP programs with real-time constraints and validated the implementation method for two case studies. The experimental results for a module of a robotic application show that the CPU utilisation and the size of the model are reduced compared with existing implementations. The experimental results for an adaptive video encoder also show that a lack of time-robustness may seriously degrade the performance for increasing platform execution speed.

Correct and efficient implementation of general real-time applications remains by far an open problem. A key issue is meeting timing constraints whose satisfaction depends on features of the execution platform, in particular its speed. Existing rigorous implementation techniques are applicable to specific classes of systems e.g. with periodic tasks, time deterministic systems.

We present a method for fine grain QoS control of multimedia applications. This method takes as input an application software composed of actions. The execution times are unknown increasing functions of quality level parameters. Our method allows the construction of a quality manager which computes adequate action quality levels, so as to meet QoS requirements for a given platform. These include requirements for safety (action deadlines are met) as well as optimality (maximization and smoothness of quality levels). In this paper, we use learning techniques for computation of quality management policies. Given input parameters of the actions, a neural network is used to refine online pre-computed average execution times. Using refine average execution times allows a better control of the application, which leads to a reduction of fluctuations of CPU load. We present experimental results including the implementation of the method and benchmarks for an MPEG4 video encoder.

We present a quality management method for multimedia applications. The method takes as input an application software composed of actions. The execution times of actions are unknown increasing junctions of quality level parameters. The method allows the construction of a quality manager which computes adequate action quality levels so as to meet QoS requirements for a given platform. These include deadlines for the actions as well as quality maximization and smoothness. We extend and improve results of a previous paper by focusing on the reduction of overhead due to quality management. We propose a symbolic quality management method using speed diagrams, a representation of the system's dynamics. Instead of numerically computing a quality level for each action, the quality manager changes action quality levels based on the knowledge of constraints characterizing control relaxation regions. These are sets of states in which quality management for a given number of steps can be relaxed without degrading quality. We provide experimental results for quality management of an MPEG encoder, in particular performance benchmarks for both numeric and symbolic quality management.

We propose a method for fine grain QoS control of dataflow applications. We assume that the application software is described as the composition of actions (C-functions) with quality level parameters. The method allows a QoS controller to be computed from this description, and also average execution times, worst case execution times and deadlines for its actions. The controller computes dynamically feasible schedules and quality assignments for their actions. Furthermore, the control policy ensures optimal time budget utilization. A prototype tool implementing the method is shown, as well as experimental results for a non trivial example. The results show the interest of fine grain QoS control for video encoders.

We propose a method for fine grain QoS control of real-time applications. The method allows adapting the overall system behavior by adequately setting the quality level parameters of its actions. The objective of the control policy is to meet QoS requirements including three types of properties: 1) safety that is, no deadline is missed; 2) optimality that is, maximization of the available time budget; 3) smoothness of quality levels. The method takes as input a model of the application software, QoS requirements and platform-dependent timing information, and produces a controlled application software meeting the QoS requirements on the target platform. This paper provides a complete formalization of the quality control problem. It proposes a new control management policy ensuring safety, near-optimality and smoothness. It also describes a prototype tool implementing the quality control algorithm and experimental results about its application to a video encoder.