Because ensembles and swarms occur everywhere in nature, in social and in technical contexts, their modeling and programming is one of the challenges of modern software systems engineering. While it is well-known how self-adaptive or autonomic systems can be designed advantageously (Kounev et al., 2017), this often requires the engineering of new software languages with a tremendous development effort. This paper presents a novel context-role-adaptive approach for modeling and programming of ensembles and swarms that relies on a small library in Julia (1300 SLOC), exploiting its facilities for metaprogramming, multiple dispatch, and equational modeling. We demonstrate the validity of the approach with a tutorial on two scenarios from the technical and natural domain in which ensembles are represented by (dynamic) contexts. RailCabs are shuttle-based autonomous trains, self-forming ensembles, represented as contexts that re-group during their travels. Bird swarms show specific formations, represented as contexts to save energy and to prevent attackers. In the latter case study, we show how to model the dynamic behavior of the birds with an equational modeling library in Julia. Therefore, the paper contributes a new library-based approach to Context-Role-oriented Equational Modeling of Ensembles (CREME).
In order for future development environments to support the production of highly trustworthy software in an efficient, developer friendly way, an integrated exploitation of three building blocks will be essential: language servers, LLM-based copiloting, and verification technology. The formal methods community has long faced challenges with the availability of modern, user-friendly tooling, potentially affecting its broader adoption in industry. This paper explores the complex and rapidly evolving landscape of development tooling within modern programming environments. Given this rapid advancement, developers and researchers, often concentrated on their specific subfields, face uncertainty about where to begin when creating development tools. This paper aims to provide an informal guide to the existing design space surrounding code assistants and copilots. We explore successful projects within the realm of theorem proving and verification, describing their high-level design components and how they relate to each other. This work also examines how existing tools can be leveraged to facilitate the development of new formal methods tooling, building upon established abstractions. Moreover, we present visions for the future of formal methods tooling, drawing insights from the successes and limitations of current systems.
The evolution of automotive systems has been rapid. Nowadays, electronic brains control dozens of functions in vehicles, like braking, cruising, etc. Model-based design approaches, in environments such as MATLAB Simulink, seem to help in addressing the ever-increasing need to enhance quality, and manage complexity, by supporting functional design from predefined block libraries, which can be simulated and analyzed for hidden errors, but also used for code generation. For this reason, providing assurance that Simulink models fulfill given functional and timing requirements is desirable. In this paper, we propose formal syntax and semantics of Simulink blocks and their composition, and introduce the tool SIMPPAAL that automates a previously introduced pattern-based, execution-order preserving transformation of Simulink atomic and composite blocks into stochastic timed automata. The resulting model can then be analyzed formally with UPPAAL Statistical Model Checker. We validate the approach on an industrial prototype called the Brake-by-Wire system. This work enables the formal analysis of industrial Simulink models, by automatically generating their semantic counterpart.
Formal specification is the prerequisite for verification of behavioral properties of programs. Most specification languages are tied to the programming language they specify, the features and the verification techniques they support can differ substantially. Complex, particularly, concurrent behavior, requires non-intuitive and low-level specifications. Together with language-specificity, this causes specification languages to suffer from a lack of interoperability. Even when two specifications expressed in different languages are intended to describe the same behavior, they cannot be easily compared, let alone formally analyzed. Context-aware trace contracts (CATs) are a highly expressive specification trace logic that can describe complex behaviors intuitively and independently of an underlying programming language. We propose CATs as a lingua franca for behavioral specification. We demonstrate how target language-specific formalisms can be desugared into CATs, resulting in intuitive, comparable specifications, that are independent of code. We illustrate the desugaring process for the Java Modeling Language and apply it to an excerpt of the Casino case study.
Cyber-physical systems are systems that exhibit both discrete computational and continuous physical behavior. They are often subject to different kinds of uncertainty, ranging from sensor noise over random component failures to inconfidences induced by sample-based statistical learning. Quantitative formal methods have proven to be especially useful for assessing the impact of uncertainty on the system evolution over time. However, they lack compositionality. Existing methods for compositional design and verification, such as contracts, traditionally abstract from or (over-)approximate probability distributions, and resort to purely qualitative safety assessments in worst-case scenarios. This paper proposes a first step towards the integration of probabilistic methods into contract-based verification schemes to enable compositional reasoning over uncertain system behavior. We discuss different sources of uncertainties, as well as the necessity of probabilistic contracts for cyber-physical systems. Our key idea for integrating probabilities into contracts is the identification of safe yet precise approximations for sets of distributions, for which we use subdistributions. With that, we hope to reconcile probabilistic with set-based reasoning.
Informal requirements are often ambiguous, hence leaving the choice of an interpretation to the implementation phase. In this paper, we describe an experience in the development of a safety-critical software component for on-board train control. Despite the requirements being part of the ERTMS standard, the development resulted in multiple iterations, with increases in cost and delays in delivery. These problems could be traced back to ambiguities of the natural language. As a result, we investigate a formal approach for the analysis of requirements. The idea is to formalize the informal specifications while ensuring traceability, and to encode various forms of validation. The methodology is based on Satisfiability Modulo Theories and encompasses user-defined as well as structural properties.
The SyDPaCC framework supports the development of scalable parallel functional programs with COQ and helps the developers to write correct-by-construction programs with respect to specifications written as simple (and possibly very inefficient) functional programs. Parallel programs are built from specifications using verified program transformations offered by SyDPaCC. Leveraging the COQ extraction mechanism, compilable code can be obtained and executed on shared-memory or large scale distributed memory parallel machines. This paper presents the usage of SyDPaCC via an example, explains the internals of SyDPaCC and gives a tour of the program transformations provided by the framework.
In industrial-sized cyber-physical systems, ensuring fulfillment of requirements gets increasingly more costly as the number of components increases. To make the task feasible, compositional verification has been suggested as a scalable solution. Such techniques allow verification by divide-and-conquer, often using assume-guarantee contracts. Although previous research has focused mostly on the non-probabilistic setting, in the real world, probabilities often arise due to random hardware failures, stochastic communication delays, sensor ghost objects, machine learning components, rounding errors caused by finite-precision arithmetic, human behavior, and probabilistic algorithms. Therefore, for contract theories to be practically relevant to cyber-physical systems, there is a need to support probabilistic reasoning, for instance regarding safety and reliability. To this end, we propose a completely trace-based probabilistic contract theory, supporting general probability measures, continuous time, and continuous state spaces. To verify decompositions of such contracts, we also present a deductive system, which is illustrated on an industrially inspired automatic emergency braking example.
Interoperability between deductive program verification tools is a well-recognized long-standing challenge. In this paper we propose a solution for a well-delineated aspect of this challenge, namely the exchange of abstract contracts for possibly stateful interfaces that represent modularity boundaries. Interoperability across tools, specification paradigms, and programming languages is achieved by focusing on abstract implementation-independent behavioral models. The approach, called Contract-LIB in reminiscence of the widely-successful SMT-LIB format, aims to standardize the language over which such contracts are formulated and provides clear guidance on its integration with established methods to connect high-level specifications with code-level data structures. We demonstrate the ideas with examples, define syntax and semantics, and discuss the rationale behind key design decisions.
This paper gives an overview of previous work in which the authors used NASA's Formal Requirement Elicitation Tool (FRET) to formalise requirements. We discuss four case studies where we used FRET to capture the system's requirements. These formalised requirements subsequently guided the case study specifications in a combination of formal paradigms. For each case study we summarise insights gained during this process, exploring the expressiveness and the potential interoperability of these approaches. Our experience confirms FRET's suitability as a framework for the elicitation and understanding of requirements and for providing traceability from requirements to specification.
GPUexplore, a GPU-accelerated explicit-state LTL model checker, achieves significant speedups compared to sequential and multi-core CPU model checkers, but it is limited by the amount of memory available on GPUs. Partial-Order Reduction is a way to remedy this problem, by excluding unnecessary transitions and states from exploration. For this work, we implemented the ample and clustered-ample reduction techniques in GPUexplore. Experiments show that our implementations achieve reductions similar to the state-of-the-art Breadth-First Search configurations of multi-core LTSmin and sequential DiVinE and Spin without introducing significant computational overhead, even though LTSmin applies stubborn set reduction, which has often been reported as the most effective technique. At times, ample and cample reduction even speeds up exploration 4–100 × .
We consider algorithms for parity games that use attractor decomposition, such as Zielonka's recursive algorithm, priority promotion, and tangle learning. In earlier work, we identified the Two Counters parity game family that requires exponential time for many algorithms, including attractor decomposition algorithms, and we identified the main mechanism that slows down parity game algorithms as so-called distractions. We observe a fundamentally different approach in avoiding distractions between algorithms that use attractor decomposition and algorithms that compute progress measures. We now propose an alternative attractor-based method to avoid distractions by applying the attractor decomposition recursively. We demonstrate that this algorithm solves the Two Counters games efficiently, but that a modification of the Two Counters method can also delay the recursive algorithm exponentially.
Model checking temporal properties of software is algorithmically hard. To be practically feasible, it usually requires the creation of simpler, abstract models of the software, over which the properties are checked. However, creating suitable abstractions is another difficult problem. We argue that such abstract models can be obtained with little effort, when the state transformation properties of the software components have already been deductively verified. As a concrete, language-independent representation of such abstractions we propose the use of flow graphs, a formalism previously developed for the purposes of compositional model checking. In this paper, we describe how we envisage the work flow and tool chain to support the proposed verification approach in the context of embedded, safety-critical software written in C.
Many formal verification techniques are concerned with comparing system behaviours with formal specifications. Although runtime verification has followed this path (comparing observed traces against formal properties), it has traditionally been burdened with another task-that of raising a flag when a violation is detected. Different approaches can be found in the literature: identifying the earliest such instance, identifying all instances, identifying instances where (potentially future) violations are inevitable, etc. We argue that the lack of a clear distinction between the notion of system correctness and the hard-wired means of identification of points when violation is somehow detected, conflates the notions of points-of-detection and points-of-violation. Frequently, the point at which a point-of-violation may be detected is independent of the point of interest itself, and also independent of the point-of-reaction if a corrective measure is needed. We observe that this distinction becomes more salient in some cases, such as deontic specification languages, which may identify notions such as permission, and in the case of multi-agent systems, where the notion of blame is essential. Using practical and varied examples we motivate why these limitations are significant for the field of runtime verification.
