Systèmes réactifs : modélisation, spécification et vérification Van Luca Aceto, Anna Ingolfsdottir et Kim Guldstrand Larsen est un manuel anglophone destiné à la spécification et à la vérification de logiciels et de systèmes distribués. Cet ouvrage de référence vise les professionnels et les étudiants qui recherchent une introduction équilibrée aux méthodes formelles.
Le livre traite des méthodologies pour la spécification et la vérification de logiciels à l’aide d’une logique mathématique, notamment le CCS de Milner et des techniques de simulation bisimilaire. En outre, une attention est portée à la sémantique opérationnelle et à des variantes de la logique modale de Hennessy-Milner. De plus, les modèles sont étendus avec des éléments de temps, ce qui est pertinent pour les systèmes temps réel.
Grâce à l’intégration de diverses approches, ce titre offre une vue d’ensemble large des possibilités et des limites de la spécification et de la vérification au sein de l’algèbre des processus et des systèmes distribués. Le contenu est basé sur des leçons en Islande et au Danemark et comprend des exercices pour soutenir le processus d’apprentissage.
Sur le plan du contenu, ce livre s’inscrit dans des domaines tels que le génie logiciel et le développement de logiciels ; il constitue ainsi une ressource précieuse pour les formations techniques et les professionnels spécialisés.