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 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
Formal Methods for an Informal World : ICTAC 2021 Summer School, Virtual Event, Astana, Kazakhstan, September 1-7, 2021, Tutorial Lectures / / Antonio Cerone, editors
Formal Methods for an Informal World : ICTAC 2021 Summer School, Virtual Event, Astana, Kazakhstan, September 1-7, 2021, Tutorial Lectures / / Antonio Cerone, editors
Edizione [First edition.]
Pubbl/distr/stampa Cham, Switzerland : , : Springer, , [2023]
Descrizione fisica 1 online resource (180 pages)
Disciplina 005.3
Collana Lecture Notes in Computer Science Series
Soggetto topico Formal methods (Computer science)
ISBN 3-031-43678-4
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Modelling Interactions: Digital and Physical -- Modelling and Analysing Cognition and Interaction -- Object-Centric Process Mining: An Introduction -- Model-based engineering for robotics with RoboChart and RoboTool -- Formal Methods Adoption in Industry: An Experience Report -- Security Research: Program Analysis Meets Security.
Record Nr. UNINA-9910760284203321
Cham, Switzerland : , : Springer, , [2023]
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Formal Methods for an Informal World : ICTAC 2021 Summer School, Virtual Event, Astana, Kazakhstan, September 1-7, 2021, Tutorial Lectures / / Antonio Cerone, editors
Formal Methods for an Informal World : ICTAC 2021 Summer School, Virtual Event, Astana, Kazakhstan, September 1-7, 2021, Tutorial Lectures / / Antonio Cerone, editors
Edizione [First edition.]
Pubbl/distr/stampa Cham, Switzerland : , : Springer, , [2023]
Descrizione fisica 1 online resource (180 pages)
Disciplina 005.3
Collana Lecture Notes in Computer Science Series
Soggetto topico Formal methods (Computer science)
ISBN 3-031-43678-4
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Modelling Interactions: Digital and Physical -- Modelling and Analysing Cognition and Interaction -- Object-Centric Process Mining: An Introduction -- Model-based engineering for robotics with RoboChart and RoboTool -- Formal Methods Adoption in Industry: An Experience Report -- Security Research: Program Analysis Meets Security.
Record Nr. UNISA-996565872003316
Cham, Switzerland : , : Springer, , [2023]
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
Formal methods for components and objects : 5th International Symposium, FMCO 2006, Amsterdam, the Netherlands, November 7-10, 2006 : revised lectures / / Frank S. de Boer [and three others], editors
Formal methods for components and objects : 5th International Symposium, FMCO 2006, Amsterdam, the Netherlands, November 7-10, 2006 : revised lectures / / Frank S. de Boer [and three others], editors
Edizione [1st ed. 2007.]
Pubbl/distr/stampa Berlin ; ; Heidelberg : , : Springer, , [2007]
Descrizione fisica 1 online resource (VIII, 300 p.)
Disciplina 004.0151
Collana Lecture Notes in Computer Science
Soggetto topico Formal methods (Computer science)
Object-oriented programming (Computer science)
ISBN 3-540-74792-3
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Testing -- Model-Based Testing of Environmental Conformance of Components -- Exhaustive Testing of Exception Handlers with Enforcer -- Model-Based Test Selection for Infinite-State Reactive Systems -- Program Verification -- Verifying Object-Oriented Programs with KeY: A Tutorial -- Rebeca: Theory, Applications, and Tools -- Learning Meets Verification -- Trust and Security -- JACK — A Tool for Validation of Security and Behaviour of Java Applications -- Towards a Formal Framework for Computational Trust -- Models of Computation -- On Recursion, Replication and Scope Mechanisms in Process Calculi -- Bounded Session Types for Object Oriented Languages -- Distributed Programming -- Reflecting on Aspect-Oriented Programming, Metaprogramming, and Adaptive Distributed Monitoring -- Links: Web Programming Without Tiers.
Record Nr. UNINA-9910483617003321
Berlin ; ; Heidelberg : , : Springer, , [2007]
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Formal methods for components and objects : 5th International Symposium, FMCO 2006, Amsterdam, the Netherlands, November 7-10, 2006 : revised lectures / / Frank S. de Boer [and three others], editors
Formal methods for components and objects : 5th International Symposium, FMCO 2006, Amsterdam, the Netherlands, November 7-10, 2006 : revised lectures / / Frank S. de Boer [and three others], editors
Edizione [1st ed. 2007.]
Pubbl/distr/stampa Berlin ; ; Heidelberg : , : Springer, , [2007]
Descrizione fisica 1 online resource (VIII, 300 p.)
Disciplina 004.0151
Collana Lecture Notes in Computer Science
Soggetto topico Formal methods (Computer science)
Object-oriented programming (Computer science)
ISBN 3-540-74792-3
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Testing -- Model-Based Testing of Environmental Conformance of Components -- Exhaustive Testing of Exception Handlers with Enforcer -- Model-Based Test Selection for Infinite-State Reactive Systems -- Program Verification -- Verifying Object-Oriented Programs with KeY: A Tutorial -- Rebeca: Theory, Applications, and Tools -- Learning Meets Verification -- Trust and Security -- JACK — A Tool for Validation of Security and Behaviour of Java Applications -- Towards a Formal Framework for Computational Trust -- Models of Computation -- On Recursion, Replication and Scope Mechanisms in Process Calculi -- Bounded Session Types for Object Oriented Languages -- Distributed Programming -- Reflecting on Aspect-Oriented Programming, Metaprogramming, and Adaptive Distributed Monitoring -- Links: Web Programming Without Tiers.
Record Nr. UNISA-996465920203316
Berlin ; ; Heidelberg : , : Springer, , [2007]
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
Formal methods for industrial critical systems : 27th International Conference, FMICS 2022, Warsaw, Poland, September 14-15, 2022, proceedings / / Jan Friso Groote, Marieke Huisman (editors)
Formal methods for industrial critical systems : 27th International Conference, FMICS 2022, Warsaw, Poland, September 14-15, 2022, proceedings / / Jan Friso Groote, Marieke Huisman (editors)
Pubbl/distr/stampa Cham, Switzerland : , : Springer, , [2022]
Descrizione fisica 1 online resource (246 pages)
Disciplina 004.0151
Collana Lecture notes in computer science
Soggetto topico Formal methods (Computer science)
Software engineering
ISBN 3-031-15008-2
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Intro -- Preface -- Organization -- Contents -- Invited Keynote Talks -- Reinforcement Learning with Guarantees that Hold for Ever -- 1 Learning from Rewards -- 2 Learning with -Regular Objectives -- 2.1 Good-for-MDP Automata -- 2.2 From GFM Büchi Automata to Reachability and RL -- 3 Related Work -- References -- Supporting Railway Innovations with Formal Modelling and Verification -- References -- Certification -- Formal Monotony Analysis of Neural Networks with Mixed Inputs: An Asset for Certification -- 1 Introduction -- 2 Certification Preamble -- 3 Related Work -- 4 Monotony Analysis -- 4.1 Goal of the Analysis -- 4.2 MILP Formulation -- 4.3 Verification Procedure -- 5 Case Study: Braking Distance Estimation -- 5.1 Description of the Case Study -- 5.2 Experimentation -- 6 Conclusion -- References -- Generating Domain-Specific Interactive Validation Documents -- 1 Introduction and Motivation -- 2 Validation Workflow -- 3 Static VisB HTML Export -- 4 Dynamic HTML Export: Code Generation to HTML and JavaScript -- 4.1 Graphical User Interface -- 4.2 Applicability of JavaScript Code Generation -- 5 Case Studies -- 6 Related Work -- 7 Conclusion and Future Work -- References -- Deductive Verification of Smart Contracts with Dafny -- 1 Introduction -- 2 Verification of Closed Smart Contracts -- 3 Verification Under Adversarial Conditions -- 3.1 Aborting a Computation -- 3.2 Reasoning with Arbitrary External Calls -- 4 Conclusion -- References -- Industrial Use Cases -- Towards Reusable Formal Models for Custom Real-Time Operating Systems -- 1 Introduction -- 2 Preliminaries -- 2.1 Core Components of Real-Time Operating Systems -- 2.2 Uppaal Timed Automata -- 3 Related Work -- 4 Reusable Formal Models for Custom RTOS -- 4.1 Formalization of Tasks -- 4.2 Formalization of Cyclic Handlers -- 4.3 Events and Timing Behavior.
4.4 Configurable Formal Scheduler Model -- 4.5 Modeling Sensor Inputs and Communication -- 5 Case Study: Search and Rescue Robots -- 6 Conclusion -- References -- Formal Verification of an Industrial UML-like Model using mCRL2 -- 1 Introduction -- 2 Cordis Models -- 2.1 Class Diagrams -- 2.2 State Machine Diagrams -- 3 Cylinder -- 4 Model Checking Cordis Models Using mCRL2 -- 4.1 Translation to mCRL2 -- 4.2 Formal Verification of Requirements -- 4.3 Results -- 5 Discussion -- 6 Concluding Remarks -- References -- Chemical Case Studies in KeYmaera X -- 1 Introduction -- 2 Background -- 2.1 Differential Dynamic Logic -- 2.2 KeYmaera X -- 3 Results -- 3.1 Controlled Irreversible Reactions -- 3.2 Uncontrolled Reversible Reactions -- 4 Related Work -- 5 Conclusion -- References -- Analysing Capacity Bottlenecks in Rail Infrastructure by Episode Mining -- 1 Introduction -- 2 Related Work -- 3 Identification of Capacity Bottlenecks -- 3.1 Method -- 3.2 Results -- 4 Analysing Delay Propagations -- 4.1 Goals and Overview -- 4.2 Episode Mining -- 4.3 Algorithm and Implementation -- 4.4 Adaptations -- 5 Evaluation Results -- 6 Conclusions and Outlook -- References -- Testing and Monitoring -- Test Suite Augmentation for Reconfigurable PLC Software in the Internet of Production -- 1 Introduction -- 1.1 Limitations and Contributions -- 2 Related Work -- 3 Methodology -- 3.1 Intermediate Representation -- 3.2 Bounded Symbolic Execution -- 3.3 Shadow Symbolic Execution -- 4 Evaluation -- 5 Conclusion -- References -- Monitoring of Spatio-Temporal Properties with Nonlinear SAT Solvers -- 1 Introduction -- 2 Preliminaries -- 3 Running Example -- 3.1 Formalization of Road Traffic Rules with LTL MS -- 3.2 Scenario and Trace Encoding (Static and Dynamic Objects) -- 4 Monitoring Model Construction -- 5 Empirical Evaluation -- 6 Related Work.
7 Conclusion and Future Work -- References -- Model-Based Testing of Internet of Things Protocols -- 1 Introduction -- 1.1 Related Work -- 1.2 Contributions -- 2 Preliminaries -- 2.1 Internet of Things -- 2.2 Model-Based Testing -- 2.3 Axini Modeling Platform (AMP) -- 3 MBT in the Context of IoT -- 3.1 IoT Testing Challenges -- 3.2 Positioning MBT in IoT -- 4 The AMP MBT Environment to Test BLE IoT Systems -- 4.1 SUT -- 4.2 Model Creation -- 4.3 AML Model Example -- 4.4 Adapter -- 5 Testing BLE Using AMP -- 5.1 Assumption -- 5.2 Test Generation Configurations -- 5.3 Conformance Experiment -- 5.4 Model Assumption Experiment -- 6 Discussion -- 7 Conclusion -- 7.1 Future Work -- References -- Methodology -- Formally Verifying Decompositions of Stochastic Specifications -- 1 Introduction -- 2 Problem Illustration -- 3 A Theory for Specifying Stochastic Behavior -- 3.1 Traces and Behaviors -- 3.2 Specifications -- 3.3 Trace Automata -- 3.4 Probabilistic Automaton Contracts -- 4 Verification of Refinement -- 5 Case Study -- 6 Related Work -- 7 Conclusions -- References -- Verification of Behavior Trees using Linear Constrained Horn Clauses -- 1 Introduction -- 2 Related Works -- 3 Preliminaries -- 3.1 Behavior Trees -- 3.2 Constrained Horn Clauses -- 4 Encoding of Behavior Trees -- 4.1 Idea -- 4.2 Action Node -- 4.3 Condition Node -- 4.4 Sequence Node -- 4.5 Sequence Node with Memory -- 4.6 Selector Node -- 4.7 Parallel Node -- 4.8 Root Node -- 4.9 Safety Property -- 4.10 Environment -- 5 Experiments -- 5.1 Benchmark -- 5.2 Discussion -- 6 Conclusion and Outlook -- References -- A Multi-level Methodology for Behavioral Comparison of Software-Intensive Systems -- 1 Introduction -- 2 Background -- 2.1 Software Behavior -- 2.2 State Machines -- 2.3 State Machine Comparison -- 3 Behavioral Comparison Methodology -- 3.1 Level 1: Model Set Variants.
3.2 Level 2: Model Set Variant Relations -- 3.3 Level 3: Model Set Variant Differences -- 3.4 Level 4: Model Variants -- 3.5 Level 5: Model Variant Relations -- 3.6 Level 6: Model Variant Differences -- 4 Evaluation -- 4.1 Case Study 1: Legacy Component Technology Migration -- 4.2 Case Study 2: System Behavior Matching Recipe -- 5 Conclusions and Future Work -- References -- Author Index.
Record Nr. UNINA-9910591039203321
Cham, Switzerland : , : Springer, , [2022]
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Formal methods for industrial critical systems : 27th International Conference, FMICS 2022, Warsaw, Poland, September 14-15, 2022, proceedings / / Jan Friso Groote, Marieke Huisman (editors)
Formal methods for industrial critical systems : 27th International Conference, FMICS 2022, Warsaw, Poland, September 14-15, 2022, proceedings / / Jan Friso Groote, Marieke Huisman (editors)
Pubbl/distr/stampa Cham, Switzerland : , : Springer, , [2022]
Descrizione fisica 1 online resource (246 pages)
Disciplina 004.0151
Collana Lecture notes in computer science
Soggetto topico Formal methods (Computer science)
Software engineering
ISBN 3-031-15008-2
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Intro -- Preface -- Organization -- Contents -- Invited Keynote Talks -- Reinforcement Learning with Guarantees that Hold for Ever -- 1 Learning from Rewards -- 2 Learning with -Regular Objectives -- 2.1 Good-for-MDP Automata -- 2.2 From GFM Büchi Automata to Reachability and RL -- 3 Related Work -- References -- Supporting Railway Innovations with Formal Modelling and Verification -- References -- Certification -- Formal Monotony Analysis of Neural Networks with Mixed Inputs: An Asset for Certification -- 1 Introduction -- 2 Certification Preamble -- 3 Related Work -- 4 Monotony Analysis -- 4.1 Goal of the Analysis -- 4.2 MILP Formulation -- 4.3 Verification Procedure -- 5 Case Study: Braking Distance Estimation -- 5.1 Description of the Case Study -- 5.2 Experimentation -- 6 Conclusion -- References -- Generating Domain-Specific Interactive Validation Documents -- 1 Introduction and Motivation -- 2 Validation Workflow -- 3 Static VisB HTML Export -- 4 Dynamic HTML Export: Code Generation to HTML and JavaScript -- 4.1 Graphical User Interface -- 4.2 Applicability of JavaScript Code Generation -- 5 Case Studies -- 6 Related Work -- 7 Conclusion and Future Work -- References -- Deductive Verification of Smart Contracts with Dafny -- 1 Introduction -- 2 Verification of Closed Smart Contracts -- 3 Verification Under Adversarial Conditions -- 3.1 Aborting a Computation -- 3.2 Reasoning with Arbitrary External Calls -- 4 Conclusion -- References -- Industrial Use Cases -- Towards Reusable Formal Models for Custom Real-Time Operating Systems -- 1 Introduction -- 2 Preliminaries -- 2.1 Core Components of Real-Time Operating Systems -- 2.2 Uppaal Timed Automata -- 3 Related Work -- 4 Reusable Formal Models for Custom RTOS -- 4.1 Formalization of Tasks -- 4.2 Formalization of Cyclic Handlers -- 4.3 Events and Timing Behavior.
4.4 Configurable Formal Scheduler Model -- 4.5 Modeling Sensor Inputs and Communication -- 5 Case Study: Search and Rescue Robots -- 6 Conclusion -- References -- Formal Verification of an Industrial UML-like Model using mCRL2 -- 1 Introduction -- 2 Cordis Models -- 2.1 Class Diagrams -- 2.2 State Machine Diagrams -- 3 Cylinder -- 4 Model Checking Cordis Models Using mCRL2 -- 4.1 Translation to mCRL2 -- 4.2 Formal Verification of Requirements -- 4.3 Results -- 5 Discussion -- 6 Concluding Remarks -- References -- Chemical Case Studies in KeYmaera X -- 1 Introduction -- 2 Background -- 2.1 Differential Dynamic Logic -- 2.2 KeYmaera X -- 3 Results -- 3.1 Controlled Irreversible Reactions -- 3.2 Uncontrolled Reversible Reactions -- 4 Related Work -- 5 Conclusion -- References -- Analysing Capacity Bottlenecks in Rail Infrastructure by Episode Mining -- 1 Introduction -- 2 Related Work -- 3 Identification of Capacity Bottlenecks -- 3.1 Method -- 3.2 Results -- 4 Analysing Delay Propagations -- 4.1 Goals and Overview -- 4.2 Episode Mining -- 4.3 Algorithm and Implementation -- 4.4 Adaptations -- 5 Evaluation Results -- 6 Conclusions and Outlook -- References -- Testing and Monitoring -- Test Suite Augmentation for Reconfigurable PLC Software in the Internet of Production -- 1 Introduction -- 1.1 Limitations and Contributions -- 2 Related Work -- 3 Methodology -- 3.1 Intermediate Representation -- 3.2 Bounded Symbolic Execution -- 3.3 Shadow Symbolic Execution -- 4 Evaluation -- 5 Conclusion -- References -- Monitoring of Spatio-Temporal Properties with Nonlinear SAT Solvers -- 1 Introduction -- 2 Preliminaries -- 3 Running Example -- 3.1 Formalization of Road Traffic Rules with LTL MS -- 3.2 Scenario and Trace Encoding (Static and Dynamic Objects) -- 4 Monitoring Model Construction -- 5 Empirical Evaluation -- 6 Related Work.
7 Conclusion and Future Work -- References -- Model-Based Testing of Internet of Things Protocols -- 1 Introduction -- 1.1 Related Work -- 1.2 Contributions -- 2 Preliminaries -- 2.1 Internet of Things -- 2.2 Model-Based Testing -- 2.3 Axini Modeling Platform (AMP) -- 3 MBT in the Context of IoT -- 3.1 IoT Testing Challenges -- 3.2 Positioning MBT in IoT -- 4 The AMP MBT Environment to Test BLE IoT Systems -- 4.1 SUT -- 4.2 Model Creation -- 4.3 AML Model Example -- 4.4 Adapter -- 5 Testing BLE Using AMP -- 5.1 Assumption -- 5.2 Test Generation Configurations -- 5.3 Conformance Experiment -- 5.4 Model Assumption Experiment -- 6 Discussion -- 7 Conclusion -- 7.1 Future Work -- References -- Methodology -- Formally Verifying Decompositions of Stochastic Specifications -- 1 Introduction -- 2 Problem Illustration -- 3 A Theory for Specifying Stochastic Behavior -- 3.1 Traces and Behaviors -- 3.2 Specifications -- 3.3 Trace Automata -- 3.4 Probabilistic Automaton Contracts -- 4 Verification of Refinement -- 5 Case Study -- 6 Related Work -- 7 Conclusions -- References -- Verification of Behavior Trees using Linear Constrained Horn Clauses -- 1 Introduction -- 2 Related Works -- 3 Preliminaries -- 3.1 Behavior Trees -- 3.2 Constrained Horn Clauses -- 4 Encoding of Behavior Trees -- 4.1 Idea -- 4.2 Action Node -- 4.3 Condition Node -- 4.4 Sequence Node -- 4.5 Sequence Node with Memory -- 4.6 Selector Node -- 4.7 Parallel Node -- 4.8 Root Node -- 4.9 Safety Property -- 4.10 Environment -- 5 Experiments -- 5.1 Benchmark -- 5.2 Discussion -- 6 Conclusion and Outlook -- References -- A Multi-level Methodology for Behavioral Comparison of Software-Intensive Systems -- 1 Introduction -- 2 Background -- 2.1 Software Behavior -- 2.2 State Machines -- 2.3 State Machine Comparison -- 3 Behavioral Comparison Methodology -- 3.1 Level 1: Model Set Variants.
3.2 Level 2: Model Set Variant Relations -- 3.3 Level 3: Model Set Variant Differences -- 3.4 Level 4: Model Variants -- 3.5 Level 5: Model Variant Relations -- 3.6 Level 6: Model Variant Differences -- 4 Evaluation -- 4.1 Case Study 1: Legacy Component Technology Migration -- 4.2 Case Study 2: System Behavior Matching Recipe -- 5 Conclusions and Future Work -- References -- Author Index.
Record Nr. UNISA-996490368003316
Cham, Switzerland : , : Springer, , [2022]
Materiale a stampa
Lo trovi qui: Univ. di Salerno
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
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. UNINA-9910495155003321
Cham, Switzerland : , : Springer, , [2021]
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Formal methods for industrial critical systems : a survey of applications / / edited by Stefania Gnesi, Tiziana Margaria
Formal methods for industrial critical systems : a survey of applications / / edited by Stefania Gnesi, Tiziana Margaria
Pubbl/distr/stampa Hoboken, New Jersey : , : John Wiley and Sons Incorporated, , [2012]
Descrizione fisica 1 online resource (294 p.)
Disciplina 004.21
620.86028551
Altri autori (Persone) GnesiStefania <1954->
Margaria-SteffenTiziana <1964->
Soggetto topico Formal methods (Computer science)
System design
ISBN 1-118-45989-X
1-283-85888-6
1-118-45986-5
Classificazione COM059000
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto FOREWORD by Mike Hinchey xiii -- FOREWORD by Alessandro Fantechi and Pedro Merino xv -- PREFACE xvii -- CONTRIBUTORS xix -- PART I INTRODUCTION AND STATE OF THE ART 1 -- 1 FORMAL METHODS: APPLYING {LOGICS IN, THEORETICAL} COMPUTER SCIENCE 3 -- Diego Latella -- 1.1 Introduction and State of the Art 3 -- 1.2 Future Directions 9 -- PART II MODELING PARADIGMS 15 -- 2 A SYNCHRONOUS LANGUAGE AT WORK: THE STORY OF LUSTRE 17 -- Nicolas Halbwachs -- 2.1 Introduction 17 -- 2.2 A Flavor of the Language 18 -- 2.3 The Design and Development of Lustre and Scade 20 -- 2.4 Some Lessons from Industrial Use 25 -- 2.5 And Now . . . 28 -- 3 REQUIREMENTS OF AN INTEGRATED FORMAL METHOD FOR INTELLIGENT SWARMS 33 -- Mike Hinchey, James L. Rash, Christopher A. Rouff, Walt F. Truszkowski, and Amy K.C.S. Vanderbilt -- 3.1 Introduction 33 -- 3.2 Swarm Technologies 35 -- 3.3 NASA FAST Project 39 -- 3.4 Integrated Swarm Formal Method 41 -- 3.5 Conclusion 55 -- PART III TRANSPORTATION SYSTEMS 61 -- 4 SOME TRENDS IN FORMAL METHODS APPLICATIONS TO RAILWAY SIGNALING 63 -- Alessandro Fantechi, Wan Fokkink, and Angelo Morzenti -- 4.1 Introduction 63 -- 4.2 CENELEC Guidelines 65 -- 4.3 Software Procurement in Railway Signaling 66 -- 4.4 A Success Story: The B Method 70 -- 4.5 Classes of Railway Signaling Equipment 71 -- 4.6 Conclusions 80 -- 5 SYMBOLIC MODEL CHECKING FOR AVIONICS 85 -- Radu I. Siminiceanu and Gianfranco Ciardo -- 5.1 Introduction 85 -- 5.2 Application: The Runway Safety Monitor 87 -- 5.3 A Discrete Model of RSM 95 -- 5.4 Discussion 107 -- PART IV TELECOMMUNICATIONS 113 -- 6 APPLYING FORMAL METHODS TO TELECOMMUNICATION SERVICES WITH ACTIVE NETWORKS 115 -- Marƒia del Mar Gallardo, Jesús Martƒinez, and Pedro Merino -- 6.1 Overview 115 -- 6.2 Active Networks 116 -- 6.3 The Capsule Approach 117 -- 6.4 Previous Approaches on Analyzing Active Networks 118 -- 6.5 Model Checking Active Networks with SPIN 122 -- 6.6 Conclusions 129 -- 7 PRACTICAL APPLICATIONS OF PROBABILISTIC MODEL CHECKING TO COMMUNICATION PROTOCOLS 133 -- Marie Dufl ot, Marta Kwiatkowska, Gethin Norman, David Parker, Sylvain Peyronnet, Claudine Picaronny, and Jeremy Sproston.
7.1 Introduction 133 -- 7.2 PTAs 134 -- 7.3 Probabilistic Model Checking 136 -- 7.4 Case Study: CSMA/CD 139 -- 7.5 Discussion and Conclusion 146 -- PART V INTERNET AND ONLINE SERVICES 151 -- 8 DESIGN FOR VERIFIABILITY: THE OCS CASE STUDY 153 -- Johannes Neubauer, Tiziana Margaria, and Bernhard Steffen -- 8.1 Introduction 153 -- 8.2 The User Model 155 -- 8.3 The Models and the Framework 158 -- 8.4 Model Checking 159 -- 8.5 Validating Emerging Global Behavior via Automata Learning 161 -- 8.6 Related Work 170 -- 8.7 Conclusion and Perspectives 173 -- 9 AN APPLICATION OF STOCHASTIC MODEL CHECKING IN THE INDUSTRY: USER-CENTERED MODELING AND ANALYSIS OF COLLABORATION IN THINKTEAM 179 -- Maurice H. ter Beek, Stefania Gnesi, Diego Latella, Mieke Massink, Maurizio Sebastianis, and Gianluca Trentanni -- 9.1 Introduction 179 -- 9.2 thinkteam 182 -- 9.3 Analysis of the thinkteam Log File 184 -- 9.4 thinkteam with Replicated Vaults 189 -- 9.5 Lessons Learned 201 -- 9.6 Conclusions 201 -- PART VI RUNTIME: TESTING AND MODEL LEARNING 205 -- 10 THE TESTING AND TEST CONTROL NOTATION TTCN-3 AND ITS USE 207 -- Ina Schieferdecker and Alain-Georges Vouffo-Feudjio -- 10.1 Introduction 207 -- 10.2 The Concepts of TTCN-3 210 -- 10.3 An Introductory Example 216 -- 10.4 TTCN-3 Semantics and Its Application 219 -- 10.5 A Distributed Test Platform for the TTCN-3 220 -- 10.6 Case Study I: Testing of Open Service Architecture (OSA)/Parlay Services 223 -- 10.7 Case Study II: Testing of IP Multimedia Subsystem (IMS) Equipment 225 -- 10.8 Conclusion 230 -- 11 PRACTICAL ASPECTS OF ACTIVE AUTOMATA LEARNING 235 -- Falk Howar, Maik Merten, Bernhard Steffen, and Tiziana Margaria -- 11.1 Introduction 235 -- 11.2 Regular Extrapolation 239 -- 11.3 Challenges in Regular Extrapolation 244 -- 11.4 Interacting with Real Systems 247 -- 11.5 Membership Queries 250 -- 11.6 Reset 253 -- 11.7 Parameters and Value Domains 256 -- 11.8 The NGLL 260 -- 11.9 Conclusion and Perspectives 263 -- References 264 -- INDEX 269.
Record Nr. UNINA-9910141360103321
Hoboken, New Jersey : , : John Wiley and Sons Incorporated, , [2012]
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui