SPLASH Workshop/Symposium Events 2023
2023 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity (SPLASH Events 2023)
Powered by
Conference Publishing Consulting

9th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2023), October 22, 2023, Cascais, Portugal

FTSCS 2023 – Proceedings

Contents - Abstracts - Authors

9th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2023)

Frontmatter

Title Page


Welcome from the Chairs
This volume contains the proceedings of the Ninth ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2023), held in Caltais, Portugal, on October 22, 2023, as a satellite event of SPLASH 2023: The ACM SIGPLAN Conference on Systems, Programming, Languages, and Applications: Software for Humanity.

Invited Talk

Bounded STL Model Checking for Hybrid Systems (Invited Talk)
Kyungmin Bae ORCID logo
(Pohang University of Science and Technology, Republic of Korea)
Signal temporal logic (STL) is a temporal logic formalism for specifying properties of continuous signals. STL has been widely used for specifying, monitoring, and testing properties of hybrid systems that exhibit both discrete and continuous behavior. However, model checking techniques for hybrid systems have been primarily limited to invariant and reachability properties. This is mainly due to the intrinsic nature of hybrid systems, which involve uncountably many signals that continuously change over time. For hybrid systems, checking whether all possible behaviors satisfy an STL formula requires a certain form of abstraction and discretization, which has not been developed for general STL properties.
In this talk, I introduce bounded model checking algorithms and tools for general STL properties of hybrid systems. Central to our technique is a novel logical foundation for STL: (i) a syntactic separation of STL, which decomposes an STL formula into components, with each component relying exclusively on separate segments of a signal, and (ii) a signal discretization, which ensures a complete abstraction of a signal, given by a set of discrete elements. With this new foundation, the STL model checking problem can be reduced to the satisfiability of a first-order logic formula. This allows us to develop the first model checking algorithm for STL that can guarantee the correctness of STL up to given bound parameters, and a pioneering bounded model checker for hybrid systems, called STLmc.

Publisher's Version

Papers

Formal Verification of a Mechanical Ventilator using UPPAAL
Jaime Cuartas ORCID logo, David Cortés ORCID logo, Joan S. Betancourt ORCID logo, Jesús Aranda ORCID logo, José I. García ORCID logo, Andrés M. Valencia ORCID logo, and James Ortiz ORCID logo
(Universidad del Valle, Colombia; University of Namur, Belgium)
Mechanical ventilators are increasingly used for life support of critically ill patients. In this sense, despite recent technological advances, the accurate specification of their properties remains challenging, and the use of formal tools is limited. This work focuses on verifying the properties of the architecture of a mechanical ventilator using UPPAAL as a modeling tool. As a result, the system requirements and specification of a functional prototype were verified and improved using the formal model of a mechanical ventilator. This approach provides a valuable means of ensuring the correctness and reliability of mechanical ventilator systems.

Publisher's Version
Symbolic Analysis by Using Folding Narrowing with Irreducibility and SMT Constraints
Santiago EscobarORCID logo, Raúl López-RuedaORCID logo, and Julia Sapiña ORCID logo
(Universitat Politècnica de València, Spain)
Symbolic reachability analysis using rewriting with Satisfiability Modulo Theories (SMT) has been used to model different systems, including a variety of security protocols. Recently, it has also been used to analyze systems modeled using Parametric Timed Automata (PTAs). These techniques are based on reachability in a finite state graph generated from symbolic initial states where each generated state is constrained by an SMT expression checked for satisfiability. In this work, by rewriting with SMT but by narrowing with SMT. we use narrowing with SMT instead of rewriting with SMT. Narrowing with SMT allows a greater generalization, since (i) an infinite number of initial states may be represented by a finite number of states with variables, not only SMT variables, and (ii) an infinite state graph from an initial state may be represented by a finite state graph from another initial state with variables, not only SMT variables. We use graph search pruning techniques via irreducible terms and SMT constraints on conditional rules. This is supported by a novel folding SMT narrowing technique to represent infinite computations in a finite way. Additionally, we present a new textual user interface that allows the use of the algorithm in a simpler and more readable way.

Publisher's Version Info
Probabilistic Risk Assessment of an Obstacle Detection System for GoA 4 Freight Trains
Mario Gleirscher ORCID logo, Anne E. Haxthausen ORCID logo, and Jan Peleska ORCID logo
(University of Bremen, Germany; DTU, Denmark)
We propose a quantitative risk assessment approach for the design of an obstacle detection function for low-speed freight trains with grade of automation 4. In this five-step approach, starting with single detection channels and ending with a three-out-of-three model comprised of three independent dual-channel modules and a voter, we exemplify a probabilistic assessment, using a combination of statistical methods and parametric stochastic model checking. We illustrate that, under certain not unreasonable assumptions, the resulting hazard rate becomes acceptable for the discussed application setting. The statistical approach for assessing the residual risk of misclassifications in convolutional neural networks and conventional image processing software suggests that high confidence can be placed into the safety-critical obstacle detection function, even though its implementation involves realistic machine learning uncertainties.

Publisher's Version
Does Rust SPARK Joy? Safe Bindings from Rust to SPARK, Applied to the BBQueue Library
Aïssata Maiga ORCID logo, Cyrille Artho ORCID logo, Florian Gilcher ORCID logo, and Yannick Moy ORCID logo
(KTH Royal Institute of Technology, Sweden; Ferrous Systems, Germany; AdaCore, France)
Both Rust and SPARK are memory-safe programming languages and feature stronger safety guarantees than other popular programming languages for embedded software. However, modern systems often combine software written in multiple programming languages using the Foreign Function Interface (FFI). When using safety-oriented programming languages such as Rust and SPARK, maintaining compile-time safety guarantees across a language boundary is a challenge. The objective of this study is to explore if/how the inherent safety guarantees of these languages are preserved, and their potential benefits when establishing a library interface between them. In particular, we apply our method to the BBQueue circular buffer library that features complex ownership hand-over patterns when using FFI. Results reveal that most of the inherent consistency and safety features of these languages can be maintained. Yet, special caution is required at the FFI boundary to prevent potential vulnerabilities.

Publisher's Version
Solving Queries for Boolean Fault Tree Logic via Quantified SAT
Caz Saaltink ORCID logo, Stefano M. Nicoletti ORCID logo, Matthias Volk ORCID logo, Ernst Moritz Hahn ORCID logo, and Mariëlle Stoelinga ORCID logo
(University of Twente, Netherlands; Radboud University Nijmegen, Netherlands)
Fault trees (FTs) are hierarchical diagrams used to model the propagation of faults in a system. Fault tree analysis (FTA) is a widespread technique that allows to identify the key factors that contribute to system failure. In recent work we introduced BFL, a Boolean Logic for Fault trees. BFL can be used to formally define simple yet expressive properties for FTA, e.g.: 1) we can set evidence to analyse what-if scenarios; 2) check whether two elements are independent or if they share a child that can influence their status; 3) and set upper/lower boundaries for failed elements. Furthermore, we provided algorithms based on binary decision diagrams (BDDs) to check BFL properties on FTs. In this work, we evaluate usability of a different approach by employing quantified Boolean formulae (QBFs) instead of BDDs. We present a translation from BFL to QBF and provide an implementation—making it the first tool for checking BFL properties—that builds on top of the Z3 solver. We further demonstrate its usability on a case study FT and investigate runtime, memory consumption and scalability on a number of benchmark FTs. Lastly, qualitative differences from a BDD-based approach are discussed.

Publisher's Version Published Artifact Artifacts Available

proc time: 3.76