Formal methods : foundations and applications : 24th Brazilian Symposium, SBMF 2021, virtual event, December 6-10, 2021 : proceedings / Sérgio Campos, Marius Minea (eds.).

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.