top

  Info

  • Utilizzare la checkbox di selezione a fianco di ciascun documento per attivare le funzionalità di stampa, invio email, download nei formati disponibili del (i) record.

  Info

  • Utilizzare questo link per rimuovere la selezione effettuata.

Biblioteca

MARC Lista (tabellare)
2010 Ninth International Workshop on Parallel and Distributed Methods in Verification, and Second International Workshop on High Performance Computational Systems Biology / / Institute of Electrical and Electronics Engineers
2010 Ninth International Workshop on Parallel and Distributed Methods in Verification, and Second International Workshop on High Performance Computational Systems Biology / / Institute of Electrical and Electronics Engineers
Pubbl/distr/stampa Piscataway, N.J. : , : IEEE, , 2010
Descrizione fisica 1 online resource : illustrations
Disciplina 005.1
Soggetto topico Computer programs - Verification
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Altri titoli varianti Parallel and Distributed Methods in Verification, 2010 Ninth International Workshop on, and Second International Workshop on High Performance Computational Systems Biology
Record Nr. UNISA-996202053903316
Piscataway, N.J. : , : IEEE, , 2010
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
2010 Ninth International Workshop on Parallel and Distributed Methods in Verification, and Second International Workshop on High Performance Computational Systems Biology / / Institute of Electrical and Electronics Engineers
2010 Ninth International Workshop on Parallel and Distributed Methods in Verification, and Second International Workshop on High Performance Computational Systems Biology / / Institute of Electrical and Electronics Engineers
Pubbl/distr/stampa Piscataway, N.J. : , : IEEE, , 2010
Descrizione fisica 1 online resource : illustrations
Disciplina 005.1
Soggetto topico Computer programs - Verification
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Altri titoli varianti Parallel and Distributed Methods in Verification, 2010 Ninth International Workshop on, and Second International Workshop on High Performance Computational Systems Biology
Record Nr. UNINA-9910141033403321
Piscataway, N.J. : , : IEEE, , 2010
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
2019 Forum for Specification and Design Languages (FDL) / / Institute of Electrical and Electronics Engineers
2019 Forum for Specification and Design Languages (FDL) / / Institute of Electrical and Electronics Engineers
Pubbl/distr/stampa [Place of publication not identified] : , : IEEE, , 2019
Descrizione fisica 1 online resource
Disciplina 005.14
Soggetto topico Computer programs - Verification
ISBN 1-7281-4113-3
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Altri titoli varianti 2019 Forum for Specification and Design Languages
Record Nr. UNINA-9910347944203321
[Place of publication not identified] : , : IEEE, , 2019
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
2019 Forum for Specification and Design Languages (FDL) / / Institute of Electrical and Electronics Engineers
2019 Forum for Specification and Design Languages (FDL) / / Institute of Electrical and Electronics Engineers
Pubbl/distr/stampa [Place of publication not identified] : , : IEEE, , 2019
Descrizione fisica 1 online resource
Disciplina 005.14
Soggetto topico Computer programs - Verification
ISBN 1-7281-4113-3
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Altri titoli varianti 2019 Forum for Specification and Design Languages
Record Nr. UNISA-996575400703316
[Place of publication not identified] : , : IEEE, , 2019
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
2022 IEEE/ACM Sixth International Workshop on Software Correctness for HPC Applications (Correctness) / / IEEE Computer Society
2022 IEEE/ACM Sixth International Workshop on Software Correctness for HPC Applications (Correctness) / / IEEE Computer Society
Pubbl/distr/stampa Piscataway, New Jersey : , : IEEE Computer Society, , 2022
Descrizione fisica 1 online resource
Disciplina 005.14
Soggetto topico Computer programs - Verification
ISBN 1-66546-335-X
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Altri titoli varianti 2022 IEEE/ACM Sixth International Workshop on Software Correctness for HPC Applications
Record Nr. UNISA-996575100903316
Piscataway, New Jersey : , : IEEE Computer Society, , 2022
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
Computervalidierung in labor und betrieb [[electronic resource] ] : sicherheit und qualität computergestützter systeme / / H.D. Unkelbach, P. Bosshard, H. Wolf
Computervalidierung in labor und betrieb [[electronic resource] ] : sicherheit und qualität computergestützter systeme / / H.D. Unkelbach, P. Bosshard, H. Wolf
Autore Unkelbach H. D (Hans-Dieter)
Pubbl/distr/stampa Weinheim, : Wiley-VCH, 1998
Descrizione fisica 1 online resource (338 p.)
Disciplina 629.895
Altri autori (Persone) BosshardP (Peter)
WolfH
Soggetto topico Computer programs - Verification
Computer software - Quality control
Soggetto genere / forma Electronic books.
ISBN 1-282-02153-2
9786612021534
3-527-62456-2
3-527-62457-0
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione ger
Nota di contenuto Computervalidierung in Labor und Betrieb; Inhaltsverzeichnis; 1 Einleitung; 2 Grundlegende Begriffe und Konzepte; 2.1 Der Begriff ,, Validierung"; 2.2 Computervalidierung in der Anwendungspraxis; 2.3 Qualität von Information; 2.4 Qualität von Daten; 2.4.1 Korrektheit und Genauigkeit; 2.4.2 Gültigkeit und Authentizität; 2.4.3 Datenintegrität und Datensicherheit; 2.4.4 Vertraulichkeit; 2.4.5 Verfügbarkeit; 2.4.6 Bedeutung; 2.5 Qualität von Verfahren; 2.6 Validierung im Software-Lebenszyklus; 2.7 Maßnahmen zur Daten- und Programmsicherheit; 2.7.1 Datensicherungen; 2.7.2 Ersatzprozeduren
2.7.3 Physische Zugangskontrolle2.7.4 Logische Zugangskontrolle; 2.7.5 Virenschutz; 2.7.6 Kryptografische Verfahren; 3 Software-Entwicklung; 3.1 Phasenmodell; 3.2 Validierung in der Software-Entwicklung; 3.2.1 Reviews; 3.2.2 Statische Analysemethoden; 3.2.3 Tests; 3.3 Entwicklungsdokumentation; 3.4 Computer Aided Software Engineering (CASE); 3.5 Qualitätsmanagement in der Software-Entwicklung; 4 Betrieb computergestützter Systeme; 4.1 Installation und Installationstest; 4.2 Abnahme- und Akzeptanztest; 4.3 Validierungsplan; 4.4 Validierungsdokumentation; 4.5 Revalidierungen
4.6 Software-Lebenszyklus5 Validierungsanforderungen; 5.1 Gesetze, Verordnungen, Normen und Richtlinien; 5.2 Qualitätsregelwerke für chemisch-pharmazeutische Bereiche; 5.2.1 Good Manufacturing Practice (GMP); 5.2.2 Good Laboratory Practice (GLP); 5.2.3 Good Clinical Practice (GCP); 5.3 Weitere branchenspezifische und branchenunspezifische Qualitätsregelwerke; 5.3.1 DIN EN 45 001 ff und ISO/IEC Guideline 25; 5.3.2 HACCP; 5.3.3 Grundsätze ordnungsmäßiger Buchführung (GoB); 5.3.4 DIN EN IS0 9000 ff; 5.4 Spezifische Anforderungen an computergestützte Systeme
5.4.1 Ergänzende Leitlinien für computergestützte Systeme5.4.2 Good Automated Manufacturing Practice (GAMP); 5.4.3 OECD-GLP-Konsensdokument Nr. 10; 5.4.4 Good Automated Laboratory Practices (GALP); 5.4.5 21 CFR Part 11; 5.5 Richtlinien und Standards der Informationstechnologie; 5.5.1 IEEE-Standards; 5.5.2 ISO/IEC 9126; 5.5.3 DIN 66 285 und RAL; 5.5.4 IT-Sicherheitskriterien; 5.6 Zusammenfassung der Anforderungen; 6 Verantwortlichkeit und Organisation; 6.1 Verantwortlichkeiten; 6.1.1 Organisatorische Leitung (Management); 6.1.2 Fachliche Leitung; 6.1.3 Personal; 6.1.4 Qualitätssicherung
6.1.5 Archivverantwortlicher6.1.6 DV-Verantwortlicher; 6.1.7 Externe sachverständige Personen, Subunternehmer und Auftragslabors; 6.1.8 Hersteller, Entwickler oder Lieferanten von DV-Systemen; 6.2 Organisation; 6.2.1 Aufbauorganisation; 6.2.2 Ablauforganisation; 6.2.3 Organisation der Computervalidierung; 6.2.4 Betrieb der computergestützten Systeme; 6.3 Rechtliche Situation und Haftung; 6.4 Software-Entwicklungsverträge und Outsourcing; 7 Validierung unterschiedlicher Systeme; 7.1 Konstruktionsmerkmale von DV-Systemen; 7.2 LIMS; 7.2.1 Leistungsspektrum eines LlMS
7.2.2 Unvermeidbares Integritätsrisiko
Record Nr. UNINA-9910144381503321
Unkelbach H. D (Hans-Dieter)  
Weinheim, : Wiley-VCH, 1998
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Computervalidierung in labor und betrieb [[electronic resource] ] : sicherheit und qualität computergestützter systeme / / H.D. Unkelbach, P. Bosshard, H. Wolf
Computervalidierung in labor und betrieb [[electronic resource] ] : sicherheit und qualität computergestützter systeme / / H.D. Unkelbach, P. Bosshard, H. Wolf
Autore Unkelbach H. D (Hans-Dieter)
Pubbl/distr/stampa Weinheim, : Wiley-VCH, 1998
Descrizione fisica 1 online resource (338 p.)
Disciplina 629.895
Altri autori (Persone) BosshardP (Peter)
WolfH
Soggetto topico Computer programs - Verification
Computer software - Quality control
ISBN 1-282-02153-2
9786612021534
3-527-62456-2
3-527-62457-0
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione ger
Nota di contenuto Computervalidierung in Labor und Betrieb; Inhaltsverzeichnis; 1 Einleitung; 2 Grundlegende Begriffe und Konzepte; 2.1 Der Begriff ,, Validierung"; 2.2 Computervalidierung in der Anwendungspraxis; 2.3 Qualität von Information; 2.4 Qualität von Daten; 2.4.1 Korrektheit und Genauigkeit; 2.4.2 Gültigkeit und Authentizität; 2.4.3 Datenintegrität und Datensicherheit; 2.4.4 Vertraulichkeit; 2.4.5 Verfügbarkeit; 2.4.6 Bedeutung; 2.5 Qualität von Verfahren; 2.6 Validierung im Software-Lebenszyklus; 2.7 Maßnahmen zur Daten- und Programmsicherheit; 2.7.1 Datensicherungen; 2.7.2 Ersatzprozeduren
2.7.3 Physische Zugangskontrolle2.7.4 Logische Zugangskontrolle; 2.7.5 Virenschutz; 2.7.6 Kryptografische Verfahren; 3 Software-Entwicklung; 3.1 Phasenmodell; 3.2 Validierung in der Software-Entwicklung; 3.2.1 Reviews; 3.2.2 Statische Analysemethoden; 3.2.3 Tests; 3.3 Entwicklungsdokumentation; 3.4 Computer Aided Software Engineering (CASE); 3.5 Qualitätsmanagement in der Software-Entwicklung; 4 Betrieb computergestützter Systeme; 4.1 Installation und Installationstest; 4.2 Abnahme- und Akzeptanztest; 4.3 Validierungsplan; 4.4 Validierungsdokumentation; 4.5 Revalidierungen
4.6 Software-Lebenszyklus5 Validierungsanforderungen; 5.1 Gesetze, Verordnungen, Normen und Richtlinien; 5.2 Qualitätsregelwerke für chemisch-pharmazeutische Bereiche; 5.2.1 Good Manufacturing Practice (GMP); 5.2.2 Good Laboratory Practice (GLP); 5.2.3 Good Clinical Practice (GCP); 5.3 Weitere branchenspezifische und branchenunspezifische Qualitätsregelwerke; 5.3.1 DIN EN 45 001 ff und ISO/IEC Guideline 25; 5.3.2 HACCP; 5.3.3 Grundsätze ordnungsmäßiger Buchführung (GoB); 5.3.4 DIN EN IS0 9000 ff; 5.4 Spezifische Anforderungen an computergestützte Systeme
5.4.1 Ergänzende Leitlinien für computergestützte Systeme5.4.2 Good Automated Manufacturing Practice (GAMP); 5.4.3 OECD-GLP-Konsensdokument Nr. 10; 5.4.4 Good Automated Laboratory Practices (GALP); 5.4.5 21 CFR Part 11; 5.5 Richtlinien und Standards der Informationstechnologie; 5.5.1 IEEE-Standards; 5.5.2 ISO/IEC 9126; 5.5.3 DIN 66 285 und RAL; 5.5.4 IT-Sicherheitskriterien; 5.6 Zusammenfassung der Anforderungen; 6 Verantwortlichkeit und Organisation; 6.1 Verantwortlichkeiten; 6.1.1 Organisatorische Leitung (Management); 6.1.2 Fachliche Leitung; 6.1.3 Personal; 6.1.4 Qualitätssicherung
6.1.5 Archivverantwortlicher6.1.6 DV-Verantwortlicher; 6.1.7 Externe sachverständige Personen, Subunternehmer und Auftragslabors; 6.1.8 Hersteller, Entwickler oder Lieferanten von DV-Systemen; 6.2 Organisation; 6.2.1 Aufbauorganisation; 6.2.2 Ablauforganisation; 6.2.3 Organisation der Computervalidierung; 6.2.4 Betrieb der computergestützten Systeme; 6.3 Rechtliche Situation und Haftung; 6.4 Software-Entwicklungsverträge und Outsourcing; 7 Validierung unterschiedlicher Systeme; 7.1 Konstruktionsmerkmale von DV-Systemen; 7.2 LIMS; 7.2.1 Leistungsspektrum eines LlMS
7.2.2 Unvermeidbares Integritätsrisiko
Record Nr. UNINA-9910830240603321
Unkelbach H. D (Hans-Dieter)  
Weinheim, : Wiley-VCH, 1998
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Computervalidierung in labor und betrieb [[electronic resource] ] : sicherheit und qualität computergestützter systeme / / H.D. Unkelbach, P. Bosshard, H. Wolf
Computervalidierung in labor und betrieb [[electronic resource] ] : sicherheit und qualität computergestützter systeme / / H.D. Unkelbach, P. Bosshard, H. Wolf
Autore Unkelbach H. D (Hans-Dieter)
Pubbl/distr/stampa Weinheim, : Wiley-VCH, 1998
Descrizione fisica 1 online resource (338 p.)
Disciplina 629.895
Altri autori (Persone) BosshardP (Peter)
WolfH
Soggetto topico Computer programs - Verification
Computer software - Quality control
ISBN 1-282-02153-2
9786612021534
3-527-62456-2
3-527-62457-0
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione ger
Nota di contenuto Computervalidierung in Labor und Betrieb; Inhaltsverzeichnis; 1 Einleitung; 2 Grundlegende Begriffe und Konzepte; 2.1 Der Begriff ,, Validierung"; 2.2 Computervalidierung in der Anwendungspraxis; 2.3 Qualität von Information; 2.4 Qualität von Daten; 2.4.1 Korrektheit und Genauigkeit; 2.4.2 Gültigkeit und Authentizität; 2.4.3 Datenintegrität und Datensicherheit; 2.4.4 Vertraulichkeit; 2.4.5 Verfügbarkeit; 2.4.6 Bedeutung; 2.5 Qualität von Verfahren; 2.6 Validierung im Software-Lebenszyklus; 2.7 Maßnahmen zur Daten- und Programmsicherheit; 2.7.1 Datensicherungen; 2.7.2 Ersatzprozeduren
2.7.3 Physische Zugangskontrolle2.7.4 Logische Zugangskontrolle; 2.7.5 Virenschutz; 2.7.6 Kryptografische Verfahren; 3 Software-Entwicklung; 3.1 Phasenmodell; 3.2 Validierung in der Software-Entwicklung; 3.2.1 Reviews; 3.2.2 Statische Analysemethoden; 3.2.3 Tests; 3.3 Entwicklungsdokumentation; 3.4 Computer Aided Software Engineering (CASE); 3.5 Qualitätsmanagement in der Software-Entwicklung; 4 Betrieb computergestützter Systeme; 4.1 Installation und Installationstest; 4.2 Abnahme- und Akzeptanztest; 4.3 Validierungsplan; 4.4 Validierungsdokumentation; 4.5 Revalidierungen
4.6 Software-Lebenszyklus5 Validierungsanforderungen; 5.1 Gesetze, Verordnungen, Normen und Richtlinien; 5.2 Qualitätsregelwerke für chemisch-pharmazeutische Bereiche; 5.2.1 Good Manufacturing Practice (GMP); 5.2.2 Good Laboratory Practice (GLP); 5.2.3 Good Clinical Practice (GCP); 5.3 Weitere branchenspezifische und branchenunspezifische Qualitätsregelwerke; 5.3.1 DIN EN 45 001 ff und ISO/IEC Guideline 25; 5.3.2 HACCP; 5.3.3 Grundsätze ordnungsmäßiger Buchführung (GoB); 5.3.4 DIN EN IS0 9000 ff; 5.4 Spezifische Anforderungen an computergestützte Systeme
5.4.1 Ergänzende Leitlinien für computergestützte Systeme5.4.2 Good Automated Manufacturing Practice (GAMP); 5.4.3 OECD-GLP-Konsensdokument Nr. 10; 5.4.4 Good Automated Laboratory Practices (GALP); 5.4.5 21 CFR Part 11; 5.5 Richtlinien und Standards der Informationstechnologie; 5.5.1 IEEE-Standards; 5.5.2 ISO/IEC 9126; 5.5.3 DIN 66 285 und RAL; 5.5.4 IT-Sicherheitskriterien; 5.6 Zusammenfassung der Anforderungen; 6 Verantwortlichkeit und Organisation; 6.1 Verantwortlichkeiten; 6.1.1 Organisatorische Leitung (Management); 6.1.2 Fachliche Leitung; 6.1.3 Personal; 6.1.4 Qualitätssicherung
6.1.5 Archivverantwortlicher6.1.6 DV-Verantwortlicher; 6.1.7 Externe sachverständige Personen, Subunternehmer und Auftragslabors; 6.1.8 Hersteller, Entwickler oder Lieferanten von DV-Systemen; 6.2 Organisation; 6.2.1 Aufbauorganisation; 6.2.2 Ablauforganisation; 6.2.3 Organisation der Computervalidierung; 6.2.4 Betrieb der computergestützten Systeme; 6.3 Rechtliche Situation und Haftung; 6.4 Software-Entwicklungsverträge und Outsourcing; 7 Validierung unterschiedlicher Systeme; 7.1 Konstruktionsmerkmale von DV-Systemen; 7.2 LIMS; 7.2.1 Leistungsspektrum eines LlMS
7.2.2 Unvermeidbares Integritätsrisiko
Record Nr. UNINA-9910840634903321
Unkelbach H. D (Hans-Dieter)  
Weinheim, : Wiley-VCH, 1998
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Experimental validation of clock synchronization algorithms / / Daniel L. Palumbo, R. Lynn Graham
Experimental validation of clock synchronization algorithms / / Daniel L. Palumbo, R. Lynn Graham
Autore Palumbo Daniel L.
Pubbl/distr/stampa Washington, DC : , : National Aeronautics and Space Administration, Office of Management, Scientific and Technical Information Program, , [July 1992]
Descrizione fisica 1 online resource (approximately 26 pages) : illustrations
Collana NASA/TP
Soggetto topico Proving
Computer systems programs
Data processing
Synchronization
Electronic data processing - Distributed processing
Computer programs - Validation
Computer programs - Verification
Real-time data processing
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Record Nr. UNINA-9910717004303321
Palumbo Daniel L.  
Washington, DC : , : National Aeronautics and Space Administration, Office of Management, Scientific and Technical Information Program, , [July 1992]
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Formal methods for industrial critical systems : 26th international conference, FMICS 2021, Paris, France, August 24-26, 2021 : proceedings / / Alberto Lluch Lafuente, Anastasia Mavridou (editors)
Formal methods for industrial critical systems : 26th international conference, FMICS 2021, Paris, France, August 24-26, 2021 : proceedings / / Alberto Lluch Lafuente, Anastasia Mavridou (editors)
Pubbl/distr/stampa Cham, Switzerland : , : Springer, , [2021]
Descrizione fisica 1 online resource (253 pages)
Disciplina 004.0151
Collana Lecture Notes in Computer Science
Soggetto topico Formal methods (Computer science)
Software engineering
Computer programs - Verification
ISBN 3-030-85248-2
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Intro -- Preface -- Organization -- Haunting Tales of Applied Formal Methods from Academia and Industry (Abstract of Invited Talk) -- Contents -- Verification -- Verification of Co-simulation Algorithms Subject to Algebraic Loops and Adaptive Steps -- 1 Introduction -- 2 Background -- 2.1 Simulation Units -- 2.2 Co-simulation Algorithms -- 2.3 Correct Co-simulation Algorithms -- 3 Related Work -- 4 Verifying Complex Co-simulation Algorithms -- 4.1 Verifying an Algorithm Using UPPAAL -- 4.2 Verifying Complex Simulation Scenarios in UPPAAL -- 4.3 Debugging Algorithm Errors -- 5 Validation -- 5.1 Motivation Example -- 5.2 Complex Scenario -- 6 Concluding Remarks -- References -- Automated Verification of Temporal Properties of Ladder Programs -- 1 Introduction -- 2 Introduction to Ladder Programming -- 3 Translation of Ladder Programs to WhyML -- 3.1 The Why3 Environment -- 3.2 Translation of Ladder Codes -- 3.3 The Ladder Loop, and the Encoding of Timing Charts -- 4 Implementation and Experimental Results -- 4.1 Overview of the Approach -- 4.2 Results on Correct Code -- 4.3 Results on Incorrect Code -- 5 Discussions, Related Work and Future Work -- References -- Spatial Model Checking for Smart Stations -- 1 Introduction and Outline -- 2 Industrial Context and Case Study: Station Lighting -- 3 Challenges in User-Centric Design of Smart Stations -- 4 Methodology -- 4.1 Spatial Model Checking -- 4.2 Statistical Spatio-Temporal Model Checking -- 5 Conclusion and Outlook -- References -- Program Safety and Education -- Parametric Faults in Safety Critical Programs -- 1 Introduction -- 2 Background -- 3 Identifying Incorrect Parameters -- 4 Case Study -- 5 Discussion -- 6 Related Works -- 7 Conclusion -- References -- Modular Transformation of Java Exceptions Modulo Errors -- 1 Introduction -- 2 Background -- 2.1 Abrupt Termination -- 2.2 VerCors.
3 Related Work -- 4 Semantics of Exceptions -- 4.1 Errors and Sources of Errors -- 4.2 Ideal Semantics -- 4.3 Semantics Modulo Errors -- 5 The finally Encoding Problem -- 5.1 Candidate Encodings -- 6 Evaluation -- 6.1 Common Exception Patterns in Commercial Software -- 6.2 Verification with VerCors -- 7 Discussion -- 7.1 Backend Requirements -- 7.2 Performance -- 8 Conclusion -- References -- On Education and Training in Formal Methods for Industrial Critical Systems -- 1 Introduction -- 2 Terminology -- 3 Roles in Formal Methods for Industrial Critical Systems: [Engineer] and [Engineer] -- 3.1 FMICS Roles and Activities -- 3.2 Consequences on Education and Training -- 4 Learning Objectives: vs. -- 5 Curriculum and Course Construction -- 6 Exemplary Implementation -- 7 Conclusion -- References -- (Event-)B Modeling and Validation -- Improving SMT Solver Integrations for the Validation of B and Event-B Models -- 1 Introduction -- 2 Former Z3 Integration -- 2.1 High-Level Translation -- 2.2 Workflow -- 3 New Z3 Integration -- 3.1 High-Level Translation -- 3.2 New Workflow -- 4 Empirical Evaluation -- 4.1 Weaknesses of the Integration of Z3 -- 4.2 Strengths of the Integration of Z3 -- 4.3 Symbolic Model Checking -- 5 Related Work -- 6 Future Work -- 7 Conclusion -- References -- Standard Conformance-by-Construction with Event-B -- 1 Introduction -- 2 Certification and Conformance -- 3 Event-B -- 3.1 Contexts and Machines (Tables1b and 1c) -- 3.2 Event-B Extensions with Theories -- 4 Case Study: ARINC 661 + Multi-purpose Interactive Application -- 4.1 ARINC 661 Standard Specification: An Extract -- 4.2 Multi-purpose Interactive Application and Weather Radar System -- 5 Standards Formalised as Ontologies ((1) on Fig.2) -- 6 Our Approach -- 6.1 Domain Standards as Ontology-Based Theories ((2) on Fig.2) -- 6.2 Standard Theory Instantiation ((3) on Fig.2).
6.3 Model Annotation for Conformance ((4) on Fig.2) -- 7 Standard Conformance-by-Construction: The Case of ARINC 661 -- 7.1 ARINC 661 Standard Formalisation ((2) on Fig.2) -- 7.2 System-Specific Concepts Describing WXR Widgets ((3) on Fig.2) -- 7.3 Annotated Event-B Model of WXR Application ((4) on Fig.2) -- 8 Assessment -- 9 Conclusion -- References -- Formal Analysis -- Randomized Reachability Analysis in Uppaal: Fast Error Detection in Timed Systems -- 1 Introduction -- 2 Randomized Reachability Analysis -- 3 New Results on Herschel-Planck -- 4 More Schedulability -- 5 Gossiping Girls -- 6 Scalability Experiments -- 7 Conclusion -- 8 Future Work -- References -- Verifying the Mathematical Library of an UAV Autopilot with Frama-C -- 1 Introduction -- 2 The Paparazzi Autopilot -- 3 Proving the Absence of Runtime Errors -- 4 Functional Verification Using Automatic Provers -- 5 Functional Verification Using Interactive Provers -- 6 Conclusion -- References -- Formal Analysis of the UNISIG Safety Application Intermediate Sub-layer -- 1 Introduction -- 2 Background -- 3 The Model -- 4 The Analysis -- 5 Conclusion -- References -- Tools -- ProB2-UI: A Java-Based User Interface for ProB -- 1 Introduction and Motivation -- 2 Features of ProB2-UI -- 3 Related Work -- 4 Conclusion -- References -- Intrepid: A Scriptable and Cloud-Ready SMT-Based Model Checker -- 1 Introduction -- 2 Constructing Models -- 2.1 Translating Industrially-Relevant Models -- 3 Simulating Models -- 4 Model Checking -- 4.1 A Comparison of the Engines -- 5 Sample Applications -- 5.1 Equivalence Checking for Clock-Gating -- 5.2 Automated Test Generation of MC/DC -- 6 A REST API for Model Checking -- 7 Conclusion -- References -- Merit and Blame Assignment with Kind 2 -- 1 Introduction -- 2 Running Example -- 3 The New Features -- 4 Implementation Details -- References.
Test Generation and Probabilistic Verification -- PSY-TaLiRo: A Python Toolbox for Search-Based Test Generation for Cyber-Physical Systems -- 1 Introduction -- 2 Architecture -- 3 Interface -- 3.1 System Under Test (SUT) -- 3.2 Specifications -- 3.3 Optimizers -- 3.4 Options -- 4 Examples -- 4.1 MATLAB/Simulink -- 4.2 PX4 -- 5 Conclusions -- References -- Probabilistic Verification for Reliability of a Two-by-Two Network-on-Chip System -- 1 Introduction -- 2 Motivation -- 3 Concrete Formal Model for NoC -- 4 Need for Abstraction -- 4.1 Predicate Abstraction to Simplify Complex Data Structures -- 4.2 Probabilistic Choice Abstraction -- 4.3 Boolean Queue Abstraction -- 5 Results -- 5.1 Every Other Cycle Flit Injection -- 5.2 Burst Flit Injection -- 5.3 Minimizing PSN with Flit Generation Pattern -- 5.4 Results Summary and Discussion -- 6 Conclusion -- References -- Author Index.
Record Nr. UNISA-996464384103316
Cham, Switzerland : , : Springer, , [2021]
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui