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

63documents trouvés

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
16202
11/11/2016

Model checking real-time properties on the functional layer of autonomous robots

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

RIS, VERTICS, IDEA

Manifestation avec acte : International Conference on Formal Engineering Methods ( ICFEM ) 2016 du 11 novembre au 14 novembre 2016, Tokyo (Japon), Novembre 2016, 16p. , N° 16202

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

Diffusable

Plus d'informations

Abstract

Software is an essential part of robotic systems. As robots and autonomous systems are more and more deployed in human environments, we need to use elaborate validation and verification techniques in order to gain a higher level of trust in our systems. This motivates our determination to apply formal verification methods to robotics software. In this paper, we describe our results obtained using model-checking on the functional layer of an autonomous robot. We implement an automatic translation from GenoM, a robotics model-based software engineering framework, to the formal specification language Fiacre. This translation takes into account the semantics of the robotics middleware. TINA, our model-checking toolbox, can be used on the synthesized models to prove real-time properties of the functional modules implementation on the robot. We illustrate our approach using a realistic autonomous navigation example.

138502
15357
17/10/2016

On the complexity of flanked finite state automata

F.AVELLANEDA, S.DAL ZILIO, J.B.RACLET

VERTICS, IRIT

Manifestation avec acte : International Symposium on Automated Technology for Verification and Analysis ( ATVA ) 2016 du 10 octobre au 20 octobre 2016, Chiba (Japon), Octobre 2016, 16p. , N° 15357

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

Diffusable

Plus d'informations

Abstract

We define a new subclass of nondeterministic finite automata for prefix-closed languages called Flanked Finite Automata (FFA). We show that this class enjoys good complexity properties while preserving the succinctness of nondeterministic automata. In particular, we show that the universality problem for FFA is in linear time and that language inclusion can be checked in polynomial time. A useful application of FFA is to provide an efficient way to compute the quotient and inclusion of regular languages without the need to use the powerset construction. These operations are the building blocks of several verification algorithms.

139334
16610
04/10/2016

Model-driven approach to the optimal configuration of time-triggered flows in a TTEthernet network

S.BEJI, A.GHERBI, J.MULLINS, P.E.HLADIK

Ecole Montréal, ETSMTL, VERTICS

Manifestation avec acte : System Analysis and Modelling ( SAM ) 2016 du 03 octobre au 04 octobre 2016, Saint Malo (France), Octobre 2016, 16p. , N° 16610

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

Diffusable

Plus d'informations

Abstract

The SAE standard Time-triggered Ethernet defines a strong networking infrastructure, which supports the engineering of avionic systems. Avionic functions are often designed independently and integrated to form the avionic system. The iterative integration approach helps in controlling the design complexity of evolving avionic systems and aims at minimizing the cost associate with the reconfiguration of scheduling parameters of already integrated parts. On the other hand, the iterative approach requires to specify and manage a huge set of constraints, which are then solved to compute the optimal scheduling parameters. In this paper, we focus on this issue of manual specification of these constraints by the system engineer. We propose a model-driven approach, which provides the required abstractions and automation to support the system engineer in using effectively the iterative integration approach. The abstractions consist in a metamodel, which describes the system at a given integration step and a metamodel for the constraints. The automation consists in a model transformation which enables generating automatically the relevant constraints at integration step.

141043
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/