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)
Formal method : industrial use from model to the code / / editor, Jean-Louis Boulanger
Formal method : industrial use from model to the code / / editor, Jean-Louis Boulanger
Pubbl/distr/stampa London : , : ISTE
Descrizione fisica 1 online resource (376 pages)
Disciplina 385.0285/53
Altri autori (Persone) BoulangerJean-Louis
Collana Industrial implementation of formal methods series
Soggetto topico Railroads - Management - Data processing
Formal methods (Computer science)
Application software - Development
ISBN 1-118-61437-2
1-118-56189-9
1-299-31507-0
1-118-61438-0
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto From classic languages to formal methods -- Formal method in railway, the first complex application : SAET-METEOR -- B method and B tools -- Model-based design using Simulink : modeling, code generation, verification, and validation -- Proof of global properties with the aid of the Simulink Design verifier proof tool -- SCADE : implementation and applications -- GATel : a V & V platform for scade models -- Control build.
Record Nr. UNINA-9910139052403321
London : , : ISTE
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Formal method : industrial use from model to the code / / editor, Jean-Louis Boulanger
Formal method : industrial use from model to the code / / editor, Jean-Louis Boulanger
Edizione [1st ed.]
Pubbl/distr/stampa London : , : ISTE
Descrizione fisica 1 online resource (376 pages)
Disciplina 385.0285/53
Altri autori (Persone) BoulangerJean-Louis
Collana Industrial implementation of formal methods series
Soggetto topico Railroads - Management - Data processing
Formal methods (Computer science)
Application software - Development
ISBN 1-118-61437-2
1-118-56189-9
1-299-31507-0
1-118-61438-0
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto From classic languages to formal methods -- Formal method in railway, the first complex application : SAET-METEOR -- B method and B tools -- Model-based design using Simulink : modeling, code generation, verification, and validation -- Proof of global properties with the aid of the Simulink Design verifier proof tool -- SCADE : implementation and applications -- GATel : a V & V platform for scade models -- Control build.
Record Nr. UNINA-9910820783003321
London : , : ISTE
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Formal methods applied to complex systems : implementation of the B method / / edited by Jean-Louis Boulanger
Formal methods applied to complex systems : implementation of the B method / / edited by Jean-Louis Boulanger
Pubbl/distr/stampa London, England ; ; Hoboken, New Jersey : , : iSTE : , : Wiley, , 2014
Descrizione fisica 1 online resource (512 p.)
Disciplina 005.1
Collana Computer Engineering Series
Soggetto topico B method (Computer science)
Formal methods (Computer science)
ISBN 1-119-00292-3
1-119-00272-9
1-119-00268-0
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Cover; Title Page; Copyright; Contents; Introduction; Chapter 1: Presentation of the B Method ; 1.1. Introduction; 1.2. The B method; 1.2.1. Presentation; 1.2.2. The concept of an abstract machine; 1.2.2.1. Abstract machine; 1.2.2.2. Declarative part; 1.2.2.3. Composition part; 1.2.2.4. Executive part; 1.2.3. From machines to implementations; 1.2.3.1. Principle; 1.2.3.2. Refinement; 1.2.3.3. Process; 1.3. Verification and validation (V&V); 1.3.1. Internal verification; 1.3.1.1. Principles; 1.3.1.2. Syntactic and semantic analysis; 1.3.1.3. Generation of proof obligations
1.3.2. Validation or external verification1.4. Methodology; 1.4.1. Development by layer; 1.4.2. Role of the breakdown in the makeup of the POs; 1.4.3. Development cycle of a B project; 1.5. Feedback based on experience; 1.5.1. A few figures; 1.5.2. Some uses; 1.5.2.1. The current situation; 1.5.2.2. SAET-METEOR; 1.5.2.3. VAL CdG; 1.5.2.4. Eurobalise coder; 1.6. Conclusion; 1.7. Glossary; 1.8. Bibliography; Chapter 2: Atelier B; 2.1. Introduction; 2.2. Automatic refinement; 2.3. Code generation; 2.4. Proof and model animation; 2.5. The move toward open source; 2.6. Glossary; 2.7. Bibliography
Chapter 3: B Tools3.1. Introduction; 3.2. General principles; 3.3. Atelier B; 3.3.1. Project management; 3.3.2. Typechecking and PO generation; 3.3.2.1. Typechecking; 3.3.2.2. PO generation; 3.3.3. Code generation; 3.3.3.1. Verification of B0; 3.3.3.2. Code generation; 3.3.4. Prover; 3.3.4.1. Automatic prover; 3.3.4.2. Principles of proof in interactive mode; 3.3.4.3. Implementation of proof in interactive mode; 3.3.5. Tool qualification; 3.4. Open source tools; 3.4.1. Presentation; 3.4.2. ABTools; 3.4.2.1. Presentation; 3.4.2.2. The ANTLR compiler generator; 3.4.2.3. The ABTools environment
3.4.2.3.1. Presentation3.4.2.3.2. Lexical and syntactic analysis; 3.4.2.3.3. Tree manipulation; 3.4.2.3.4. Generation of POs; 3.4.2.4. Scalability; 3.4.2.4.1. Classic B; 3.4.2.4.2. B Prime; 3.4.2.4.3. System B; 3.4.2.4.4. Event B; 3.4.2.5. Results; 3.5. Conclusion; 3.6. Glossary; 3.7. Bibliography; Chapter 4: The B Method at Siemens; 4.1. Introduction; 4.1.1. Siemens Industry Mobility; 4.1.2. The CBTC system3; 4.1.3. Characteristics of B programs; 4.1.4. The target calculator; 4.2. The development process using B; 4.2.1. Development; 4.2.2. Informal specification
4.2.3. Formalization of the specification4.2.3.1. General principles; 4.2.3.2. Cutting machines; 4.2.3.3. Architecture of the abstract model and the decomposition approach; 4.2.4. Refinement and coding; 4.2.4.1. General principles; 4.2.4.2. Stages in the refinement process; 4.2.4.3. Loops and abstract iteration; 4.2.4.4. Data refinement; 4.2.5. Proof; 4.2.5.1. General principles; 4.2.5.2. Proof in practice; 4.2.5.3. Ease of proof; 4.3. Monitoring; 4.3.1. Development review; 4.3.1.1. Review objectives; 4.3.1.2. Initiation criteria; 4.3.2. Testing; 4.3.3. Safety validation
4.3.3.1. Specification analysis
Record Nr. UNINA-9910132183003321
London, England ; ; Hoboken, New Jersey : , : iSTE : , : Wiley, , 2014
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Formal methods applied to complex systems / / edited by Jean-Louis Boulanger
Formal methods applied to complex systems / / edited by Jean-Louis Boulanger
Pubbl/distr/stampa London, [England] ; ; Hoboken, New Jersey : , : ISTE : , : Wiley, , 2014
Descrizione fisica 1 online resource (478 p.)
Disciplina 620.00420285
Collana Computer Engineering Series
Soggetto topico Computer-aided design
Computer engineering
Systems engineering
ISBN 1-119-00477-2
1-119-00470-5
1-119-00484-5
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Cover; Title Page ; Copyright; Contents; Introduction; Chapter 1. Formal Description and Modeling of Risks; 1.1. Introduction; 1.2. Standard process; 1.2.1. Risks, undesirable events and accidents; 1.2.2. Usual process; 1.2.3. Formal software processes for safety-critical systems; 1.2.4. Formal methods for safety-critical systems; 1.2.5. Safety kernel; 1.3. Methodology; 1.3.1. Presentation; 1.3.2. Risk mastery process; 1.4. Case study; 1.4.1. Rail transport system; 1.4.2. Presentation; 1.4.3. Description of the environment; 1.4.4. Definition of side-on collision; 1.4.5. Risk analysis
1.5. Implementation 1.5.1. The B method; 1.5.2. Implementation; 1.5.3. Specification of the rail transport system and side-on collision; 1.6. Conclusion; 1.7. Glossary; 1.8. Bibliography; Chapter 2. An Innovative Approach and an Adventure in Rail Safety; 2.1. Introduction; 2.2. Open Control of Train Interchangeable and Integrated System; 2.3. Computerized interlocking systems; 2.4. Conclusion; 2.5. Glossary; 2.6. Bibliography; Chapter 3. Use of Formal Proof for Cbtc (Octys); 3.1. Introduction; 3.2. Presentation of the Open Control of Train Interchangeable and Integrated System CBTC
3.2.1. Open Control of Train Interchangeable and Integrated System 3.2.2. Purpose of CBTC; 3.2.3. CBTC architectures; 3.3. Zone control equipment; 3.3.1. Presentation; 3.3.2. SCADE model; 3.4. Implementation of the solution; 3.5. Technical solution and implementation; 3.5.1. Property definition; 3.5.2. Two basic principles of property definition; 3.5.3. Test topologies; 3.5.4. Initial analyses; 3.5.5. The property treatment process; 3.5.6. Non-regression; 3.6. Results; 3.7. Possible improvements; 3.8. Conclusion; 3.9. Glossary; 3.10. Bibliography
Chapter 4. Safety Demonstration for A Rail Signaling Application in Nominal and Degraded Modes Using Formal Proof 4.1. Introduction; 4.1.1. Context; 4.2. Case description; 4.2.1. Operational architecture of the PMI system; 4.2.2. CIM subsystem; 4.2.3. CIM program verification with and without proof; 4.2.4. Scope of verification; 4.3. Modeling the whole system; 4.3.1. Application model; 4.3.2. Safety properties; 4.3.3. Environment model; 4.4. Formal proof suite; 4.4.1. Modeling the system; 4.4.2. Non-certified analysis chain; 4.4.3. The certified analysis chain
4.4.4. Assessment of the proof suite 4.5. Application; 4.6. Results of our experience; 4.6.1. Environment modeling; 4.6.2. Proof vs. testing; 4.6.3. Limitations; 4.7. Conclusion and prospects; 4.8. Glossary; 4.9. Bibliography; Chapter 5. Formal Verification of Data for Parameterized Systems; 5.1. Introduction; 5.1.1. Systerel; 5.1.2. Data verification; 5.1.3. Parameterized systems; 5.2. Data in the development cycle; 5.2.1. Data and property identification; 5.2.2. Modeling; 5.2.3. Property validation; 5.2.4. Data production; 5.2.5. Property verification using data; 5.2.6. Data integration
5.3. Data verification
Record Nr. UNINA-9910132203503321
London, [England] ; ; Hoboken, New Jersey : , : ISTE : , : Wiley, , 2014
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Formal methods applied to complex systems / / edited by Jean-Louis Boulanger
Formal methods applied to complex systems / / edited by Jean-Louis Boulanger
Pubbl/distr/stampa London, [England] ; ; Hoboken, New Jersey : , : ISTE : , : Wiley, , 2014
Descrizione fisica 1 online resource (478 p.)
Disciplina 620.00420285
Collana Computer Engineering Series
Soggetto topico Computer-aided design
Computer engineering
Systems engineering
ISBN 1-119-00477-2
1-119-00470-5
1-119-00484-5
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Cover; Title Page ; Copyright; Contents; Introduction; Chapter 1. Formal Description and Modeling of Risks; 1.1. Introduction; 1.2. Standard process; 1.2.1. Risks, undesirable events and accidents; 1.2.2. Usual process; 1.2.3. Formal software processes for safety-critical systems; 1.2.4. Formal methods for safety-critical systems; 1.2.5. Safety kernel; 1.3. Methodology; 1.3.1. Presentation; 1.3.2. Risk mastery process; 1.4. Case study; 1.4.1. Rail transport system; 1.4.2. Presentation; 1.4.3. Description of the environment; 1.4.4. Definition of side-on collision; 1.4.5. Risk analysis
1.5. Implementation 1.5.1. The B method; 1.5.2. Implementation; 1.5.3. Specification of the rail transport system and side-on collision; 1.6. Conclusion; 1.7. Glossary; 1.8. Bibliography; Chapter 2. An Innovative Approach and an Adventure in Rail Safety; 2.1. Introduction; 2.2. Open Control of Train Interchangeable and Integrated System; 2.3. Computerized interlocking systems; 2.4. Conclusion; 2.5. Glossary; 2.6. Bibliography; Chapter 3. Use of Formal Proof for Cbtc (Octys); 3.1. Introduction; 3.2. Presentation of the Open Control of Train Interchangeable and Integrated System CBTC
3.2.1. Open Control of Train Interchangeable and Integrated System 3.2.2. Purpose of CBTC; 3.2.3. CBTC architectures; 3.3. Zone control equipment; 3.3.1. Presentation; 3.3.2. SCADE model; 3.4. Implementation of the solution; 3.5. Technical solution and implementation; 3.5.1. Property definition; 3.5.2. Two basic principles of property definition; 3.5.3. Test topologies; 3.5.4. Initial analyses; 3.5.5. The property treatment process; 3.5.6. Non-regression; 3.6. Results; 3.7. Possible improvements; 3.8. Conclusion; 3.9. Glossary; 3.10. Bibliography
Chapter 4. Safety Demonstration for A Rail Signaling Application in Nominal and Degraded Modes Using Formal Proof 4.1. Introduction; 4.1.1. Context; 4.2. Case description; 4.2.1. Operational architecture of the PMI system; 4.2.2. CIM subsystem; 4.2.3. CIM program verification with and without proof; 4.2.4. Scope of verification; 4.3. Modeling the whole system; 4.3.1. Application model; 4.3.2. Safety properties; 4.3.3. Environment model; 4.4. Formal proof suite; 4.4.1. Modeling the system; 4.4.2. Non-certified analysis chain; 4.4.3. The certified analysis chain
4.4.4. Assessment of the proof suite 4.5. Application; 4.6. Results of our experience; 4.6.1. Environment modeling; 4.6.2. Proof vs. testing; 4.6.3. Limitations; 4.7. Conclusion and prospects; 4.8. Glossary; 4.9. Bibliography; Chapter 5. Formal Verification of Data for Parameterized Systems; 5.1. Introduction; 5.1.1. Systerel; 5.1.2. Data verification; 5.1.3. Parameterized systems; 5.2. Data in the development cycle; 5.2.1. Data and property identification; 5.2.2. Modeling; 5.2.3. Property validation; 5.2.4. Data production; 5.2.5. Property verification using data; 5.2.6. Data integration
5.3. Data verification
Record Nr. UNINA-9910825168103321
London, [England] ; ; Hoboken, New Jersey : , : ISTE : , : Wiley, , 2014
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Formal methods applied to complex systems : implementation of the B method / / edited by Jean-Louis Boulanger
Formal methods applied to complex systems : implementation of the B method / / edited by Jean-Louis Boulanger
Pubbl/distr/stampa London, England ; ; Hoboken, New Jersey : , : iSTE : , : Wiley, , 2014
Descrizione fisica 1 online resource (512 p.)
Disciplina 005.1
Collana Computer Engineering Series
Soggetto topico B method (Computer science)
Formal methods (Computer science)
ISBN 1-119-00292-3
1-119-00272-9
1-119-00268-0
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Cover; Title Page; Copyright; Contents; Introduction; Chapter 1: Presentation of the B Method ; 1.1. Introduction; 1.2. The B method; 1.2.1. Presentation; 1.2.2. The concept of an abstract machine; 1.2.2.1. Abstract machine; 1.2.2.2. Declarative part; 1.2.2.3. Composition part; 1.2.2.4. Executive part; 1.2.3. From machines to implementations; 1.2.3.1. Principle; 1.2.3.2. Refinement; 1.2.3.3. Process; 1.3. Verification and validation (V&V); 1.3.1. Internal verification; 1.3.1.1. Principles; 1.3.1.2. Syntactic and semantic analysis; 1.3.1.3. Generation of proof obligations
1.3.2. Validation or external verification1.4. Methodology; 1.4.1. Development by layer; 1.4.2. Role of the breakdown in the makeup of the POs; 1.4.3. Development cycle of a B project; 1.5. Feedback based on experience; 1.5.1. A few figures; 1.5.2. Some uses; 1.5.2.1. The current situation; 1.5.2.2. SAET-METEOR; 1.5.2.3. VAL CdG; 1.5.2.4. Eurobalise coder; 1.6. Conclusion; 1.7. Glossary; 1.8. Bibliography; Chapter 2: Atelier B; 2.1. Introduction; 2.2. Automatic refinement; 2.3. Code generation; 2.4. Proof and model animation; 2.5. The move toward open source; 2.6. Glossary; 2.7. Bibliography
Chapter 3: B Tools3.1. Introduction; 3.2. General principles; 3.3. Atelier B; 3.3.1. Project management; 3.3.2. Typechecking and PO generation; 3.3.2.1. Typechecking; 3.3.2.2. PO generation; 3.3.3. Code generation; 3.3.3.1. Verification of B0; 3.3.3.2. Code generation; 3.3.4. Prover; 3.3.4.1. Automatic prover; 3.3.4.2. Principles of proof in interactive mode; 3.3.4.3. Implementation of proof in interactive mode; 3.3.5. Tool qualification; 3.4. Open source tools; 3.4.1. Presentation; 3.4.2. ABTools; 3.4.2.1. Presentation; 3.4.2.2. The ANTLR compiler generator; 3.4.2.3. The ABTools environment
3.4.2.3.1. Presentation3.4.2.3.2. Lexical and syntactic analysis; 3.4.2.3.3. Tree manipulation; 3.4.2.3.4. Generation of POs; 3.4.2.4. Scalability; 3.4.2.4.1. Classic B; 3.4.2.4.2. B Prime; 3.4.2.4.3. System B; 3.4.2.4.4. Event B; 3.4.2.5. Results; 3.5. Conclusion; 3.6. Glossary; 3.7. Bibliography; Chapter 4: The B Method at Siemens; 4.1. Introduction; 4.1.1. Siemens Industry Mobility; 4.1.2. The CBTC system3; 4.1.3. Characteristics of B programs; 4.1.4. The target calculator; 4.2. The development process using B; 4.2.1. Development; 4.2.2. Informal specification
4.2.3. Formalization of the specification4.2.3.1. General principles; 4.2.3.2. Cutting machines; 4.2.3.3. Architecture of the abstract model and the decomposition approach; 4.2.4. Refinement and coding; 4.2.4.1. General principles; 4.2.4.2. Stages in the refinement process; 4.2.4.3. Loops and abstract iteration; 4.2.4.4. Data refinement; 4.2.5. Proof; 4.2.5.1. General principles; 4.2.5.2. Proof in practice; 4.2.5.3. Ease of proof; 4.3. Monitoring; 4.3.1. Development review; 4.3.1.1. Review objectives; 4.3.1.2. Initiation criteria; 4.3.2. Testing; 4.3.3. Safety validation
4.3.3.1. Specification analysis
Record Nr. UNINA-9910828908603321
London, England ; ; Hoboken, New Jersey : , : iSTE : , : Wiley, , 2014
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Industrial used of formal method [[electronic resource] ] : formal verification / / edited by Jean-Louis Boulanger
Industrial used of formal method [[electronic resource] ] : formal verification / / edited by Jean-Louis Boulanger
Pubbl/distr/stampa London, : ISTE
Descrizione fisica 1 online resource (307 p.)
Disciplina 005.101
620.0042
Altri autori (Persone) BoulangerJean-Louis
Collana ISTE
Soggetto topico Systems engineering - Data processing
Computer simulation
Formal methods (Computer science)
Computer software - Verification
Nondestructive testing
Soggetto genere / forma Electronic books.
ISBN 1-118-58784-7
1-118-56182-1
1-299-18707-2
1-118-58790-1
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Cover; Title; Copyright; Table of Contents; Introduction; Chapter 1. SPARK - A Language and Tool-Set for High-Integrity Software Development; 1.1. Introduction; 1.2. An overview of SPARK; 1.2.1. What is SPARK?; 1.3. The rationale behind SPARK; 1.3.1. Flow analysis; 1.3.2. Code proof; 1.3.3. Correctness by construction; 1.4. Industrial applications of SPARK; 1.4.1. SHOLIS; 1.4.2. Lockheed-Martin C-130J mission computer; 1.4.3. MULTOS CA; 1.4.4. Tokeneer; 1.4.5. Aircraft monitoring software; 1.4.6. iFACTS; 1.4.7. SPARK Skein; 1.5. Conclusion; 1.6. Bibliography
Chapter 2. Model-Based Testing Automatic Generationof Test Cases Using the Markov Chain Model2.1. Preliminaries on the test process; 2.1.1. Findings; 2.1.2. Test optimization; 2.1.3. The statistical usage test; 2.1.4. Generating test cases; 2.2. Modeling using Markov chains; 2.2.1. Origin; 2.2.2. Mathematical formalization; 2.2.3. Principles of generation; 2.2.4. Some indicators; 2.2.5. Calculating reliability; 2.3. The MaTeLo tool; 2.3.1. Engineering tests directed by models,model-based testing; 2.3.2. A chain of tools; 2.3.3. The usage model; 2.3.4. Configuration of test strategies
2.3.5. Generating test campaigns2.3.6. Analysis of the results and indicators; 2.4. Examples of industrial applications; 2.4.1. AUDI; 2.4.2. Magneti marelli; 2.4.3. Other industrial applications; 2.4.4. Industrialization of the tests; 2.5. Conclusion; 2.6. Bibliography; Chapter 3. Safety Analysis of the Embedded Systems with the AltaRica Approach; 3.1. Introduction; 3.2. Safety analysis of embedded systems; 3.3. AltaRica language and tools; 3.3.1. The AltaRica language; 3.3.2. Modeling the propagation of failures with AltaRica; 3.3.3. Tools associated with AltaRica
3.4. Examples of modeling and safety analysis3.4.1. Integrated modular avionics architecture; 3.4.2. System of electric power generation and distribution; 3.5. Comparison with other approaches; 3.5.1. Some precursors; 3.5.2. Tools for preexisting formal languages; 3.5.3. Languages for physical systems; 3.5.4. Injecting faults in nominal models; 3.6. Conclusion; 3.6.1. An approach to assess the safetyof systems tested in aeronautics; 3.6.2. Clarification of the system architectureand horizontal exploration of the failure propagation:impacts on the scope of analyses
3.6.3. Clarification of the nominal system characteristics:impacts on the generic definitions of the failure modes3.6.4. Compositional models of failure propagation:impacts on the overall safety process; 3.7. Special thanks; 3.8. Bibliography; Chapter 4. Polyspace®; 4.1. Overview; 4.2. Introduction to software quality and verification procedures; 4.3. Static analysis; 4.4. Dynamic tests; 4.5. Abstract interpretation; 4.6. Code verification; 4.7. Robustness verification or contextual verification; 4.7.1. Robustness verification; 4.7.2. Contextual verification
4.8. Examples of Polyspace® results
Record Nr. UNINA-9910141475603321
London, : ISTE
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Industrial used of formal method [[electronic resource] ] : formal verification / / edited by Jean-Louis Boulanger
Industrial used of formal method [[electronic resource] ] : formal verification / / edited by Jean-Louis Boulanger
Pubbl/distr/stampa London, : ISTE
Descrizione fisica 1 online resource (307 p.)
Disciplina 005.101
620.0042
Altri autori (Persone) BoulangerJean-Louis
Collana ISTE
Soggetto topico Systems engineering - Data processing
Computer simulation
Formal methods (Computer science)
Computer software - Verification
Nondestructive testing
ISBN 1-118-58784-7
1-118-56182-1
1-299-18707-2
1-118-58790-1
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Cover; Title; Copyright; Table of Contents; Introduction; Chapter 1. SPARK - A Language and Tool-Set for High-Integrity Software Development; 1.1. Introduction; 1.2. An overview of SPARK; 1.2.1. What is SPARK?; 1.3. The rationale behind SPARK; 1.3.1. Flow analysis; 1.3.2. Code proof; 1.3.3. Correctness by construction; 1.4. Industrial applications of SPARK; 1.4.1. SHOLIS; 1.4.2. Lockheed-Martin C-130J mission computer; 1.4.3. MULTOS CA; 1.4.4. Tokeneer; 1.4.5. Aircraft monitoring software; 1.4.6. iFACTS; 1.4.7. SPARK Skein; 1.5. Conclusion; 1.6. Bibliography
Chapter 2. Model-Based Testing Automatic Generationof Test Cases Using the Markov Chain Model2.1. Preliminaries on the test process; 2.1.1. Findings; 2.1.2. Test optimization; 2.1.3. The statistical usage test; 2.1.4. Generating test cases; 2.2. Modeling using Markov chains; 2.2.1. Origin; 2.2.2. Mathematical formalization; 2.2.3. Principles of generation; 2.2.4. Some indicators; 2.2.5. Calculating reliability; 2.3. The MaTeLo tool; 2.3.1. Engineering tests directed by models,model-based testing; 2.3.2. A chain of tools; 2.3.3. The usage model; 2.3.4. Configuration of test strategies
2.3.5. Generating test campaigns2.3.6. Analysis of the results and indicators; 2.4. Examples of industrial applications; 2.4.1. AUDI; 2.4.2. Magneti marelli; 2.4.3. Other industrial applications; 2.4.4. Industrialization of the tests; 2.5. Conclusion; 2.6. Bibliography; Chapter 3. Safety Analysis of the Embedded Systems with the AltaRica Approach; 3.1. Introduction; 3.2. Safety analysis of embedded systems; 3.3. AltaRica language and tools; 3.3.1. The AltaRica language; 3.3.2. Modeling the propagation of failures with AltaRica; 3.3.3. Tools associated with AltaRica
3.4. Examples of modeling and safety analysis3.4.1. Integrated modular avionics architecture; 3.4.2. System of electric power generation and distribution; 3.5. Comparison with other approaches; 3.5.1. Some precursors; 3.5.2. Tools for preexisting formal languages; 3.5.3. Languages for physical systems; 3.5.4. Injecting faults in nominal models; 3.6. Conclusion; 3.6.1. An approach to assess the safetyof systems tested in aeronautics; 3.6.2. Clarification of the system architectureand horizontal exploration of the failure propagation:impacts on the scope of analyses
3.6.3. Clarification of the nominal system characteristics:impacts on the generic definitions of the failure modes3.6.4. Compositional models of failure propagation:impacts on the overall safety process; 3.7. Special thanks; 3.8. Bibliography; Chapter 4. Polyspace®; 4.1. Overview; 4.2. Introduction to software quality and verification procedures; 4.3. Static analysis; 4.4. Dynamic tests; 4.5. Abstract interpretation; 4.6. Code verification; 4.7. Robustness verification or contextual verification; 4.7.1. Robustness verification; 4.7.2. Contextual verification
4.8. Examples of Polyspace® results
Record Nr. UNINA-9910831059503321
London, : ISTE
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Industrial used of formal method : formal verification / / edited by Jean-Louis Boulanger
Industrial used of formal method : formal verification / / edited by Jean-Louis Boulanger
Pubbl/distr/stampa London, : ISTE
Descrizione fisica 1 online resource (307 p.)
Disciplina 005.101
Altri autori (Persone) BoulangerJean-Louis
Collana ISTE
Soggetto topico Systems engineering - Data processing
Computer simulation
Formal methods (Computer science)
Computer software - Verification
Nondestructive testing
ISBN 1-118-58784-7
1-118-56182-1
1-299-18707-2
1-118-58790-1
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Cover; Title; Copyright; Table of Contents; Introduction; Chapter 1. SPARK - A Language and Tool-Set for High-Integrity Software Development; 1.1. Introduction; 1.2. An overview of SPARK; 1.2.1. What is SPARK?; 1.3. The rationale behind SPARK; 1.3.1. Flow analysis; 1.3.2. Code proof; 1.3.3. Correctness by construction; 1.4. Industrial applications of SPARK; 1.4.1. SHOLIS; 1.4.2. Lockheed-Martin C-130J mission computer; 1.4.3. MULTOS CA; 1.4.4. Tokeneer; 1.4.5. Aircraft monitoring software; 1.4.6. iFACTS; 1.4.7. SPARK Skein; 1.5. Conclusion; 1.6. Bibliography
Chapter 2. Model-Based Testing Automatic Generationof Test Cases Using the Markov Chain Model2.1. Preliminaries on the test process; 2.1.1. Findings; 2.1.2. Test optimization; 2.1.3. The statistical usage test; 2.1.4. Generating test cases; 2.2. Modeling using Markov chains; 2.2.1. Origin; 2.2.2. Mathematical formalization; 2.2.3. Principles of generation; 2.2.4. Some indicators; 2.2.5. Calculating reliability; 2.3. The MaTeLo tool; 2.3.1. Engineering tests directed by models,model-based testing; 2.3.2. A chain of tools; 2.3.3. The usage model; 2.3.4. Configuration of test strategies
2.3.5. Generating test campaigns2.3.6. Analysis of the results and indicators; 2.4. Examples of industrial applications; 2.4.1. AUDI; 2.4.2. Magneti marelli; 2.4.3. Other industrial applications; 2.4.4. Industrialization of the tests; 2.5. Conclusion; 2.6. Bibliography; Chapter 3. Safety Analysis of the Embedded Systems with the AltaRica Approach; 3.1. Introduction; 3.2. Safety analysis of embedded systems; 3.3. AltaRica language and tools; 3.3.1. The AltaRica language; 3.3.2. Modeling the propagation of failures with AltaRica; 3.3.3. Tools associated with AltaRica
3.4. Examples of modeling and safety analysis3.4.1. Integrated modular avionics architecture; 3.4.2. System of electric power generation and distribution; 3.5. Comparison with other approaches; 3.5.1. Some precursors; 3.5.2. Tools for preexisting formal languages; 3.5.3. Languages for physical systems; 3.5.4. Injecting faults in nominal models; 3.6. Conclusion; 3.6.1. An approach to assess the safetyof systems tested in aeronautics; 3.6.2. Clarification of the system architectureand horizontal exploration of the failure propagation:impacts on the scope of analyses
3.6.3. Clarification of the nominal system characteristics:impacts on the generic definitions of the failure modes3.6.4. Compositional models of failure propagation:impacts on the overall safety process; 3.7. Special thanks; 3.8. Bibliography; Chapter 4. Polyspace®; 4.1. Overview; 4.2. Introduction to software quality and verification procedures; 4.3. Static analysis; 4.4. Dynamic tests; 4.5. Abstract interpretation; 4.6. Code verification; 4.7. Robustness verification or contextual verification; 4.7.1. Robustness verification; 4.7.2. Contextual verification
4.8. Examples of Polyspace® results
Record Nr. UNINA-9910877828103321
London, : ISTE
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Safety of computer architectures [[electronic resource] /] / edited by Jean-Louis Boulanger
Safety of computer architectures [[electronic resource] /] / edited by Jean-Louis Boulanger
Pubbl/distr/stampa London, : ISTE
Descrizione fisica 1 online resource (506 p.)
Disciplina 005.8
Altri autori (Persone) BoulangerJean-Louis
Collana ISTE
Soggetto topico Computer architecture
Computer systems - Reliability
Computer security
Avionics - Safety measures
ISBN 1-118-60069-X
1-299-18750-1
1-118-60061-4
1-118-60080-0
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Cover; Safety of Computer Architectures; Title Page; Copyright Page; Table of Contents; Introduction; Chapter 1. Principles; 1.1. Introduction; 1.2. Presentation of the basic concepts: faults, errors and failures; 1.2.1. Obstruction to functional safety; 1.2.2. Safety demonstration studies; 1.2.3. Assessment; 1.3. Safe and/or available architecture; 1.4. Resetting a processing unit; 1.5. Overview of safety techniques; 1.5.1. Error detection; 1.5.2. Diversity; 1.5.3. Redundancy; 1.5.4. Error recovery and retrieval; 1.5.5. Partitioning; 1.6. Conclusion; 1.7. Bibliography
Chapter 2. Railway Safety Architecture2.1. Introduction; 2.2. Coded secure processor; 2.2.1. Basic principle; 2.2.2. Encoding; 2.2.3. Hardware architecture; 2.2.4. Assessment; 2.3. Other applications; 2.3.1. TVM 430; 2.3.2. SAET-METEOR; 2.4. Regulatory and normative context; 2.4.1. Introduction; 2.4.2. CENELEC and IEC history; 2.4.3. Commissioning evaluation, certification, and authorization; 2.5. Conclusion; 2.6. Bibliography; Chapter 3. From the Coded Uniprocessor to 2oo3; 3.1. Introduction; 3.2. From the uniprocessor to the dual processor with voter
3.2.1. North LGV requirements and the Channel Tunnel3.2.2. The principles of the dual processor with voter by coded uniprocessor; 3.2.3. Architecture characteristics; 3.2.4. Requirements for the Mediterranean LGV; 3.3. CSD: available safety computer; 3.3.1. Background; 3.3.2. Functional architecture; 3.3.3. Software architecture; 3.3.4. Synchronization signals; 3.3.5. The CSD mail system; 3.4. DIVA evolutions; 3.4.1. ERTMS equipment requirements; 3.4.2. Functional evolution; 3.4.3. Technological evolution; 3.5. New needs and possible solutions; 3.5.1. Management of the partitions
3.5.2. Multicycle services3.6. Conclusion; 3.7. Assessment of installations; 3.8. Bibliography; Chapter 4. Designing a Computerized Interlocking Module: a Key Component of Computer-Based Signal Boxes Designed by the SNCF; 4.1. Introduction; 4.2. Issues; 4.2.1. Persistent bias; 4.2.2. Challenges for tomorrow; 4.2.3. Probability and computer safety; 4.2.4. Maintainability and modifiability; 4.2.5. Specific problems of critical systems; 4.2.6. Towards a targeted architecture for safety automatons; 4.3. Railway safety: fundamental notions; 4.3.1. Safety and availability
4.3.2. Intrinsic safety and closed railway world4.3.3. Processing safety; 4.3.4. Provability of the safety of computerized equipment; 4.3.5. The signal box; 4.4. Development of the computerized interlocking module; 4.4.1. Development methodology of safety systems; 4.4.2. Technical architecture of the system; 4.4.3. MEI safety; 4.4.4. Modeling the PETRI network type; 4.5. Conclusion; 4.6. Bibliography; Chapter 5. Command Control of Railway Signaling Safety: Safety at Lower Cost; 5.1. Introduction; 5.2. A safety coffee machine; 5.3. History of the PIPC; 5.4. The concept basis
5.5. Postulates for safety requirements
Record Nr. UNINA-9910141480603321
London, : ISTE
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui