Formal Methods: Foundations and Applications: 25th Brazilian Symposium, SBMF 2022, Virtual Event, December 6–9, 2022, Proceedings

Description

This book constitutes the refereed proceedings of the 25th Brazilian Symposium on Formal Methods, SBMF 2022, which was held  virtually in December 2022. The 8 regular papers presented in this book were carefully reviewed and selected from 15 submissions. The symposium focuses on the development, dissemination, and use of formal methods for the construction of high-quality computational systems, aiming to promote opportunities for researchers and practitioners with an interest in formal methods to discuss the recent advances in this area.   Preface Organization Invited Talks Cooperative Verification Taming Monsters with Dragons: A Fractal Approach to Digital Twin Pipelines Developing an Open-Source, State-of-the-Art Symbolic Model-Checking Framework for the Model-Checking Research Community Some Applications of Formal Methods Contents Model Checking and Semantics An Efficient Customized Clock Allocation Algorithm for a Class of Timed Automata 1 Introduction 2 Timed automata 3 The Class TADS 4 The Notion of Optimality 5 Finding an Optimal Allocation of Clocks 5.1 Liveness Analysis of Clocks 5.2 Clock Allocation 5.3 The Clock Allocation Algorithm 5.4 Generating Clock Constraints and Clock Resets 6 Related Work and Conclusions References Formalization of Functional Block Diagrams Using HOL Theorem Proving 1 Introduction 2 Preliminaries 2.1 Formal ET Modeling 2.2 Formal ET Probabilistic Analysis 3 Functional Block Diagrams 4 FBD Formalization 4.1 Formal FBD Modeling 4.2 Formal FBD Probabilistic Analysis 5 Conclusions References Generation and Synthesis A Sound Strategy to Compile General Recursion into Finite Depth Pattern Matching 1 Introduction 2 Basic Definitions 3 Expansion and Transformation 3.1 Unrolling 3.2 Recursion Elimination 4 Term Generation 4.1 Soundness of Term Generation 5 Quick-Checking Properties 6 Related Work 7 Conclusion References Automatic Generation of Verified Concurrent Hardware Using VHDL 1 Introduction 1.1 Related Work 2 Theoretical Background 2.1 CSP 2.2 VHDL 3 CSP to VHDL Translation 3.1 Translation Overview 3.2 Restrictions 4 Tool Support 5 Case Study 6 Conclusion References Synthesis of Implementations for Divide-and-Conquer Specifications 1 Introduction 2 Preliminaries 3 From Divide-and-Conquer Specifications to Their Implementations 3.1 The Synthesis Rule 4 Case Study: Deriving an Implementation of a Greedy Algorithm 4.1 Weighted Matroids and Their Bases 4.2 Establishing max-basisI as a Divide-and-Conquer Specification 4.3 Implementations of Decomposition and Composition 5 Related Work 6 Conclusions and Outlook A The Three Auxiliary Lemmas References Verification and Solvers Compositional Verification of Simulink Block Diagrams Using tock-CSP and CSP-Prover 1 Introduction 2 Background 2.1 Block Diagrams and MDD 2.2 Running Example - Simple Actuator System (SAS) 2.3 Formal Verification and CSP 2.4 tock-CSP 2.5 Roscoe and Dathi's Compositional Deadlock Analysis Theory 2.6 CSP-Prover 3 Mechanised Compositional Verification of Timed Process Networks 3.1 Time-Stop Free Processes 3.2 Time-Stop Free Process Networks 3.3 Mechanisation in CSP-Prover 4 From Simulink to tock-CSP 5 Conclusion and Future Works References Excommunication: Transforming -Calculus Specifications to Remove Internal Communication 1 Introduction 2 The -Calculus 3 The Excommunication Algorithm 3.1 Transformation Rules 4 Example Application: A Leakage Analysis 4.1 An Application of the Leakage Analysis 5 Conclusion and Further Work References Level-Up - From Bits to Words 1 Introduction 2 Background 2.1 Verification Using Satisfiability Solvers 2.2 Word-Level Verification 3 Using Bit-Level Information on Word-Level 3.1 Computing Bit-Level Information 3.2 Bit-Level Information for the Example 3.3 Integration Strategies 3.4 Integration Strategies for Bit-Level Information 3.5 Implementation and Tool Chain 4 Evaluation Experiments 4.1 Experimental Setup 4.2 Experimental Results 5 Related Work 6 Conclusion and Outlook References Author Index