| Titre : |
Outils de Mise en Oeuvre Industrielle des Techniques Formelles |
| Type de document : |
texte imprimé |
| Auteurs : |
BOULANGER, Jean-Louis, Auteur |
| Editeur : |
Lavoisier |
| Année de publication : |
2012 |
| Importance : |
389p. |
| Présentation : |
couv. illus. en coul. |
| Format : |
24 cm. |
| ISBN/ISSN/EAN : |
978-2-7462-3801-5 |
| Langues : |
Français (fre) |
| Catégories : |
04 Génie Electrique
|
| Mots-clés : |
SCAD SPARK ControlBuild Polyspace. |
| Index. décimale : |
04-04- Automatique |
| Résumé : |
Les techniques formelles réalisent des modèles de spécifications et/ou de conception et servent principalement à l'analyse statique de code, à la démonstration du respect de propriété et à la bonne gestion des calculs sur les flottants.
Différents domaines tels les systèmes de transport, la production d'énergie ou la santé prennent en compte l'implémentation de ces méthodes pour satisfaire les exigences de sécurité élevées des systèmes critiques. Leur mise en oeuvre dans le cadre d'une application industrielle (application de grande taille, contrainte de coût et de délais, etc.) ne peut se faire que par l'emploi d'outils suffisamment matures et performants.
Cet ouvrage collectif présente des exemples concrets d'utilisation des techniques formelles comme la méthode B, SCADE, MaTeLo, ControlBuild, SparkAda et POLYSPACE et des techniques de vérification associées. Il en identifie aussi les avantages et les difficultés. |
| Note de contenu : |
Introduction
Chapitre 1: Des Langages Classique aux Méthodes Formelles
Chapitre 2: SCADE: mise en Oeuvre et Applications
Chapitre 3: SPARK, un Langage et une Boite à Outils pour le Développement de Logiciel Critique
Chapitre 4: ControlBuild
Chapitre 5: Model Based Testing.Génération Automatique de cas de Test à L'aide d'une Modélisation par Chaines de Markov
Chapitre 6: Analyse de Sécurité ds Systèmes Embarqués avec AltaRica
Chapitre 7: Méthode B et Outils B
Chapitre 8: Polyspace
Chapitre 9: Synthèse et Conclusions
Glossaire
Index |
Outils de Mise en Oeuvre Industrielle des Techniques Formelles [texte imprimé] / BOULANGER, Jean-Louis, Auteur . - Lavoisier, 2012 . - 389p. : couv. illus. en coul. ; 24 cm. ISBN : 978-2-7462-3801-5 Langues : Français ( fre)
| Catégories : |
04 Génie Electrique
|
| Mots-clés : |
SCAD SPARK ControlBuild Polyspace. |
| Index. décimale : |
04-04- Automatique |
| Résumé : |
Les techniques formelles réalisent des modèles de spécifications et/ou de conception et servent principalement à l'analyse statique de code, à la démonstration du respect de propriété et à la bonne gestion des calculs sur les flottants.
Différents domaines tels les systèmes de transport, la production d'énergie ou la santé prennent en compte l'implémentation de ces méthodes pour satisfaire les exigences de sécurité élevées des systèmes critiques. Leur mise en oeuvre dans le cadre d'une application industrielle (application de grande taille, contrainte de coût et de délais, etc.) ne peut se faire que par l'emploi d'outils suffisamment matures et performants.
Cet ouvrage collectif présente des exemples concrets d'utilisation des techniques formelles comme la méthode B, SCADE, MaTeLo, ControlBuild, SparkAda et POLYSPACE et des techniques de vérification associées. Il en identifie aussi les avantages et les difficultés. |
| Note de contenu : |
Introduction
Chapitre 1: Des Langages Classique aux Méthodes Formelles
Chapitre 2: SCADE: mise en Oeuvre et Applications
Chapitre 3: SPARK, un Langage et une Boite à Outils pour le Développement de Logiciel Critique
Chapitre 4: ControlBuild
Chapitre 5: Model Based Testing.Génération Automatique de cas de Test à L'aide d'une Modélisation par Chaines de Markov
Chapitre 6: Analyse de Sécurité ds Systèmes Embarqués avec AltaRica
Chapitre 7: Méthode B et Outils B
Chapitre 8: Polyspace
Chapitre 9: Synthèse et Conclusions
Glossaire
Index |
|  |
04-00 Généralité
Affiner la recherche Interroger des sources externesOutils de Mise en Oeuvre Industrielle des Techniques Formelles
