Retour au site du LAAS-CNRS

Laboratoire d’analyse et d’architecture des systèmes

Publications de l'équipe VERTICS

Choisir la langue : FR | EN

66documents trouvés

18189
22/06/2018

Petri Net Reductions for Counting Markings

B.BERTHOMIEU, D.LE BOTLAN, S.DAL ZILIO

VERTICS

Manifestation avec acte : International Symposium on Model Checking of Software ( SPIN ) 2018 du 20 juin au 22 juin 2018, Malaga (Espagne), Lecture Notes in Computer Science 10869, Juin 2018, 20p. , N° 18189

Lien : https://hal.laas.fr/hal-01822078

Diffusable

Plus d'informations

Abstract

We propose a method to count the number of reachable markings of a Petri net without having to enumerate these rst. The method relies on a structural reduction system that reduces the number of places and transitions of the net in such a way that we can faithfully compute the number of reachable markings of the original net from the reduced net and the reduction history. The method has been implemented and computing experiments show that reductions are eective on a large benchmark of models.

144023
18113
02/06/2018

Formal Verification of Complex Robotic Systems on Resource-Constrained Platforms

M.FOUGHALI, B.BERTHOMIEU, S.DAL ZILIO, P.E.HLADIK, F.INGRAND, A.MALLET

RIS, VERTICS, IDEA

Manifestation avec acte : International Conference on Formal Methods in Software Engineering ( FormaliSE ) 2018 du 02 juin au 02 juin 2018, Gothenburg (Suède), Juin 2018, 8p. , N° 18113

Lien : https://hal.laas.fr/hal-01778960

Diffusable

Plus d'informations

Abstract

Software constitutes a major part of the development of robotic and autonomous systems and is critical to their successful deployment in our everyday life. Robotic software must thus run and perform as specified. Since most of these systems are used in a hard real-time context, the schedulability of their tasks is a crucial property. In this work, we propose to use formal methods to check whether the tasks of a robotic application are schedulable with respect to a given hardware platform. For this, we automatically translate functional components specified in GenoM into FIACRE, a formal language for timed systems. The generated models integrate realistic real-time schedulers based on the FCFS and the SJF cooperative policies. We use then the model-checker TINA to assert schedulability properties. We carry out experiments on a real robotic system, namely a quadcopter flight controller. We demonstrate that, on its actual hardware, schedulability properties can be formally expressed and verified. We give examples on how we can check other important behavioral and timed properties on the same synthesized models.

143433
18126
22/05/2018

Time-accurate Middleware for the Virtualization of Communication Protocols

R.SCARDUELLI, P.A.BOURDIL, S.DAL ZILIO, D.LE BOTLAN

VERTICS, SCALIAN

Rapport LAAS N°18126, Mai 2018, 48p.

Lien : https://hal.laas.fr/hal-01793367

Diffusable

Plus d'informations

Abstract

Communication between devices in avionics systems must be predictable and deterministic, and data must be delivered reliably. To help the system architects comply with these requirements, network protocol standards like ARINC 429 and AFDX were created. Even though the behaviour of each component in a network is well defined, it is still necessary to test extensively every applications before deployment. But physical test benches used in the aircraft development process are complex and expensive platforms. In order to limit the need for physical tests, we propose a time-accurate middleware for virtualizing communication protocols that can be used to replace physical tests with simulations. We specified three formal models of AFDX networks that take into ac- count temporal constraints with different levels of precision. We also de- veloped a prototype for a network virtualization middleware based on the AFDX protocol specification that provides an easy-to-setup environment for testing network configurations. Finally, we used formal models together with virtualization in order to define runtime monitors for checking whether the behavior of the middleware is time-accurate with respect to a real system.

143553
18053
13/04/2018

A Brute-Force Schedulability Analysis for Formal Model under Logical Execution Time Assumption

P.E.HLADIK

VERTICS

Manifestation avec acte : Annual ACM Symposium on Applied Computing ( ACM-SAC ) 2018 du 09 avril au 13 avril 2018, Pau (France), Avril 2018, 13p. , N° 18053

Lien : https://hal.laas.fr/hal-01717293

Diffusable

Plus d'informations

Abstract

This article presents a schedulability analysis for real-time systems designed under the Logical Execution Time (LET) assumption. This assumption increases the predictability of real-time systems by separating time events from scheduling events. A toolchain based on the formal language Fiacre combined with the LET assumption is designed to organize a set of tools to model, verify, and generate code. In this context, an exact brute-force schedulability analysis based on a simulation is proposed. The tools and algorithms to manage the computation are described and a speedup is proposed. An experiment on a synthetic system shows the efficiency of this approach.

142788
18036
02/02/2018

Timed Formal Model and Verification of Satellite FDIR in Early Design Phase

A.ALBORE, S.DAL ZILIO, M.DE ROQUEMAUREL, C.SEGUIN, P.VIRELIZIER

VERTICS, Airbus Defence & Sp, ONERA, IRT

Manifestation avec acte : Embedded Real Time Software and Systems ( ERTS² ) 2018 du 31 janvier au 02 février 2018, Toulouse (France), Février 2018, 10p. , N° 18036

Lien : https://hal.archives-ouvertes.fr/hal-01709008

Diffusable

Plus d'informations

Abstract

Regular Paper Abstract 1 In a previous work, we proposed an extension of the AltaRica language and tools to deal with the modelling and analysis of failures propagation in presence of timed and temporal constraints. This need is crucial in the space industry, where safety functionalities raise new challenges for the early validation of systems during model conception. This paper focuses on the application of our approach to the Failure Detection Isolation and Recovery (FDIR) mechanisms of the Attitude and Orbit Control System (AOCS) of a satellite. We discuss the modelling methodology applied to this system and its properties, as well as the tractability of the model-checking analysis. 1 An Expression of Industrial Needs and Requirements Failure Detection, Isolation and Recovery (FDIR) functions are implemented aboard satellites in order to detect the occurrence of failures and to prevent the failure from propagating in the whole system, which could cause critical events and thus jeopardize the mission. The complexity of the FDIR verification and validation (V&V) increases with the system complexity. As systems include more and more interacting functions and functional modes, it becomes harder to evaluate at the overall system level the effects of local failures. That is even truer when we consider the effects of time. Indeed, unexpected behavior can arise from a bad timing of events. Timing constraints allow to represent the impact of computation times, delays on the propagation of failures, and the reaction time of the reconfigurations steps triggered in reaction to failure detection. Thus, new models and tools are needed to assist early V&V of the on-board processes and FDIR design. Thomas and Blanquart [1] describe a process to model FDIR satellite functions. This process requires to model failure propagation, detection, and recovery times, which requires modelling languages expressive enough to support complex system modelling. Associated tools should provide automatic verification that on-board FDIR functions are correct despite latency in failure 1 We thank Jean-Paul Blanquart of AIRBUS Defence and Space for his kindness in discussing the FDIR model, and the evaluation of requirements for AOCS mode during the assessment of the scalability of the approach.

142663
17308
15/09/2017

Formal verification of user-level real-time property patterns

N.GE, M.PANTEL, S.DAL ZILIO

Beihang University, IRIT-ENSEEIHT, VERTICS

Manifestation avec acte : International Symposium on Theoretical Aspects of Software Engineering ( TASE ) 2017 du 13 septembre au 15 septembre 2017, Sophia Antipolis (France), Septembre 2017, 8p. , N° 17308

Lien : https://hal.archives-ouvertes.fr/hal-01589479

Diffusable

Plus d'informations

Abstract

To ease the expression of real-time requirements, Dwyer, and then Konrad, studied a large collection of existing systems in order to identify a set of real-time property patterns covering most of the useful use cases. The goal was to provide a set of reusable patterns that system designers can instantiate to express requirements instead of using complex temporal logic formulas. A limitation of this approach is that the choice of patterns is more oriented towards expressiveness than efficiency; meaning that it does not take into account the computational complexity of checking patterns. For this purpose, we define a set of verification-dedicated, atomic property patterns for qualitative and quantitative real-time requirements. End-user requirements can then be expressed as a composition of these patterns using a predefined meta-model and a mapping library. These properties can be checked efficiently using a set of elementary observers and a model checking approach.

140893
17339
13/09/2017

A model-checking approach to analyse temporal failure propagation with AltaRica

A.ALBORE, S.DAL ZILIO, G.INFANTES, C.SEGUIN, P.VIRELIZIER

VERTICS, RIS, ONERA, IRT

Manifestation avec acte : International Symposium on Model-Based Safety and Assessment ( IMBSA ) 2017 du 11 septembre au 13 septembre 2017, Trento (Italie), Septembre 2017, 15p. , N° 17339

Lien : https://hal.archives-ouvertes.fr/hal-01693391

Diffusable

Plus d'informations

Abstract

The design of complex safety critical systems raises new technical challenges for the industry. As systems become more complex—and include more and more interacting functions—it becomes harder to evaluate the safety implications of local failures and their possible propagation through a whole system. That is all the more true when we add time to the problem, that is when we consider the impact of computation times and delays on the propagation of failures. We describe an approach that extends models developed for Safety Analysis with timing information and provide tools to reason on the correctness of temporal safety conditions. Our approach is based on an extension of the AltaRica language where we can associate timing constraints with events and relies on a translation into a realtime model-checking toolset. We illustrate our method with an example that is representative of safety architectures found in critical systems.

141115
16601
15/12/2016

Symmetry reduction for time Petri net state classes

P.A.BOURDIL, B.BERTHOMIEU, S.DAL ZILIO, F.VERNADAT

VERTICS

Revue Scientifique : Science of Computer Programming, Vol.132, N°Part 2, pp.209-225, Décembre 2016 , N° 16601

Lien : https://hal.laas.fr/hal-01561994

Diffusable

Plus d'informations

Abstract

We propose a method to exploit the symmetries of a real-time system represented by a Time Petri net for its verification by model-checking. The method handles both markings and timing constraints; it can be used in conjunction with the widely used state classes abstraction, a construction providing a finite representation of the behavior of a Time Petri net preserving its markings and traces. The approach has been implemented and experiments are reported.

140493
16432
12/12/2016

De l'illustration du guidage à l'optimisation d'un plan par un robot Lego Mindstorm NXT

E.CHANTHERY, G.LE CORRE, P.E.HLADIK

DISCO, INSAT, VERTICS

Revue Scientifique : Journal sur l'enseignement des sciences et technologies de l'information et des, Vol.15, 12p., Décembre 2016 , N° 16432

Lien : https://hal.archives-ouvertes.fr/hal-01392601

Diffusable

Plus d'informations

Résumé

Cet article présente un projet mené au Département Génie Électrique et Informatique de l’Institut National des Sciences Appliquées (INSA) de Toulouse dont le but est la commande d’un robot Lego NXT. L’objectif est d’illustrer les différents niveaux de commande, du guidage bas niveau effectué par une régulation de position jusqu’à l’optimisation d’un plan de mission.

138343
16510
21/11/2016

Contribution à la conception et à la vérification de systèmes temps réel - Focus sur l'ordonnancement temps réel

P.E.HLADIK

VERTICS

Habilitation à diriger des recherches : 21 Novembre 2016, 153p., Président: J.C.FABRE, Rapporteurs: L.GEORGE, E.GROLLEAU, G.LIPARI, Examinateurs: N.NAVET, F.SINGHOFF , N° 16510

Lien : https://hal.archives-ouvertes.fr/tel-01451027

Diffusable

Plus d'informations

Résumé

Cette Habilitation à Diriger les Recherches est l'occasion de présenter mes travaux de recherche sur la conception et la validation des systèmes embarqués critiques. Après une introduction du contexte de recherche, l'exposé se focalisera sur les problématiques de l’ordonnancement temps réel et sur les diverses problématiques que j'ai pu aborder dans ce contexte. Une attention particulière sera portée à la configuration d'architectures avioniques ainsi qu’à l'évaluation des politiques d'ordonnancement multiprocesseur pour l'automobile. L’exposé se conclura sur les perspectives envisagées pour poursuivre ces travaux et les étendre à la génération d’exécutable temporellement fiable.

Mots-Clés / Keywords
Conception; Ordonnancement; Système embarqué; Temps réel; Validation;

138933
Les informations recueillies font l’objet d’un traitement informatique destiné à des statistiques d'utilisation du formulaire de recherche dans la base de données des publications scientifiques. Les destinataires des données sont : le service de documentation du LAAS.Conformément à la loi « informatique et libertés » du 6 janvier 1978 modifiée en 2004, vous bénéficiez d’un droit d’accès et de rectification aux informations qui vous concernent, que vous pouvez exercer en vous adressant à
Pour recevoir une copie des documents, contacter doc@laas.fr en mentionnant le n° de rapport LAAS et votre adresse postale. Signalez tout problème de dysfonctionnement à sysadmin@laas.fr. http://www.laas.fr/pulman/pulman-isens/web/app.php/