Top

2025 | Book

Read chapter Read first chapter

Formal Methods: Foundations and Applications

27th Brazilian Symposium, SBMF 2024, Vitória, Brazil, December 4–6, 2024, Proceedings

Editors: Sidney C. Nogueira, Ciprian Teodorov

Publisher: Springer Nature Switzerland

Book Series : Lecture Notes in Computer Science

Part of: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Table of Contents

About this book

This book constitutes the refereed proceedings of the 27th Brazilian Symposium on Formal Methods: Foundations and Applications, SBMF 2024, held in Vitória, Brazil, during December 4–6, 2024.

The 8 full papers and 4 short papers included in this book were carefully reviewed and selected from 18 submissions. They were organized in topical sections as follows: Formal Analysis and Verification in Temporal and Symbolic Systems; Formal Semantics and Verification of UML Models; Formal Verification and Proof Techniques in Algorithms and Logics; and Formal Methods for Security and Privacy.

Frontmatter

Formal Analysis and Verification in Temporal and Symbolic Systems

Frontmatter

On the Existence of Unions of Timed Scenarios

Abstract

In earlier work it was shown that, given two consistent timed scenarios, there might not exist a scenario whose semantics is the union of those of the two. A sufficient condition for the non-existence of such a union was also identified. In this paper we report on a comprehensive study of the union operation for scenarios. We identify a new sufficient condition that provides a syntactic criterion for the existence of a scenario that is the union of two given scenarios. We also prove that the condition is necessary.

Neda Saeedloei

SMTQuery: Analysing SMT-LIB String Benchmarks

Abstract

Constraint satisfaction problems involving strings have been a subject of theoretical study for decades, but it is only in recent years that practical solving methods have begun to emerge. This increasing interest in solving string constraints led to the development of various techniques and solvers, often accompanied by specific benchmark sets. As a result, there is now a substantial corpus of publicly available, yet largely unclassified, such benchmarks. In this context, we present SMTQuery, a framework for maintaining and analyzing benchmarks for SMT string problems. SMTQuery enables the execution of user-defined queries to extract domain-specific information from these benchmarks, facilitating a deeper analysis of the underlying problems. We demonstrate its utility by analyzing over 100,000 benchmarks and training an algorithm selection model to match benchmarks with suitable solvers.

Mitja Kulczynski, Kevin Lotz, Florin Manea, Danny Bøgsted Poulsen, Paul Sarnighausen-Cahn

Autonomous Vehicles Path Planning Under Temporal Logic Specifications

Abstract

Path planning is an essential component of autonomous driving. A global planner is responsible for the high-level planning. It basically performs a shortest-path search on a known map, thereby defining waypoints used to control the local (low-level) planner. Local planning is a runtime verification method which is repeatedly run on the vehicle itself in real-time, so as to find the optimal short-horizon path which leads to the desired waypoint in a way which is both efficient and safe. The challenge is that the local planner has to take into account repeatedly incoming updates about the information available of the environment. In addition, it performs a complex task, as it has to take into account a large variety of requirements, originating from the necessity of collision avoidance with obstacles, respecting traffic rules, sticking to regulatory requirements, and lastly to reach the next waypoint efficiently. In this paper, we describe a logic-based specification mechanism which fulfills all these requirements.

Akshay Dhonthi, Nicolas Schischka, Ernst Moritz Hahn, Vahid Hashemi

Formal Semantics and Verification of UML Models

Frontmatter

A CSP Semantics for UML State Machines Aiming at Hidden Formal Methods Verification

Abstract

The increasing complexity of software systems, especially in safety-critical domains, requires rigorous verification methodologies to ensure reliability and correctness. This paper presents a semantics for UML state machines using the formal language CSP to support automatic property verification. Our approach integrates the intuitive modeling capabilities of UML with the precise verification tooling available for CSP, thus facilitating the detection and correction of design errors at the early stages of system development. We implemented a framework as a plugin for the Astah modeling tool, which translates UML diagrams into CSP specifications and utilizes the FDR model checker for verification. The results are traced back to the diagram level, thus hiding the complexity of formal notations and tools. A case study of a flashlight system demonstrates the practical applicability and benefits of our approach, highlighting its ability to identify and solve design issues early in the development process.

Diego Ferreira, Lucas Lima

Verifying Integrated Designs of UML State Machines and Activities Using CSP

Abstract

This paper presents a framework for verifying deadlock and nondeterminism in UML state machines integrated with activities, addressing the critical need for automated checks in UML projects. The framework aims to support architects and system designers in modeling and verifying properties of state machine diagrams integrated with activity diagrams, emphasizing the absence of deadlock and nondeterminism, crucial aspects of critical systems. We implemented this tool as a plug-in for the Astah modeling environment, utilizing the Astah API to read the components used in state machine and activity diagrams. We consider the formal language CSP as the underlying semantic domain, and we verify the translated models using the FDR tool. In the case of an issue is found, an interactive counterexample is generated in the modeling platform, facilitating the identification of the reasons for the failure and to hide the complexity of the rigorous notation and manipulation of formal method tooling. The paper also discusses the developed semantics, a case study, and the functionalities of the framework. Additionally, it compares this work with related approaches and discusses its limitations and future directions.

Diego Ferreira, Lucas Lima

An Integrated Framework for Analysing, Simulating and Testing UML Models

Abstract

UML is widely adopted for modelling object-oriented software systems, including diagrams that cover the several facets of the entire development life cycle. Approaches to formal semantics of UML tend to concentrate on individual diagrams and, so far, no complete, standard, semantics is available. Here, we explore a different path and define a natural-language semantics for a component UML model that embodies state machines and composite structure diagrams. We then integrate with the NAT2TEST strategy to provide means for analysis (via model checking and theorem proving), simulation and testing. The integration is based on a systematic process (mapping rules), and its soundness has been validated considering an independent reference formal semantics. The developed tool support automates the translation from UML models to natural-language requirements directly based on the proposed mapping rules. We illustrate our contributions and tool support with respect to two case studies: the classical Dijkstra’s dining philosophers problem, and a distributed ring-buffer model.

Gustavo Carvalho, José Dihego, Augusto Sampaio

Formal Verification and Proof Techniques in Algorithms and Logics

Frontmatter

Brzozowski’s Algorithm for Automata Minimization Verified in Coq

Abstract

Deterministic finite automata are abstract machines that play a vital role in computer science and control engineering, aiding in the development of compilers, search algorithms, modeling of discrete event systems and more. With the aim of optimizing computational resources, minimization algorithms have been developed to eliminate unreachable and indistinguishable states in these automata. Brzozowski’s algorithm is one such method which involves reversing and determinizing the automaton twice. Despite its apparent simplicity, proving the correctness of this minimization method requires various inductive strategies. For this purpose, the Coq proof assistant was employed to streamline the proof and provide a means of verification for the algorithm. In addition to the related demonstrations, this paper contributes with a straightforward representation of automata in functional programming languages. This approach uses only lists and types with decidable equality, so that common data structures can be utilized to represent finite automata. It also offers an accessible explanation for the reasoning process.

Filipe Ramos, Karina Girardi Roggia, Rafael Castro G. Silva

Soundness-Preserving Fusion of Modal Logics in Coq

Abstract

This work presents the formal verification of the concept of fusion of modal logics in the Coq proof assistent, along with a proof of the preservation of soundness. Our formalization is based on previous work by da Silveira et al. that formalizes several normal modal systems using Coq and proves their soundness and weak completeness. We give a high level description of the base library, how we modified it to fit our needs, how we defined fusion and how we proved the transfer of soundness. Our definition allows for the fusion of any normal modal logics, with any amount of modalities, requiring no changes to the definitions in the library.

Miguel Alfredo Nunes, Karina Girardi Roggia, Paulo Henrique Torrens

Formally Verified Implementation of the K-Nearest Neighbors Classification Algorithm

Abstract

Classification, one of the most commonly applied algorithmic techniques in data mining, involves assigning a class label to observations based on previously seen data. Among the most ubiquitous and well-known approaches to classification is K-nearest neighbor (\(K\)NN) search, which predicts the class label for a query by determining the plurality class of its K-nearest data points. In this paper, we present a mechanically verified implementation of a K-nearest neighbors classification algorithm in the Coq proof assistant, a powerful formal verification tool. Formally certifying the implementation, by proving that it meets its specification, provides a strong guarantee and high confidence that the classifier actually produces results in the expected manner. Given the conceptually simple nature of the \(K\)NN algorithm, this serves as a good baseline for developing specification and verification techniques for machine learning implementations.

Bernny Velasquez, Jessica Herring, Nadeem Abdul Hamid

Formal Methods for Security and Privacy

Frontmatter

Formal Verification of Forward Secrecy and Post-Compromise Security for TreeKEM

Abstract

The TreeKEM protocol is the preeminent implementation candidate for the Message Layer Security standard. Prior work analyzed TreeKEM by defining the Continuous Group Key Agreement security game, which facilitated proof of some security guarantees and also identified protocol deficiencies which were subsequently remedied. This work extends such applications by formalizing the Continuous Group Key Agreement security game through multiple soundness preserving abstractions. The model is parameterized by N, representing an unbounded protocol duration among N distinct participants. Once formalized, the game is encoded within Promela and essential security guarantees are verified for \(N \le 16\) via the model checker Spin. This represents a notable achievement, both in practical security terms for the TreeKEM protocol, as well as demonstrating scalability techniques for non-trivial parameter bounds when modeling a complex, concurrent protocol.

Alex J. Washburn, Subash Shankar

Formal Privacy Analyses for Open Banking

Abstract

The term “Open Banking” describes a series of global initiatives to allow the sharing of customer data between financial companies to facilitate competition within their sector. In this paper, we formalise in the rigorous framework of quantitative information flow (QIF) relevant privacy risks in a concrete Open Banking scenario, namely: (i) transaction-history recovery and (ii) collateral attribute-inferences using external correlations. We provide extensive analyses of these risks in real-world data from Open Banking, supplied by a fintech in Australia. We show that the Open Banking system studied presents considerable privacy risks with respect to transactions, both in the presence and in the absence of demographic data. Finally, we exemplify potential real-world collateral attribute-inference attacks, in which we show how an attacker might leverage scientific correlations to infer individuals’ level of neuroticism and self-control from their transaction history. We hope that this work may: (i) help financial customers in Australia make better-informed decisions about what kind of information, and how much of it, to share via Open Banking; (ii) raise awareness about the potential privacy risks of Open Banking in other countries; and (iii) foster the development of privacy regulation in digital finance and the open data economy.

Luigi D. C. Soares, Mário S. Alvim, Di Bu, Natasha Fernandes, Yin Liao

Trusted Deployer: A Tool for Safe Creation and Upgrade of Ethereum Smart Contracts

Abstract

The lack of systematic and, particularly, mechanised support to ensure a safe creation and upgrade of smart contracts has led to the deployment of instances with flaws that have been thoroughly exploited, putting digital assets at risk. Formal verification can potentially help to eliminate these high impact flaws, particularly by allowing one to check whether smart contracts obey some desired properties. We have already proposed the concept of a trusted deployer to address these issues. In this work we present the detailed design of a public, open-source, and off-chain tool that supports the creation and upgrade of smart contracts, ensuring that they meet corresponding formal specifications. We detail the tool’s overall architecture, its usage, and its applicability to real-world smart contracts.

Juliandson Ferreira, Pedro Antonino, Augusto Sampaio, A. W. Roscoe, Filipe Arruda

Backmatter

Title: Formal Methods: Foundations and Applications
Editors: Sidney C. Nogueira
Ciprian Teodorov
Publisher: Springer Nature Switzerland
Electronic ISBN: 978-3-031-78116-2
Print ISBN: 978-3-031-78115-5
DOI: https://doi.org/10.1007/978-3-031-78116-2