PragmaDev Studio V6.1 introduit des capacités avancées de réduction de l’espace d’états pour une exploration des modèles plus rapide et plus efficace
9 juin 2026
PragmaDev annonce aujourd’hui la sortie de PragmaDev Studio V6.1, qui apporte des améliorations majeures en matière d’exploration de modèles et de réduction de l’espace d’états. Ces nouvelles fonctionnalités renforcent encore la position de PragmaDev Studio comme outil de référence pour le model checking et la vérification formelle, en permettant aux ingénieurs d’analyser des systèmes complexes plus efficacement que jamais.
L’objectif principal du model checking est d’explorer tous les scénarios d’exécution possibles d’un modèle. Cette analyse exhaustive permet non seulement d’identifier les interblocages (deadlocks), de détecter les branches inaccessibles et de vérifier les propriétés critiques du système, mais aussi d’améliorer significativement la couverture du modèle en garantissant que tous les états, transitions et chemins d’exécution sont examinés de manière systématique. En mettant en évidence les parties du modèle qui ne sont jamais exercées et en validant les comportements attendus dans un large éventail de conditions, le model checking contribue à concevoir des systèmes plus sûrs, plus fiables et plus sécurisés.
S’appuyant sur une collaboration de longue date avec le laboratoire de recherche de l’ENSTA Bretagne, PragmaDev avait précédemment intégré le model checker Observer Based Prover (OBP) dans PragmaDev Studio V6. OBP propose une approche unique de la vérification formelle en évitant le recours à un langage de modélisation dédié. Il s’appuie à la place sur un moteur d’exécution externe pour réaliser l’exploration du modèle.
Au sein de PragmaDev Studio, OBP interagit directement avec le moteur d’exécution SDL de PragmaDev afin d’exécuter les transitions du modèle. Par conséquent, OBP reste totalement indépendant de la structure du modèle elle-même. Le même principe s’applique à la vérification des propriétés : les propriétés complexes sont décomposées en propriétés atomiques, qui sont évaluées par le moteur d’exécution au cours de l’exploration.
Les systèmes communicants génèrent naturellement un très grand nombre de scénarios d’exécution en raison de leur architecture composée de machines à états concurrentes. L’espace d’états résultant peut alors croître rapidement, rendant l’exploration exhaustive de plus en plus difficile.
Pour répondre à ce défi, PragmaDev Studio V6.1 introduit de nouvelles techniques améliorées de réduction de l’espace d’états qui augmentent considérablement l’efficacité de l’exploration tout en préservant la pertinence de la vérification. Ces capacités comprennent notamment :
- La réduction de l’intervalle des valeurs possibles pour les paramètres complexes transportés par les messages entrants.
- La limitation du nombre de messages entrants pris en compte pour chaque type de message.
- L’identification automatique des variables internes pouvant être exclues de l’état global du modèle sans affecter les résultats de la vérification.
En réduisant l’espace d’états exploré, ces améliorations permettent aux ingénieurs de vérifier des systèmes plus vastes et plus complexes, d’accélérer les analyses et de se concentrer sur les scénarios d’exécution les plus pertinents.
Grâce à ces innovations, PragmaDev Studio V6.1 offre les capacités d’exploration de modèles les plus puissantes jamais proposées par PragmaDev, aidant ainsi les équipes de développement à atteindre un niveau de confiance encore plus élevé dans la correction, la sûreté et la sécurité de leurs conceptions de systèmes.
- Source : communiqué de presse Pragmadev (membre de NextMove)
