11345nam 2200565 450 99649556940331620230305174830.03-031-19849-2(MiAaPQ)EBC7119891(Au-PeEL)EBL7119891(CKB)25179629600041(OCoLC)1348482928(PPN)265855861(EXLCZ)992517962960004120230305d2022 uy 0engurcnu||||||||txtrdacontentcrdamediacrrdacarrierLeveraging applications of formal methods, verification and validationPart I verification principles : 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22-30, 2022, proceedings /Tiziana Margaria and Bernhard Steffen (editors)Cham, Switzerland :Springer,[2022]©20221 online resource (608 pages)Lecture notes in computer science ;Volume 13701Print version: Margaria, Tiziana Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles Cham : Springer International Publishing AG,c2022 9783031198489 Includes bibliographical references and index.Intro -- Introduction -- Organization -- Contents - Part I -- SpecifyThis - Bridging Gaps Between Program Specification Paradigms -- SpecifyThis - Bridging Gaps Between Program Specification Paradigms -- 1 Introduction -- 2 Summary of Contributions -- References -- Deductive Verification Based Abstraction for Software Model Checking -- 1 Introduction -- 2 Overview of the Verification Approach -- 3 Deductive Verification and Frama-C -- 4 Model Checking and TLA -- 4.1 The TLA Framework -- 4.2 Translating Code and Contracts into TLA -- 5 Contracts as a Unifying Theory -- 5.1 An Abstract Contract Theory -- 5.2 Deductive Verification in the Abstract Contract Theory -- 5.3 Procedure-Modular Verification with TLA -- 5.4 Contract Based System Design -- 6 Preliminary Evaluation -- 6.1 Simple File Open-Close Example -- 6.2 Simplified Industrial Example -- 7 Conclusion -- References -- Abstraction in Deductive Verification: Model Fields and Model Methods -- 1 Introduction -- 2 Logical Encoding of Local Computations -- 3 Encoding Heap Access and Update-Previous and Related Work -- 3.1 Notation -- 3.2 Heaps as Maps -- 3.3 Arrays -- 3.4 Embedding in SMT -- 4 Model Fields and Model Methods -- 5 Simple Example -- 6 Using Model Methods -- 7 Encoding Model Methods -- 8 Contrast and Conclusion -- References -- A Hoare Logic with Regular Behavioral Specifications -- 1 Introduction -- 2 Motivation -- 3 Approach -- 3.1 Preliminaries and Notation -- 3.2 Regular Behavioral Specifications -- 3.3 Programs and Behavioral Correctness -- 3.4 Hoare Logic Proof Rules -- 4 Tool Support in SecC -- 4.1 Specification Syntax -- 4.2 Verification Engine -- 5 Case Studies -- 5.1 Case Study: Regular Expression Matching -- 5.2 Case-Study: VerifyThis Casino Challenge -- 5.3 Discussion -- 6 Related and Alternative Approaches -- 7 Conclusion -- References.Specification-Based Monitoring in C++ -- 1 Introduction -- 2 Related Work -- 3 Overview -- 4 The Specification Language -- 4.1 Events -- 4.2 A Simple State Machine -- 4.3 Some Alternative Monitors -- 4.4 Monitoring Events that Carry Data -- 4.5 Referring to the Past -- 4.6 A Complex Property -- 4.7 The Complete Grammar -- 5 Usage -- 6 Implementation -- 7 Experiment -- 7.1 Setting Up the Experiment -- 7.2 Result and Interpretation -- 8 Conclusion -- A Visualization of Monitors -- References -- Specification and Verification with the TLA+ Trifecta: TLC, Apalache, and TLAPS -- 1 Introduction -- 2 Specifying Termination Detection -- 3 Verification by Model Checking and Theorem Proving -- 3.1 Finite-State Model Checking Using tlc -- 3.2 Bounded Model Checking with Apalache -- 3.3 Theorem Proving Using tlaps -- 4 Safra's Algorithm for Termination Detection -- 5 Analyzing Safra's Algorithm -- 5.1 Model Checking Correctness Properties -- 5.2 Safra's Algorithm Implements Termination Detection -- 5.3 Proving Correctness Using tlaps -- 6 Conclusion -- References -- Selective Presumed Benevolence in Multi-party System Verification -- 1 Introduction -- 2 Smart Contracts, Solidity and Reentrancy -- 3 Semantics of Solidity and Handling of Callbacks -- 4 Presumption of Benevolence -- 4.1 Presuming Benevolence of Oneself -- 4.2 Presuming Benevolence of a Static Group -- 4.3 Presuming Benevolence of a Dynamic Group -- 5 Collaborative Malicious Behaviour -- 6 Conclusions -- References -- On the Pragmatics of Moving from System Models to Program Contracts -- 1 Introduction -- 2 The PGP Server Hagrid -- 3 The Alloy Model -- 4 From Alloy to VCC Contracts -- 4.1 Precondition and Framing Analysis -- 4.2 Translation to Annotated C -- 4.3 Contract Augmentation -- 5 Discussion -- References -- X-by-Construction Meets Runtime Verification.X-by-Construction Meets Runtime Verification -- 1 Motivation -- 2 Aim -- 3 Contributions -- 3.1 CbC: Robustness, Co-piloting, and Digital Twinning -- 3.2 CbC and RV: Configurable and Cyber-Physical Systems -- 3.3 XbC: Security, Resilience, and Consumption Properties -- 3.4 CbC and RV: Reinforcement Learning and Synthesis -- References -- Robustness-by-Construction Synthesis: Adapting to the Environment at Runtime -- 1 Introduction -- 2 Preliminaries -- 3 Adaptive Strategies -- 3.1 Definitions -- 3.2 Computing Adaptive Strategies -- 4 Strongly Adaptive Strategies -- 4.1 Bad Moves -- 4.2 Motivating Example -- 4.3 Definitions -- 4.4 Existence of Strongly Adaptive Strategies -- 4.5 Computing Strongly Adaptive Strategies -- 5 Conclusion -- References -- TriCo-Triple Co-piloting of Implementation, Specification and Tests -- 1 Introduction -- 1.1 Triple Co-piloting at a Glance -- 2 Emerging Trends in Software Technology -- 2.1 Code Synthesis Through Large Language Models -- 2.2 Automated Test Case Generation -- 2.3 Specification Synthesis -- 2.4 Formal Software Verification -- 3 The TriCo Methodology -- 3.1 Envisaged Workflow -- 3.2 Use Cases -- 3.3 Envisaged Technology -- 4 Research Efforts Required for TriCo -- 5 Turning Vision into Reality -- References -- Twinning-by-Construction: Ensuring Correctness for Self-adaptive Digital Twins -- 1 Introduction -- 2 Twinned-by-Construction Systems -- 3 Twinning-by-Construction and Temporal Properties -- 4 The Digital Thread as a Temporal Property -- 5 Related Work -- 6 Conclusion -- References -- On Formal Choreographic Modelling: A Case Study in EU Business Processes -- 1 Introduction -- 2 Background -- 3 Legal Provisions -- 4 Formal Models -- 5 From BPMN to Global Choreographies -- 6 Conclusions and Future Work -- References -- Configurable-by-Construction Runtime Monitoring -- 1 Introduction.2 The Quest of Configurable Runtime Monitoring -- 2.1 Feature-Oriented Example -- 2.2 Challenges -- 2.3 This Paper -- 3 Configurable Automata-Based Monitoring -- 3.1 Preliminaries -- 3.2 Featured Monitors -- 3.3 Synthesizing Featured Monitors -- 3.4 Concise Featured Monitors -- 4 Configurable Stream-Based Monitoring -- 4.1 Preliminaries -- 4.2 Configurable Lola -- 4.3 Family-Based Specification Analysis -- 5 Concluding Remarks -- References -- Runtime Verification of Correct-by-Construction Driving Maneuvers -- 1 Introduction -- 2 Workflow by Example -- 3 Modeling and Verifying Maneuvers with Hybrid Mode Automata -- 3.1 Formalization of Hybrid Mode Automata -- 3.2 Verification Based on Differential Dynamic Logic -- 4 Runtime Verification of HMA Models -- 4.1 Generating Monitor Conditions for Runtime Verification -- 4.2 Simulation -- 5 Evaluation -- 5.1 Case Studies and Setup -- 5.2 Results and Insights -- 6 Related Work -- 7 Conclusion -- References -- Leveraging System Dynamics in Runtime Verification of Cyber-Physical Systems -- 1 Introduction -- 2 Preliminary Concepts -- 2.1 Signal Model -- 2.2 Signal Temporal Logic (STL) ch16mn04 -- 3 Exploiting Knowledge of System Dynamics -- 3.1 Motivating Example -- 3.2 System Model -- 3.3 Knowledge of Signal Dynamics -- 3.4 Using Partial Knowledge -- 4 Monitoring Distributed CPS -- 4.1 Distributed CPS Architecture -- 4.2 Additional Challenges in the Distributed Setup -- 5 Using Verified Dynamics -- 6 Conclusion -- References -- Automated Repair of Security Errors in C Programs via Statistical Model Checking: A Proof of Concept -- 1 Introduction -- 2 Background and Related Work -- 2.1 Essentials of Statistical Model Checking -- 2.2 Trace Execution Properties -- 2.3 Probabilistic Verification -- 2.4 SMC Tools -- 3 Illustrative Example -- 3.1 SMC-Based Validation -- 3.2 Using Traces for Automated Program Repair.4 Designing a Repair Agent -- 4.1 A SMC-Based Program Repair Algorithm -- 5 Implementation and Experimental Results -- 5.1 Experimental Results -- 6 Conclusions and Future Work -- References -- Towards Safe and Resilient Hybrid Systems in the Presence of Learning and Uncertainty -- 1 Introduction -- 2 Background -- 2.1 Reinforcement Learning (RL) -- 2.2 Simulink and the RL Toolbox -- 2.3 Differential Dynamic Logic -- 2.4 Transformation from Simulink to dL -- 2.5 Stochastic Hybrid Model -- 2.6 Signal Temporal Logic -- 2.7 Learning Optimal Decisions for Stochastic Hybrid Systems -- 3 Related Work -- 4 Combining Deductive and Quantitative Analyses -- 4.1 An Intelligent Water Distribution System -- 4.2 Formal Verification of Safety and Resilience -- 4.3 Resilient Scheduling Under Uncertainty -- 5 Evaluation -- 5.1 Deductive Verification -- 5.2 Quantitative Analysis -- 6 Conclusion -- References -- Non-functional Testing of Runtime Enforcers in Android -- 1 Introduction -- 2 Background -- 2.1 Runtime Policy -- 2.2 Policy Enforcement Models -- 3 Test4Enforcers -- 3.1 Test Case Generation -- 3.2 Test Execution -- 4 Evaluation -- 5 Related Work -- 6 Conclusion and Future Work -- References -- Automata Learning Meets Shielding -- 1 Introduction -- 2 Related Work -- 3 Preliminaries -- 3.1 Markov Decision Processes and Reinforcement Learning -- 3.2 Learning of MDPs -- 3.3 Shielding in MDPs -- 4 Learned Shields for Safe RL -- 4.1 Setting and Problem Statement -- 4.2 Overview of Iterative Safe RL via Learned Shields -- 4.3 Details for Training Using Learned Shields -- 5 Experiments -- 5.1 Case Study Subjects -- 5.2 Experimental Results -- 5.3 Zigzag Gridworlds -- 5.4 Slippery Shortcuts Gridworlds -- 5.5 Wall Gridworlds -- 5.6 Discussion -- 6 Conclusion -- References -- Safe Policy Improvement in Constrained Markov Decision Processes -- 1 Introduction.2 Motivating Example.Lecture notes in computer science ;Volume 13701.Artificial intelligenceCongressesData miningCongressesElectronic data processingCongressesArtificial intelligenceData miningElectronic data processing006.3Margaria-Steffen Tiziana1964-Steffen BernhardMiAaPQMiAaPQMiAaPQBOOK996495569403316Leveraging applications of formal methods, verification and validation2055774UNISA