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.
Formal Methods and Software Engineering : 24th International Conference on Formal Engineering Methods, ICFEM 2023, Brisbane, QLD, Australia, November 21-24, 2023, Proceedings / / Yi Li and Sofiène Tahar, editors
| Formal Methods and Software Engineering : 24th International Conference on Formal Engineering Methods, ICFEM 2023, Brisbane, QLD, Australia, November 21-24, 2023, Proceedings / / Yi Li and Sofiène Tahar, editors |
| Edizione | [First edition.] |
| Pubbl/distr/stampa | Singapore : , : Springer, , [2024] |
| Descrizione fisica | 1 online resource (319 pages) |
| Disciplina | 004.0151 |
| Collana | Lecture Notes in Computer Science Series |
| Soggetto topico |
Formal methods (Computer science)
Software engineering |
| ISBN | 981-9975-84-0 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talk: Verifying Compiler Optimisations -- Regular Papers: An Idealist’s Approach for Smart Contract Correctness -- Active Inference of EFSMs Without Reset -- Learning Mealy Machines with Local Timers -- Compositional Vulnerability Detection with Insecurity Separation Logic -- Dynamic Extrapolation in Extended Timed Automata -- Formalizing Robustness against Character-level Perturbations for Neural Network Language Models -- Trace models of concurrent valuation algebras -- Branch and Bound for Sigmoid-like Neural Network Verification -- Certifying Sequential Consistency of Machine Learning Accelerators -- Guided Integration of Formal Verification in Assurance Cases -- Validation-Driven Development -- Incremental Property Directed Reachability -- Proving Local Invariants in ASTDs -- Doctoral Symposium Papers: Formal Verification of the Burn-to-Claim Blockchain Interoperable Protocol -- Early and systematic validation of formal models -- Verifying Neural Networks by Approximating Convex Hulls -- Eager to Stop: Efficient Falsification of Deep Neural Networks -- A Runtime Verification Framework For Cyber-physical Systems Based On Data Analytics And LTL Formula Learning -- Unified Verification of Neural Networks’ Robustness and Privacy in Computer Vision -- IoT Software Vulnerability Detection Techniques through Large Language Model -- Vulnerability Detection via Typestate-Guided Code Representation Learning. |
| Record Nr. | UNINA-9910760278703321 |
| Singapore : , : Springer, , [2024] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Formal methods and software engineering : 22nd International Conference on Formal Engineering Methods, ICFEM 2020, Singapore, Singapore, March 1-3, 2021, proceedings / / Shang-Wei Lin, Zhe Hou, Brendan Mahony (Eds.)
| Formal methods and software engineering : 22nd International Conference on Formal Engineering Methods, ICFEM 2020, Singapore, Singapore, March 1-3, 2021, proceedings / / Shang-Wei Lin, Zhe Hou, Brendan Mahony (Eds.) |
| Edizione | [1st ed. 2020.] |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2021] |
| Descrizione fisica | 1 online resource (XII, 335 p. 386 illus., 48 illus. in color.) |
| Disciplina | 004.0151 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Formal methods (Computer science)
Software engineering |
| ISBN | 3-030-63406-X |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Safety and Security -- Program Verification -- Formal Methods and Machine Learning -- Formal Languages -- Other Applications of Formal Methods. |
| Record Nr. | UNISA-996418292903316 |
| Cham, Switzerland : , : Springer, , [2021] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Formal methods and software engineering : 22nd International Conference on Formal Engineering Methods, ICFEM 2020, Singapore, Singapore, March 1-3, 2021, proceedings / / Shang-Wei Lin, Zhe Hou, Brendan Mahony (Eds.)
| Formal methods and software engineering : 22nd International Conference on Formal Engineering Methods, ICFEM 2020, Singapore, Singapore, March 1-3, 2021, proceedings / / Shang-Wei Lin, Zhe Hou, Brendan Mahony (Eds.) |
| Edizione | [1st ed. 2020.] |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2021] |
| Descrizione fisica | 1 online resource (XII, 335 p. 386 illus., 48 illus. in color.) |
| Disciplina | 004.0151 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Formal methods (Computer science)
Software engineering |
| ISBN | 3-030-63406-X |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Safety and Security -- Program Verification -- Formal Methods and Machine Learning -- Formal Languages -- Other Applications of Formal Methods. |
| Record Nr. | UNINA-9910447248903321 |
| Cham, Switzerland : , : Springer, , [2021] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Formal methods and software engineering : 10th international conference on formal engineering methods, ICFEM 2008, Kitakyushu-City, Japan, October 27-31, 2008 : proceedings / / edited by Shaoying Liu, Tom Maibaum, Keijiro Araki
| Formal methods and software engineering : 10th international conference on formal engineering methods, ICFEM 2008, Kitakyushu-City, Japan, October 27-31, 2008 : proceedings / / edited by Shaoying Liu, Tom Maibaum, Keijiro Araki |
| Edizione | [1st ed. 2008.] |
| Pubbl/distr/stampa | Berlin, Germany ; ; New York, New York : , : Springer, , [2008] |
| Descrizione fisica | 1 online resource (XI, 397 p.) |
| Disciplina | 005.1 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Software engineering
Formal methods (Computer science) |
| ISBN | 3-540-88194-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- How Can We Make Industry Adopt Formal Methods? -- Programmers Ain’t Mathematicians, and Neither Are Testers -- Contract-Based Reasoning for Verification and Certification of Secure Information Flow Policies in Industrial Workflows -- Specification and Verification -- Specifying and Verifying Event-Based Fairness Enhanced Systems -- Modelling and Proof of a Tree-Structured File System in Event-B and Rodin -- Testing -- Conformance Testing Based on UML State Machines -- An Approach to Testing with Embedded Context Using Model Checker -- Requirements Coverage as an Adequacy Measure for Conformance Testing -- Verification 1 -- Decomposition for Compositional Verification -- A Formal Soundness Proof of Region-Based Memory Management for Object-Oriented Paradigm -- Program Models for Compositional Verification -- Model Checking and Analysis -- A Unified Model Checking Approach with Projection Temporal Logic -- Formal Analysis of the Bakery Protocol with Consideration of Nonatomic Reads and Writes -- Towards Abstraction for DynAlloy Specifications -- Verification 2 -- Partial Translation Verification for Untrusted Code-Generators -- A Practical Approach to Partiality – A Proof Based Approach -- A Representative Function Approach to Symmetry Exploitation for CSP Refinement Checking -- Tools -- Probing the Depths of CSP-M: A New fdr-Compliant Validation Tool -- Practical Automated Partial Verification of Multi-paradigm Real-Time Models -- Application of Formal Methods -- Specifying and Verifying Sensor Networks: An Experiment of Formal Methods -- Correct Channel Passing by Construction -- Semantics -- A Process Semantics for BPMN -- A Formal Descriptive Semantics of UML. |
| Altri titoli varianti | ICFEM 2008 |
| Record Nr. | UNINA-9910485012503321 |
| Berlin, Germany ; ; New York, New York : , : Springer, , [2008] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Formal methods and software engineering : 10th international conference on formal engineering methods, ICFEM 2008, Kitakyushu-City, Japan, October 27-31, 2008 : proceedings / / edited by Shaoying Liu, Tom Maibaum, Keijiro Araki
| Formal methods and software engineering : 10th international conference on formal engineering methods, ICFEM 2008, Kitakyushu-City, Japan, October 27-31, 2008 : proceedings / / edited by Shaoying Liu, Tom Maibaum, Keijiro Araki |
| Edizione | [1st ed. 2008.] |
| Pubbl/distr/stampa | Berlin, Germany ; ; New York, New York : , : Springer, , [2008] |
| Descrizione fisica | 1 online resource (XI, 397 p.) |
| Disciplina | 005.1 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Software engineering
Formal methods (Computer science) |
| ISBN | 3-540-88194-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- How Can We Make Industry Adopt Formal Methods? -- Programmers Ain’t Mathematicians, and Neither Are Testers -- Contract-Based Reasoning for Verification and Certification of Secure Information Flow Policies in Industrial Workflows -- Specification and Verification -- Specifying and Verifying Event-Based Fairness Enhanced Systems -- Modelling and Proof of a Tree-Structured File System in Event-B and Rodin -- Testing -- Conformance Testing Based on UML State Machines -- An Approach to Testing with Embedded Context Using Model Checker -- Requirements Coverage as an Adequacy Measure for Conformance Testing -- Verification 1 -- Decomposition for Compositional Verification -- A Formal Soundness Proof of Region-Based Memory Management for Object-Oriented Paradigm -- Program Models for Compositional Verification -- Model Checking and Analysis -- A Unified Model Checking Approach with Projection Temporal Logic -- Formal Analysis of the Bakery Protocol with Consideration of Nonatomic Reads and Writes -- Towards Abstraction for DynAlloy Specifications -- Verification 2 -- Partial Translation Verification for Untrusted Code-Generators -- A Practical Approach to Partiality – A Proof Based Approach -- A Representative Function Approach to Symmetry Exploitation for CSP Refinement Checking -- Tools -- Probing the Depths of CSP-M: A New fdr-Compliant Validation Tool -- Practical Automated Partial Verification of Multi-paradigm Real-Time Models -- Application of Formal Methods -- Specifying and Verifying Sensor Networks: An Experiment of Formal Methods -- Correct Channel Passing by Construction -- Semantics -- A Process Semantics for BPMN -- A Formal Descriptive Semantics of UML. |
| Altri titoli varianti | ICFEM 2008 |
| Record Nr. | UNISA-996465956803316 |
| Berlin, Germany ; ; New York, New York : , : Springer, , [2008] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Formal methods and software engineering : 9th International Conference on Formal Engineering Methods, ICFEM 2007, Boca Raton, FL, USA, November 14-15, 2007 : proceedings / / Michael Butler, Michael G. Hinchey, Maria M. Larrondo-Petrie (editors)
| Formal methods and software engineering : 9th International Conference on Formal Engineering Methods, ICFEM 2007, Boca Raton, FL, USA, November 14-15, 2007 : proceedings / / Michael Butler, Michael G. Hinchey, Maria M. Larrondo-Petrie (editors) |
| Edizione | [1st ed. 2007.] |
| Pubbl/distr/stampa | Berlin : , : Springer, , [2007] |
| Descrizione fisica | 1 online resource (VIII, 387 p.) |
| Disciplina | 004.0151 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Formal methods (Computer science)
Software engineering |
| ISBN | 3-540-76650-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- A System Development Process with Event-B and the Rodin Platform -- Challenges in Software Certification -- Security and Knowledge -- Integrating Formal Methods with System Management -- Formal Engineering of XACML Access Control Policies in VDM++ -- A Verification Framework for Agent Knowledge -- Embedded Systems -- From Model-Based Design to Formal Verification of Adaptive Embedded Systems -- Machine-Assisted Proof Support for Validation Beyond Simulink -- VeSTA: A Tool to Verify the Correct Integration of a Component in a Composite Timed System -- Testing -- Integrating Specification-Based Review and Testing for Detecting Errors in Programs -- Testing for Refinement in CSP -- Reducing Test Sequence Length Using Invertible Sequences -- Automated Analysis -- Model Checking with SAT-Based Characterization of ACTL Formulas -- Automating Refinement Checking in Probabilistic System Design -- Model Checking in Practice: Analysis of Generic Bootloader Using SPIN -- Model Checking Propositional Projection Temporal Logic Based on SPIN -- Hardware -- A Denotational Semantics for Handel-C Hardware Compilation -- Automatic Generation of Verified Concurrent Hardware -- Modeling and Verification of Master/Slave Clock Synchronization Using Hybrid Automata and Model-Checking -- Concurrency -- Efficient Symbolic Execution of Large Quantifications in a Process Algebra -- Formalizing SANE Virtual Processor in Thread Algebra -- Calculating and Composing Progress Properties in Terms of the Leads-to Relation -- Erratum -- Erratum to: Challenges in Software Certification. |
| Record Nr. | UNISA-996465956103316 |
| Berlin : , : Springer, , [2007] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Formal methods and software engineering : 9th International Conference on Formal Engineering Methods, ICFEM 2007, Boca Raton, FL, USA, November 14-15, 2007 : proceedings / / Michael Butler, Michael G. Hinchey, Maria M. Larrondo-Petrie (editors)
| Formal methods and software engineering : 9th International Conference on Formal Engineering Methods, ICFEM 2007, Boca Raton, FL, USA, November 14-15, 2007 : proceedings / / Michael Butler, Michael G. Hinchey, Maria M. Larrondo-Petrie (editors) |
| Edizione | [1st ed. 2007.] |
| Pubbl/distr/stampa | Berlin : , : Springer, , [2007] |
| Descrizione fisica | 1 online resource (VIII, 387 p.) |
| Disciplina | 004.0151 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Formal methods (Computer science)
Software engineering |
| ISBN | 3-540-76650-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- A System Development Process with Event-B and the Rodin Platform -- Challenges in Software Certification -- Security and Knowledge -- Integrating Formal Methods with System Management -- Formal Engineering of XACML Access Control Policies in VDM++ -- A Verification Framework for Agent Knowledge -- Embedded Systems -- From Model-Based Design to Formal Verification of Adaptive Embedded Systems -- Machine-Assisted Proof Support for Validation Beyond Simulink -- VeSTA: A Tool to Verify the Correct Integration of a Component in a Composite Timed System -- Testing -- Integrating Specification-Based Review and Testing for Detecting Errors in Programs -- Testing for Refinement in CSP -- Reducing Test Sequence Length Using Invertible Sequences -- Automated Analysis -- Model Checking with SAT-Based Characterization of ACTL Formulas -- Automating Refinement Checking in Probabilistic System Design -- Model Checking in Practice: Analysis of Generic Bootloader Using SPIN -- Model Checking Propositional Projection Temporal Logic Based on SPIN -- Hardware -- A Denotational Semantics for Handel-C Hardware Compilation -- Automatic Generation of Verified Concurrent Hardware -- Modeling and Verification of Master/Slave Clock Synchronization Using Hybrid Automata and Model-Checking -- Concurrency -- Efficient Symbolic Execution of Large Quantifications in a Process Algebra -- Formalizing SANE Virtual Processor in Thread Algebra -- Calculating and Composing Progress Properties in Terms of the Leads-to Relation -- Erratum -- Erratum to: Challenges in Software Certification. |
| Record Nr. | UNINA-9910484765603321 |
| Berlin : , : Springer, , [2007] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Formal methods and stochastic models for performance evaluation : Fourth European Performance Engineering Workshop, EPEW 2007, Berlin, Germany, September, 2007 : proceedings / / edited by Katinka Wolter
| Formal methods and stochastic models for performance evaluation : Fourth European Performance Engineering Workshop, EPEW 2007, Berlin, Germany, September, 2007 : proceedings / / edited by Katinka Wolter |
| Edizione | [1st ed. 2007.] |
| Pubbl/distr/stampa | Berlin, Germany : , : Springer, , [2007] |
| Descrizione fisica | 1 online resource (X, 304 p.) |
| Disciplina | 004.24 |
| Collana | Programming and Software Engineering |
| Soggetto topico | Formal methods (Computer science) |
| ISBN | 3-540-75211-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Keynote -- Optimization Problems in Service Provisioning Systems -- Markov Chains -- Untold Horrors About Steady-State Probabilities: What Reward-Based Measures Won’t Tell About the Equilibrium Distribution -- Compositionality for Markov Reward Chains with Fast Transitions -- Closed Form Absorption Time Bounds -- A Canonical Representation of Order 3 Phase Type Distributions -- Process Algebras and State Machines -- SPAMR: Extending PAMR with Stochastic Time -- Faster SPDL Model Checking Through Property-Driven State Space Generation -- Testing Finite State Machines Presenting Stochastic Time and Timeouts -- Grid and Peer-to-Peer Systems -- Evaluation of P2P Search Algorithms for Discovering Trust Paths -- Building Online Performance Models of Grid Middleware with Fine-Grained Load-Balancing: A Globus Toolkit Case Study -- Performance Measuring Framework for Grid Market Middleware -- Queueing Theory and Applications of Queueing -- A Fixed-Point Algorithm for Closed Queueing Networks -- A Framework for Automated Generation of Architectural Feedback from Software Performance Analysis -- Optimal Dynamic Server Allocation in Systems with On/Off Sources -- Towards an Automatic Modeling Tool for Observed System Behavior -- Benchmarking and Bounding -- Censoring Markov Chains and Stochastic Bounds -- Workload Characterization of the SPECjms2007 Benchmark -- Resource Sharing in Performance Models -- Exploiting Commodity Hard-Disk Geometry to Efficiently Preserve Data Consistency -- Wireless Networks -- An Efficient Counter-Based Broadcast Scheme for Mobile Ad Hoc Networks -- The Effect of Mobility on Local Service Discovery in the Ahoy Ad-Hoc Network System. |
| Record Nr. | UNINA-9910484812503321 |
| Berlin, Germany : , : Springer, , [2007] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Formal methods and stochastic models for performance evaluation : Fourth European Performance Engineering Workshop, EPEW 2007, Berlin, Germany, September, 2007 : proceedings / / edited by Katinka Wolter
| Formal methods and stochastic models for performance evaluation : Fourth European Performance Engineering Workshop, EPEW 2007, Berlin, Germany, September, 2007 : proceedings / / edited by Katinka Wolter |
| Edizione | [1st ed. 2007.] |
| Pubbl/distr/stampa | Berlin, Germany : , : Springer, , [2007] |
| Descrizione fisica | 1 online resource (X, 304 p.) |
| Disciplina | 004.24 |
| Collana | Programming and Software Engineering |
| Soggetto topico | Formal methods (Computer science) |
| ISBN | 3-540-75211-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Keynote -- Optimization Problems in Service Provisioning Systems -- Markov Chains -- Untold Horrors About Steady-State Probabilities: What Reward-Based Measures Won’t Tell About the Equilibrium Distribution -- Compositionality for Markov Reward Chains with Fast Transitions -- Closed Form Absorption Time Bounds -- A Canonical Representation of Order 3 Phase Type Distributions -- Process Algebras and State Machines -- SPAMR: Extending PAMR with Stochastic Time -- Faster SPDL Model Checking Through Property-Driven State Space Generation -- Testing Finite State Machines Presenting Stochastic Time and Timeouts -- Grid and Peer-to-Peer Systems -- Evaluation of P2P Search Algorithms for Discovering Trust Paths -- Building Online Performance Models of Grid Middleware with Fine-Grained Load-Balancing: A Globus Toolkit Case Study -- Performance Measuring Framework for Grid Market Middleware -- Queueing Theory and Applications of Queueing -- A Fixed-Point Algorithm for Closed Queueing Networks -- A Framework for Automated Generation of Architectural Feedback from Software Performance Analysis -- Optimal Dynamic Server Allocation in Systems with On/Off Sources -- Towards an Automatic Modeling Tool for Observed System Behavior -- Benchmarking and Bounding -- Censoring Markov Chains and Stochastic Bounds -- Workload Characterization of the SPECjms2007 Benchmark -- Resource Sharing in Performance Models -- Exploiting Commodity Hard-Disk Geometry to Efficiently Preserve Data Consistency -- Wireless Networks -- An Efficient Counter-Based Broadcast Scheme for Mobile Ad Hoc Networks -- The Effect of Mobility on Local Service Discovery in the Ahoy Ad-Hoc Network System. |
| Record Nr. | UNISA-996465954303316 |
| Berlin, Germany : , : Springer, , [2007] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
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 | ||
| ||
