UPPAAL

UPPAAL est un environnement intégré d'outils pour la modélisation, la validation et la vérification des systèmes temps réel modélisés comme des réseaux d'automates temporisés, étendus avec des types de données (entiers bornés, des tableaux, etc.).
UPPAAL CORA est une branche de UPPAAL pour un coût optimal d'accessibilité Anslysis développé par l'équipe UPPAAL dans le cadre des projets de VHS et Ametist. Considérant que UPPAAL soutient model checking d'automates temporisés, UPPAAL CORA utilise une extension des automates temporisés appelé LPTA. LPTA vous permet d'annoter le modèle avec la notion de coût.
Cela peut être le coût du retard dans certaines situations ou le coût des actions particulières. UPPAAL CORA trouve alors trajectoires optimales répondant aux conditions de but.
UPPAAL CORA a été utilisé dans un certain nombre d'études de cas. Certains d'entre eux sont décrits sur la page d'étude de cas de ce site. Si vous venez avec des utilisations intéressantes, s'il vous plaît contactez-nous. Nous sommes intéressés à entendre ce que vous faites!
En raison des différentes structures de données internes, UPPAAL CORA se compose actuellement de deux versions différentes:
Une version pour le cas simplifié de temps optimal analyse d'accessibilité.
Une version pour la langue pleine de LPTA.
Comme UPPAAL, UPPAAL CORA est gratuit pour une utilisation à but non lucratif, par exemple, pour l'évaluation, la recherche et l'enseignement.
Voici quelques caractéristiques principales de "UPPAAL":
Robuste
 
· Le langage de modélisation de UPPAAL CORA est robuste vers des changements dans le problème modélisé. Cela signifie que votre investissement dans la modélisation ne sont pas perdues lorsque le problème change, car il est facile d'adapter le modèle existant.
 
Rapide
 
· Bien que la technologie est relativement nouvelle, expérimentale et très différent de techniques utilisées dans la recherche opérationnelle traditionnelle, UPPAAL CORA est compétitif dans un certain nombre d'études de cas.
 
Compatible
 
· La langue de UPPAAL CORA est un sur-ensemble de UPPAAL. Tout modèle UPPAAL valide est aussi un modèle UPPAAL CORA valide. Cela rend plus facile et pratique à réutiliser et à adapter vos modèles existants pour UppAal CORA.
 
Courant
 
· UPPAAL CORA est basé sur la dernière version de développement interne de UPPAAL, contenant les dernières améliorations de performance et de langue. Il est cependant un outil expérimental et manque beaucoup de fonctionnalités de vérification de UPPAAL.
Limitations:
UPPAAL CORA avec le plein appui LPTA a un certain nombre de limitations. Ces limitations ne sont pas fondamentales, mais sont le résultat de l'utilisation de nouvelles structures de données internes avec un ensemble de fonctionnalités actuellement limitée. Au fil du temps, ces limitations seront résolus.
- Aucune extrapolation, donc la résiliation ne sont pas garanties, sauf si vous garantissez que soit:
· Le système est acyclique.
· Toutes les horloges sont délimitées par des invariants.
- Accessibilité simple que:
· Aucune vérification de vivacité
· Aucune vérification de l'impasse
- Utilisation limitée de guidage:
· Prise en charge (coût + restant) tri est mis en œuvre (meilleure première recherche)
· Support pour la variable heuristique est mis en œuvre, mais l'expression ne peut pas se référer à la variable de coût.
Quoi de neuf dans cette version:
· Cette version corrige des bugs accident et une fuite de mémoire.