LEADER 09798nam 22008055 450 001 9910746292003321 005 20250414112347.0 010 $a9783031436819 010 $a3031436814 024 7 $a10.1007/978-3-031-43681-9 035 $a(MiAaPQ)EBC30746895 035 $a(Au-PeEL)EBL30746895 035 $a(CKB)28267871600041 035 $a(OCoLC)1398310626 035 $a(DE-He213)978-3-031-43681-9 035 $a(EXLCZ)9928267871600041 100 $a20230916d2023 u| 0 101 0 $aeng 135 $aurcnu|||||||| 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 10$aFormal Methods for Industrial Critical Systems $e28th International Conference, FMICS 2023, Antwerp, Belgium, September 20?22, 2023, Proceedings /$fedited by Alessandro Cimatti, Laura Titolo 205 $a1st ed. 2023. 210 1$aCham :$cSpringer Nature Switzerland :$cImprint: Springer,$d2023. 215 $a1 online resource (270 pages) 225 1 $aLecture Notes in Computer Science,$x1611-3349 ;$v14290 311 08$aPrint version: Cimatti, Alessandro Formal Methods for Industrial Critical Systems Cham : Springer International Publishing AG,c2023 9783031436802 327 $aIntro -- Preface -- Organization -- Contents -- Experimenting with Formal Verification and Model-Based Development in Railways: The Case of UMC and Sparx Enterprise Architect -- 1 Introduction -- 2 Related Work -- 3 MBSD, Sparx Enterprise Architect and UMC -- 3.1 Sparx Enterprise Architect -- 3.2 UML Model Checker -- 4 Methodology -- 5 Case Study -- 5.1 Model Checking Sparx EA Models -- 6 Lessons Learned and Limitations -- 7 Conclusion -- References -- The 4SECURail Case Study on Rigorous Standard Interface Specifications -- 1 Introduction -- 2 The Demonstrator Case Study -- 2.1 The 4SECURail Case Study -- 2.2 The Formalization of the Case Study -- 3 Cost-Benefit Analysis -- 4 Discussion and Conclusions -- References -- Statistical Model Checking for P -- 1 Introduction -- 2 An Overview of P -- 2.1 An Overview of P and its Semantics -- 2.2 A Case Study: A Bike Sharing System -- 3 Statistical Model Checking with MultiVeStA -- 4 Integration of P and MultiVeStA -- 5 A Case Study -- 5.1 Verifying Quantitative Properties of the Bikes Example -- 5.2 On the Scalability of Statistical Model Checking -- 6 Concluding Remarks -- References -- Pattern-Based Verification of ROS 2 Nodes Using UPPAAL -- 1 Introduction -- 2 Background -- 2.1 ROS 2 -- 2.2 Timed Automata and UPPAAL -- 3 Modeling and Verification of ROS 2 Nodes in UPPAAL -- 4 Evaluation of Pattern-Based Verification -- 5 Related Work -- 6 Conclusions and Future Work -- References -- Configurable Model-Based Test Generation for Distributed Controllers Using Declarative Model Queries and Model Checkers -- 1 Introduction -- 2 Preliminaries -- 2.1 Railway Interlocking System and its Object Manager Subsystem -- 2.2 Component Integration and Test Generation Approach -- 2.3 VIATRA Query Language -- 3 Configuring Message Queues for Component Interactions -- 4 Property Specification Using Model Queries. 327 $a5 Practical Evaluation -- 6 Related Work -- 7 Conclusion and Future Work -- References -- Refinement of Systems with an Attacker Focus -- 1 Introduction -- 2 Modelling Systems and Attacks -- 3 Attacker Objectives -- 4 Refinement Checking -- 5 Implementation -- 6 Case Study -- 6.1 Amazon Delivery -- 6.2 Duqu Malware -- 7 Conclusion -- References -- Modelling of Hot Water Buffer Tank and Mixing Loop for an Intelligent Heat Pump Control -- 1 Introduction -- 2 Case House and Problem Statement -- 3 Buffer Tank and Mixing Loop Thermodynamics -- 4 System Modelling in Uppaal Stratego -- 4.1 Buffer Tank Modelling in Uppaal Stratego -- 4.2 Online Synthesis -- 5 Experimental Evaluation -- 5.1 Evaluation Setup -- 5.2 Buffer Tank Quality Assessment -- 5.3 Buffer Tank Evaluations with Intelligent Stratego Controller -- 5.4 Mixing Loop Evaluations with Intelligent Stratego Controller -- 6 Conclusion -- References -- Automated Property-Based Testing from AADL Component Contracts -- 1 Introduction -- 2 Background -- 3 Example -- 4 Property-Based Testing Framework Overview -- 5 GUMBOX Illustrated -- 6 Experience Report -- 7 Related Work -- 8 Conclusion -- References -- Impossible Made Possible: Encoding Intractable Specifications via Implied Domain Constraints -- 1 Introduction -- 2 Preliminaries: Mission-Time LTL and Formula-Wise Encoding -- 2.1 MLTL Formula-Wise AST Encoding Structure -- 2.2 MLTL AST Encoding Memory Requirements ch9KZJZR20 -- 3 MLTL Encoding Optimizations -- 4 Realizing Self-Reference via Slot-Based MLTL Encoding -- 5 Realizing Unboundedness via Dynamic Set Specification Unrolling -- 6 Realizing Counting via Domain-Bounded Dynamic Sets -- 7 Applying MLTL Rewrite Rules to DBDS Specifications -- 8 Impacts and Future Work -- References. 327 $aRobustness Verification of Deep Neural Networks Using Star-Based Reachability Analysis with Variable-Length Time Series Input -- 1 Introduction -- 2 Preliminaries -- 2.1 Neural Network Verification Tool and Star Sets -- 2.2 Time Series and Regression Neural Network -- 2.3 Reachability of a Time Series Regression Network -- 3 Adversarial Noise -- 4 Verification Properties -- 5 Robustness Verification Problem Formulation -- 6 Reachability of Specific Layers to Allow Variable-Length Time Series Input -- 7 Experimental Setup -- 7.1 Dataset Description -- 7.2 Network Description -- 8 Experimental Results and Evaluation -- 9 Conclusion and Future Work -- References -- Testing Logical Diagrams in Power Plants: A Tale of LTL Model Checking -- 1 Introduction -- 2 Logical Diagram -- 3 LTL Encoding of Logical Diagrams -- 3.1 LTL Encoding of Logical Diagrams and Initializing Functions -- 3.2 LTL Encoding of Properties -- 4 Proofs -- 5 Evaluation and Discussion -- References -- Optimal Spare Management via Statistical Model Checking: A Case Study in Research Reactors -- 1 Introduction -- 1.1 Related Work -- 2 Spare Management for a Research Reactor -- 2.1 Research Reactor -- 2.2 Optimal Spare Management -- 2.3 System Parameters -- 2.4 Performance Metrics -- 3 Preliminaries -- 3.1 Fault Trees -- 3.2 Stochastic Priced Timed-Game Automata -- 3.3 Uppaal Stratego -- 4 Methodology -- 5 INVAP Emergency Shutdown System as an SPTGA -- 6 Analysis and Results -- 6.1 Formal Queries -- 6.2 Analysis Results -- 6.3 Discussion -- 7 Conclusion and Future Work -- References -- Applying Rely-Guarantee Reasoning on Concurrent Memory Management and Mailbox in C/OS-ii: A Case Study -- 1 Introduction -- 2 Background -- 2.1 Rely-Guarantee Reasoning -- 2.2 Concurrent Reactive System and PiCore -- 3 Kernel Services in C/OS-ii -- 3.1 Data Structure -- 3.2 Mechanism of Kernel Services. 327 $a3.3 Safety Invariants of Kernel Service -- 4 Formal Modelling of Kernel Services of C/OS-ii -- 4.1 Execution Model of C/OS-ii -- 4.2 Formal Specification of Kernel Service of C/OS-ii -- 5 Correctness and Rely-Guarantee Proof -- 6 Experience Using PiCore -- 7 Related Work and Conclusion -- References -- Conformance in the Railway Industry: Single-Input-Change Testing a EULYNX Controller -- 1 Introduction -- 2 Background -- 2.1 Point Architecture in EULYNX -- 2.2 Programmable Logic Controllers -- 2.3 Single-Input-Change Testing -- 3 Interpretation of EULYNX Specifications -- 3.1 Proposed Interpretation -- 3.2 Formal Model -- 4 From FSM to SIC-DFSM -- 4.1 SIC-DFSM -- 4.2 SIC-DFSM Derivation -- 5 Case Study -- 5.1 Pipelines -- 5.2 Results -- 5.3 Validation -- 6 Related Work -- 7 Final Remarks -- References -- Author Index. 330 $aThis book constitutes the proceedings of the 28th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2023, held in Antwerp, Belgium, during September 20?22, 2023. The 14 full papers included in this book were carefully reviewed and selected from 24 submissions. The papers focus on development and application of formal methods in industry. FMICS is a platform for scientists and engineers who are active in the area of formal methods and interested in exchanging their experiences in the industrial usage of these methods. FMICS also strives to promote research and development for the improvement of formal methods and tools for industrial applications. . 410 0$aLecture Notes in Computer Science,$x1611-3349 ;$v14290 606 $aCompilers (Computer programs) 606 $aSoftware engineering 606 $aApplication software 606 $aArtificial intelligence 606 $aComputer science 606 $aComputer engineering 606 $aComputer networks 606 $aCompilers and Interpreters 606 $aSoftware Engineering 606 $aComputer and Information Systems Applications 606 $aArtificial Intelligence 606 $aTheory of Computation 606 $aComputer Engineering and Networks 615 0$aCompilers (Computer programs) 615 0$aSoftware engineering. 615 0$aApplication software. 615 0$aArtificial intelligence. 615 0$aComputer science. 615 0$aComputer engineering. 615 0$aComputer networks. 615 14$aCompilers and Interpreters. 615 24$aSoftware Engineering. 615 24$aComputer and Information Systems Applications. 615 24$aArtificial Intelligence. 615 24$aTheory of Computation. 615 24$aComputer Engineering and Networks. 676 $a004.0151 700 $aCimatti$b Alessandro$01429402 701 $aTitolo$b Laura$01429403 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910746292003321 996 $aFormal Methods for Industrial Critical Systems$93568348 997 $aUNINA