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

Title Page

Message from the Chairs

Probabilistic Risk Assessment of an Obstacle Detection System for GoA 4 Freight Trains
Mario Gleirscher , Anne E. Haxthausen , and Jan Peleska 
(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.

Article Search

Does Rust SPARK Joy? Safe Bindings from Rust to SPARK, Applied to the BBQueue Library
Aïssata Maiga , Cyrille Artho , Florian Gilcher , and Yannick Moy 
(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.

Article Search

Solving Queries for Boolean Fault Tree Logic via Quantified SAT
Caz Saaltink , Stefano M. Nicoletti , Matthias Volk , Ernst Moritz Hahn , and Marielle Stoelinga 
(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.

Article Search Artifacts Available

Formal Verification of a Mechanical Ventilator using UPPAAL
Jaime Cuartas , David Cortés , Joan S. Betancourt , Jesús Aranda , José I. García , Andrés M. Valencia , and James Ortiz 
(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.

Article Search

Symbolic Analysis by Using Folding Narrowing with Irreducibility and SMT Constraints
Santiago Escobar , Raúl López-Rueda , and Julia Sapiña 
(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.

Article Search Info