Des services pour PMB
Détail de l'indexation
04-00 GénéralitéOuvrages de la bibliothèque en indexation 04-04- Automatique (54)
Affiner la recherche Interroger des sources externes
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
IndexOutils 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
IndexRéservation
Réserver ce document
Exemplaires (2)
Code-barres Cote Support Localisation Section Disponibilité 16078 04-04-55/01 Livre Bibliotheque ESG2E Document Exclu du prêt 16079 04-04-55/02 Livre Bibliotheque ESG2E Document Disponible
Titre : Logique et Démonstration Automatique : Introduction à la Logique Propositionnelle et à la Logique du Premier Ordre Type de document : texte imprimé Auteurs : DEVISMES, Stéphane, Auteur ; LAFOURCADE, Pascal, Auteur ; LEVY, Michel, Auteur Editeur : Ellipses Année de publication : 2012 Importance : 209 P. Présentation : couv. illus. en coul. Format : 26 cm. ISBN/ISSN/EAN : 978-2-7298-7229-8 Langues : Français (fre) Catégories : 04 Génie Electrique Mots-clés : Logique Propositionnelle Résolution Propositionnelle Méthodes de Herbrand Déduction Naturelle. Index. décimale : 04-04- Automatique Résumé : L'ouvrage: Niveau a (IUT-BTS-1er Cycle), Destiné Principalement aux étudiants des Premiers Cycles Scientifiques, un Livre pour leur faire Découvrir la Logique, Renforcer leur Rigueur et Conforter leur Aptitude à Raisonner.
L'ouvrage ne Nécessite pas de Connaissance a priori en Logique, ni en Mathématiques.
L'étude se Concentre sur la Logique Classique à deux Valeurs de Vérité, Logique qui est celle des Circuits Combinatoires. Sont uniquement Présentés des Résultats et Algorithmes dont il existe une Réalisation Logicielle Permettant de les Appliquer Automatiquement sur des Exemples.
Dans une Première Partie Consacrée à la Logique Propositionnelle sont Présentés les définitions, Les Résultats de Base. La Résolution, La Stratégie Complète et L'algorithme DPLL, ainsi que la Déduction Naturelle. Dans la Seconde Partie L'ensemble des Notions, Résultats et Techniques et Revisité pour la Logique de Premier Ordre.
Enfin le Livre Comprend de Nombreux Exercices Gradués avec Leurs Corrigés Détaillés, qui Permettant à Chacun de Tester ses Connaissances et la Compréhension des Concepts Présentés.Note de contenu : Avant-Propos
A- Logique Propositionnelle
1. logique Propositionnelle
2. Résolution Propositionnelle
3. Déduction Naturelle
B- Logique du Premier Ordre
4. Logique du Premier Ordre
5. Base de la Démonstration Automatique
6. Déduction Naturelle au Premier Ordre: quantificateurs ,copie et égalité
C- Annexes
Corrigés
Bibliographie
Index
Logique et Démonstration Automatique : Introduction à la Logique Propositionnelle et à la Logique du Premier Ordre [texte imprimé] / DEVISMES, Stéphane, Auteur ; LAFOURCADE, Pascal, Auteur ; LEVY, Michel, Auteur . - Ellipses, 2012 . - 209 P. : couv. illus. en coul. ; 26 cm.
ISBN : 978-2-7298-7229-8
Langues : Français (fre)
Catégories : 04 Génie Electrique Mots-clés : Logique Propositionnelle Résolution Propositionnelle Méthodes de Herbrand Déduction Naturelle. Index. décimale : 04-04- Automatique Résumé : L'ouvrage: Niveau a (IUT-BTS-1er Cycle), Destiné Principalement aux étudiants des Premiers Cycles Scientifiques, un Livre pour leur faire Découvrir la Logique, Renforcer leur Rigueur et Conforter leur Aptitude à Raisonner.
L'ouvrage ne Nécessite pas de Connaissance a priori en Logique, ni en Mathématiques.
L'étude se Concentre sur la Logique Classique à deux Valeurs de Vérité, Logique qui est celle des Circuits Combinatoires. Sont uniquement Présentés des Résultats et Algorithmes dont il existe une Réalisation Logicielle Permettant de les Appliquer Automatiquement sur des Exemples.
Dans une Première Partie Consacrée à la Logique Propositionnelle sont Présentés les définitions, Les Résultats de Base. La Résolution, La Stratégie Complète et L'algorithme DPLL, ainsi que la Déduction Naturelle. Dans la Seconde Partie L'ensemble des Notions, Résultats et Techniques et Revisité pour la Logique de Premier Ordre.
Enfin le Livre Comprend de Nombreux Exercices Gradués avec Leurs Corrigés Détaillés, qui Permettant à Chacun de Tester ses Connaissances et la Compréhension des Concepts Présentés.Note de contenu : Avant-Propos
A- Logique Propositionnelle
1. logique Propositionnelle
2. Résolution Propositionnelle
3. Déduction Naturelle
B- Logique du Premier Ordre
4. Logique du Premier Ordre
5. Base de la Démonstration Automatique
6. Déduction Naturelle au Premier Ordre: quantificateurs ,copie et égalité
C- Annexes
Corrigés
Bibliographie
Index
Exemplaires (1)
Code-barres Cote Support Localisation Section Disponibilité 16714 04-04-57/01 Livre Bibliotheque ESG2E Document Exclu du prêt
Titre : Séquence après Séquence : Logique Séquentielle Circuits Asynchrones et Synchrones Type de document : texte imprimé Auteurs : jean-pierre MERCIER, Auteur Editeur : Ellipses Année de publication : 2006 Importance : 269 p. Présentation : couv. illus. en coul. Format : 26 cm. ISBN/ISSN/EAN : 978-2-7298-2619-x Langues : Français (fre) Catégories : 04 Génie Electrique Mots-clés : Logique Séquentielle Asynchrone Logique Séquentielle Synchrone Réseaux de Petri et au Grafcet. Index. décimale : 04-04- Automatique Résumé : L'ouvrage: niveau B (Licence) et C (Master,Ecoles d'ingénieurs).
Pour tous les étudiants et élèves-ingénieurs, comme pour tous les professionnels de l'informatique et de l'automatique, cet ouvrage présente les méthodes de synthèse des machines logiques séquentielles utilisées dans les ordinateurs et dans les automates logiques. Il traite des structures asynchrones et synchrones de types Moore et Mealy. La première partie développe une méthodologie générale de synthèse des machines asynchrones, avec application aux différents types de mémoires logique.
La deuxième partie expose la mise en œuvre des automates synchrones et une introduction aux langages ASM flowchart et VHDL. La troisième partie est une introduction aux réseaux de Petri et une présentation des concepts mis en œuvre dans le grafcet. Dans chaque partie sont aussi développés de nombreux exercices corrigés.
L'ouvrage s'inscrit dans un traité complet sur les computers, avec deux autres ouvrages du même auteur, dans la même collection:
en amont: bit après bit
en aval: instruction après instruction.Note de contenu :
Avant-propos
Préambule a la Logique Séquentielle
p-1 Introduction
p-2 Machines Asynchrones et Synchrones
p-3 Structure interne d'une Machine Séquentielle
p-4 Etat d'une Machine Séquentielle
p-5 Graphe d'état d'une Machine Séquentielle
p-6 Machine de MOORE et Machine de MEALY
Chapitre 1. Logique Séquentielle Asynchrone
Chapitre 2. Logique Séquentielle Synchrone
Chapitre 3. Introduction aux Réseaux de Petri et au Grafcet
Annexes
Séquence après Séquence : Logique Séquentielle Circuits Asynchrones et Synchrones [texte imprimé] / jean-pierre MERCIER, Auteur . - Ellipses, 2006 . - 269 p. : couv. illus. en coul. ; 26 cm.
ISSN : 978-2-7298-2619-x
Langues : Français (fre)
Catégories : 04 Génie Electrique Mots-clés : Logique Séquentielle Asynchrone Logique Séquentielle Synchrone Réseaux de Petri et au Grafcet. Index. décimale : 04-04- Automatique Résumé : L'ouvrage: niveau B (Licence) et C (Master,Ecoles d'ingénieurs).
Pour tous les étudiants et élèves-ingénieurs, comme pour tous les professionnels de l'informatique et de l'automatique, cet ouvrage présente les méthodes de synthèse des machines logiques séquentielles utilisées dans les ordinateurs et dans les automates logiques. Il traite des structures asynchrones et synchrones de types Moore et Mealy. La première partie développe une méthodologie générale de synthèse des machines asynchrones, avec application aux différents types de mémoires logique.
La deuxième partie expose la mise en œuvre des automates synchrones et une introduction aux langages ASM flowchart et VHDL. La troisième partie est une introduction aux réseaux de Petri et une présentation des concepts mis en œuvre dans le grafcet. Dans chaque partie sont aussi développés de nombreux exercices corrigés.
L'ouvrage s'inscrit dans un traité complet sur les computers, avec deux autres ouvrages du même auteur, dans la même collection:
en amont: bit après bit
en aval: instruction après instruction.Note de contenu :
Avant-propos
Préambule a la Logique Séquentielle
p-1 Introduction
p-2 Machines Asynchrones et Synchrones
p-3 Structure interne d'une Machine Séquentielle
p-4 Etat d'une Machine Séquentielle
p-5 Graphe d'état d'une Machine Séquentielle
p-6 Machine de MOORE et Machine de MEALY
Chapitre 1. Logique Séquentielle Asynchrone
Chapitre 2. Logique Séquentielle Synchrone
Chapitre 3. Introduction aux Réseaux de Petri et au Grafcet
Annexes
Exemplaires (1)
Code-barres Cote Support Localisation Section Disponibilité 16713 04-04-56/01 Livre Bibliotheque ESG2E Document Exclu du prêt
Titre : Acquisition de Données : Du Capteur à L'Ordinateur. Type de document : texte imprimé Auteurs : Georges ASCH, Auteur Editeur : DUNOD Année de publication : 2011 Importance : 524p. Présentation : couv. en coull. Format : 25cm. ISBN/ISSN/EAN : 978-2-10-052331-3 Langues : Français (fre) Langues originales : Français (fre) Catégories : 04 Génie Electrique Mots-clés : Capteurs Intelligents Réseaux-Le Microprocesseur-Les Capteurs-Perturbations par Couplage électromagnétique... Index. décimale : 04-04- Automatique Acquisition de Données : Du Capteur à L'Ordinateur. [texte imprimé] / Georges ASCH, Auteur . - DUNOD, 2011 . - 524p. : couv. en coull. ; 25cm.
ISBN : 978-2-10-052331-3
Langues : Français (fre) Langues originales : Français (fre)
Catégories : 04 Génie Electrique Mots-clés : Capteurs Intelligents Réseaux-Le Microprocesseur-Les Capteurs-Perturbations par Couplage électromagnétique... Index. décimale : 04-04- Automatique Exemplaires (1)
Code-barres Cote Support Localisation Section Disponibilité 5680 04-04-45/01 Livre Bibliotheque ESG2E Document Exclu du prêt
Titre : Adaptive filtering : fundamentals of least mean squares with MATLAB Type de document : texte imprimé Auteurs : Alexander D. POULARIKAS, Auteur Editeur : CRC Press Année de publication : 2014 Importance : 343p. Présentation : ill. Format : 23cm. ISBN/ISSN/EAN : 978-1-4822-5335-1 Langues : Anglais (eng) Langues originales : Anglais (eng) Catégories : 04 Génie Electrique Mots-clés : vectors matrices processing of discrete deteministic signals: discrete systems discrete-time random processes the wiener filter Index. décimale : 04-04- Automatique Adaptive filtering : fundamentals of least mean squares with MATLAB [texte imprimé] / Alexander D. POULARIKAS, Auteur . - CRC Press, 2014 . - 343p. : ill. ; 23cm.
ISBN : 978-1-4822-5335-1
Langues : Anglais (eng) Langues originales : Anglais (eng)
Catégories : 04 Génie Electrique Mots-clés : vectors matrices processing of discrete deteministic signals: discrete systems discrete-time random processes the wiener filter Index. décimale : 04-04- Automatique Exemplaires (1)
Code-barres Cote Support Localisation Section Disponibilité 14771 04-04-24/01 Livre Bibliotheque ESG2E Document Exclu du prêt PermalinkPermalinkPermalinkPermalinkPermalinkPermalinkPermalinkPermalinkPermalinkAutonomie énergétique des Systèmes Embarqués Sans Fil et Sans Batterie Vol 1. / Jean-Marie DILHAC
Permalink
