Formal Methods: Foundations and Applications
24th Brazilian Symposium, SBMF 2021, Virtual Event, December 6-10, 2021, Proceedings
Published on 25. November 2021
IX, 141 pages
978-3-030-92137-8 (ISBN)
Description
This book constitutes the refereed proceedings of the 24rd Brazilian Symposium on Formal Methods, SBMF 2021, which was held in December 2021. Due to COVID 19-pandemic it took place virtually.
The 8 regular papers presented in this book were carefully reviewed and selected from 15 submissions. The papers detail 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
The 8 regular papers presented in this book were carefully reviewed and selected from 15 submissions. The papers detail 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
More details
Series
Edition
1st ed. 2021
Language
English
Place of publication
Cham
Switzerland
Publishing group
Springer International Publishing
Product notice
Reflowable
Illustrations
IX, 141 p. 40 illus., 16 illus. in color.
File size
9,18 MB
ISBN-13
978-3-030-92137-8 (9783030921378)
DOI
10.1007/978-3-030-92137-8
Schweitzer Classification
Other editions
Additional editions
Sérgio Campos | Marius Minea
Formal Methods: Foundations and Applications
24th Brazilian Symposium, SBMF 2021, Virtual Event, December 6-10, 2021, Proceedings
Book
11/2021
Springer
€58.84
Shipment within 7-9 days
Content
- Intro
- Preface
- Organization
- Contents
- A Two-Level Approach Based on Model Checking to Support Architecture Conformance Checking
- 1 Introduction
- 2 Theoretical Background
- 2.1 Model Checking
- 2.2 Temporal Logic and Hybrid Logic
- 2.3 Software Versioning
- 3 The Proposed Method
- 3.1 Call Graphs as Kripke Structures
- 3.2 Version Graphs as Kripke Structures
- 3.3 The Proposed Logic: A Two-Level Temporal Logic for Specifications Checking
- 3.4 Examples
- 4 Conclusion and Future Works
- References
- Statistical Model Checking for Traffic Models
- 1 Introduction
- 2 Background
- 2.1 SMC and MultiVeStA
- 2.2 SUMO - Simulation of Urban MObility
- 2.3 Car-Following and Lane Changing Models
- 3 Integration of MultiVeStA and SUMO Simulator
- 3.1 Initial Step
- 3.2 Integration
- 4 Simulation Experiments and Results
- 4.1 Simple Queries
- 4.2 Query 1: Behaviour on Emergency Vehicles
- 4.3 Query 2: Traffic Load Comparison
- 4.4 Query 3: Load Conditions for Traffic Jams
- 4.5 Query 4: Impending Drop in Traffic
- 4.6 Running Times
- 5 Conclusion and Future Work
- References
- Visual Specification of Properties for Robotic Designs
- 1 Introduction
- 2 Background
- 2.1 RoboChart
- 2.2 UML Activity Diagram
- 2.3 CSP Notation, Templates and Tools Used in the Work
- 3 Diagrammatic Language for Properties
- 3.1 Language Syntax
- 3.2 Language Semantics
- 4 Tool Support
- 5 Related Work
- 6 Conclusion
- References
- Model Checking and Strategy Synthesis for Multi-agent Systems for Resource Allocation
- 1 Introduction
- 2 Multi-agent Systems for Resource Allocation
- 3 Propositional Logic Encoding
- 3.1 Overall Encoding
- 3.2 Basic Encodings
- 3.3 Properties of the Encoding
- 4 Algorithm
- 5 Implementation and Experiments
- 6 Related Work
- 7 Conclusion and Outlook
- References
- Temporal Reasoning Through Automatic Translation of tock-CSP into Timed Automata
- 1 Introduction
- 2 Background
- 3 An Overview of the Translation Technique
- 4 Evaluation
- 4.1 Experimental Evaluation
- 4.2 Mathematical Proof
- 5 Related Work and Conclusions
- References
- Module Integration Using Graph Grammars (MIGRATE)
- 1 Introduction
- 2 Graph Grammars
- 3 Illustration of the Proposed Approach
- 4 Module Nets
- 5 MIGRATE Approach
- 5.1 Translation
- 5.2 Verification
- 6 Related Work
- 7 Conclusion
- References
- Cost Analysis for an Actor-Based Workflow Modelling Language
- 1 Introduction
- 2 Formal Workflow Modelling Language Rpl
- 2.1 The Syntax of Rpl
- 2.2 The Semantics of Rpl
- 3 Analysis of Rpl Program
- 3.1 Synchronisation Schema
- 3.2 Accumulated Costs
- 3.3 Translation Function
- 4 Properties
- 5 Related Work
- 6 Conclusion
- References
- Minimization of the Number of Clocks for Timed Scenarios
- 1 Introduction
- 2 Preliminaries
- 2.1 Timed Automata
- 2.2 Timed Scenarios
- 3 A New Optimization Algorithm
- 3.1 Cyclic Dependencies
- 3.2 Cyclic Dependencies and Equality Constraints
- 3.3 C(Ds) with Cyclic Dependencies
- 3.4 Resolving Cyclic Dependencies
- 3.5 The Optimization Algorithm
- 4 Conclusions
- References
- Author Index
