| Attributes | Values |
|---|
| type
| |
| Thesis advisor
| |
| Author
| |
| dc:subject
| - Compilateur
- Thèses et écrits académiques
- Prototype
- Sciences et techniques
- Informatique. automatique theorique. systemes
- Validation
- Langage programmation
- Verification
- Systeme reparti
- Algebre processus
- Calcul parallele
- Description formelle
- E-lotos
- Lotos
- Lotos nt
- Reseau petri
- Reseau petri temporise
- Semantique operationnelle
- Semantique structuree
- Temps reel
- Transition etiquetee
|
| preferred label
| - Contribution à la définition et à l'implémentation du langage \"Extended Lotos\"
|
| Language
| |
| Subject
| |
| dc:title
| - Contribution à la définition et à l'implémentation du langage \"Extended Lotos\"
|
| Degree granting institution
| |
| note
| - La mise au point des applications distribuees critiques est un probleme complexe pour lequel il est recommande d'utiliser des techniques de description formelle afin de specifier sans ambiguite le comportement des applications considerees, et des outils de verification automatique ou semi-automatique afin de valider le bon fonctionnement de ces applications. Les techniques de description formelle existantes (notamment les trois langages normalises estelle, lotos et sdl) presentent des inconvenients et des limitations qui restreignent leur adoption en milieu industriel. Cette these vise a resoudre ce probleme en proposant un nouveau formalisme, appele lotos nt, pour la description formelle des applications paralleles et temps-reel. Ce formalisme, qui combine des concepts issus des langages de programmation fonctionnels et imperatifs et des algebres de processus temporisees, est plus simple et plus expressif que les langages existants et autorise une compilation plus efficace. Ce travail constitue une contribution a la revision de la norme lotos entreprise a l'iso. Cette these definit formellement les trois parties du langage lotos nt (donnees, controle et modules) en donnant leur syntaxe, leur semantique statique et leur semantique dynamique (formulee de maniere operationnelle en termes de systemes de transitions temporises). Ensuite, un modele d'execution intermediaire base sur des reseaux de petri temporises est defini. Enfin, deux algorithmes de traduction permettent de passer de lotos nt a ce modele intermediaire, d'une part, et du modele intermediaire a des systemes de transitions temporises, d'autre part. L'interet de cette approche a ete montre sur plusieurs applications concretes et un compilateur prototype pour le langage lotos nt a ete developpe.
|
| dc:type
| |
| http://iflastandar...bd/elements/P1001
| |
| rdaw:P10219
| |
| has content type
| |
| is primary topic
of | |
| is rdam:P30135
of | |
![[RDF Data]](/fct/images/sw-rdf-blue.png)
