We evaluate the feasibility of generating formally verified C code that adheres to both functional and non-functional requirements using Large Language Models (LLMs) for three real industrial, automotive safety-critical software modules. We explore the capabilities of ten LLMs and four prompting techniques — Zero-Shot, Zero-Shot Chain-of-Thought, One-Shot, and One-Shot Chain-of-Thought — to generate C programs for the three modules. Functional correctness of generated programs is assessed through functional verification, and adherence to non-functional requirements is evaluated using an industrial static analyzer, along with human evaluation. The results demonstrate that it is feasible for LLMs to generate functionally correct code, with success rates of 540/800, 59/800, and 46/800 for the three modules. Additionally, the generated programs frequently adhere to the defined non-functional requirements. In the cases where the LLM-generated programs did not adhere to the non-functional requirements, deviations typically involve violations of single-read and single-write access patterns or minimal variable scope constraints. These findings highlight the promise and limitations of using LLMs to generate industrial safety-critical C programs, providing insight into improving automated LLM-based program generation in the automotive safety-critical domain.

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, communication delays, sensor ghost objects, machine learning, rounding errors, 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 first propose a contract metatheory for general input-output systems, allowing both probabilistic and non-probabilistic instantiations. Then, we instantiate the metatheory with probabilistic behaviors, introducing a new, fully trace-based probabilistic contract theory that supports general probability measures, continuous time, and continuous state spaces. To verify decompositions of such contracts, we also present a deductive system, which is illustrated by an industrially inspired automatic emergency braking example.

In this paper, we report on our experience with formally specifying and verifying an industrial software module, provided to us by a company from the heavy-vehicle industry. We start with a set of 32 informally stated requirements, also provided by the company. We discuss at length the formalization process of informally stated requirements for the purposes of their subsequent formal verification. Depending on the nature of each requirement, one of three languages was used: ACSL contracts, LTL or MITL. We use the Frama-C deductive verification framework to verify the source code of the module against the formalized requirements, with the outcome that 21 requirements are successfully verified while 6 are not. The remaining 5 requirements could not be verified for the module itself, as they specify behavior outside it. We illustrate what steps we took to convert LTL and MITL formulas into ACSL contracts to enable their verification in Frama-C. Finally, we discuss conclusions we drew from our work, notably that formal-verification-driven development of modules and verified breakdown of system requirements could likely remedy some problems we encountered.

Abstract According to the principles of compositional verification, verifying that lower-level components satisfy their specification ensures that the whole system satisfies its top-level specification. The key step is to ensure that the lower-level specifications constitute a correct decomposition of the top-level specification. In a non-stochastic context, such decomposition can be analyzed using techniques of theorem proving. In industrial applications, especially in safety-critical systems, specifications are often of stochastic nature, for example, giving a bound on the probability that a system failure will occur before a given time. A decomposition of such a specification requires techniques beyond traditional theorem proving. The first contribution of the paper is a theoretical framework that allows the representation of, and reasoning about, stochastic and timed behavior of systems as well as specifications for such behavior. The framework is based on traces that describe the continuous-time evolution of a system, and specifications are formulated using timed automata combined with probabilistic acceptance conditions. The second contribution is a novel approach to verifying decompositions of such specifications by reducing the problem to checking emptiness of the solution space for a system of linear inequalities.

Although commonly used in industry, a major drawback of Stateflow is that it lacks support for stochastic properties; properties that are often needed to build accurate models of real-world systems. In order to solve this problem, as the first contribution, Stochastic Stateflow (SSF) is presented as a stochastic extension of a subset of Stateflow models. As the second contribution, the tool SMP-tool is updated with support for SSF models specified in Stateflow. Finally, as the third contribution, an industrial case study is presented.

Big companies use many tools, jointly referred to as the toolchain, to manage vast amounts of engineering data being generated across an application lifecycle. Individual tools are typically designed to perform specific engineering tasks, and rely on specific data formats. This leads to problems when attempting to automate engineering tasks that are not supported by a particular tool, and which require data from multiple tools. This paper presents the experiences and lessons learned from an industrial research-project within the heavy vehicle manufacturer Scania, where the project goal was to identify and industrialize technologies and principles that solve the above problem. The presented lessons cover architectural, technological, and organizational aspects of a toolchain development-process. In addition, as a consequence of the lessons learned, the toolchain architecture and tool-interface architecture is also presented.

Functional safety standards such as IEC 61508 and ISO 26262 advocate a particularly stringent requirements engineering where safety requirements must be structured in a hierarchical manner and specified in accordance with the system architecture . In contrast to the stringent requirements engineering in functional safety standards, according to previous studies, requirements engineering in industry is in general of poor quality. Contracts theory has been previously shown to be suitable for supporting such a stringent requirements engineering effort; this support has also been implemented in tools. However, to use these contract-based tools, requirements must be formalized, which is a major challenge in industry. Therefore, to support current industrial requirements engineering practice and the stringent requirements engineering in functional safety standards, it is shown how tool support can be provided even when requirements, and also architectures, are not formalized. This is achieved by enforcing syntactic , yet formal, conditions in contracts theory. Despite the need for further validation, initial findings in an industrial case study indicate high potential in realizing the proposed support in an industrial setting.

A general, compositional, and component-based contract theory is proposed for modeling and specifying heterogeneous systems , characterized by consisting of parts from different domains, e.g. software, electrical and mechanical. Given a contract consisting of assumptions and a guarantee , clearly separated conditions on a component and its environment are presented where the conditions ensure that the guarantee is fulfilled—a responsibility assigned to the component, given that the environment fulfills the assumptions. The conditions are applicable whenever it cannot be ensured that the sets of ports of components are partitioned into inputs and outputs, and hence fully support scenarios where components, characterized by both causal and acausal models, are to be integrated by solely relying on the information of a contract. An example of such a scenario of industrial relevance is explicitly considered, namely a scenario in a supply chain where the development of a component is outsourced. To facilitate the application of the theory in practice, necessary properties of contracts are also derived to serve as sanity checks of the conditions. Furthermore, based on a graph that represents a structuring of a hierarchy of contracts, sufficient conditions to achieve compositionality are presented.

Product Lines (PL) in the systems engineering (SE) domain are one of the largest and most complex ones. The sheer number of different products that can be derived from PL points out to the scale of the challenge that Product Line Engineering (PLE) faces. Various development artifacts describe PL but due to their diversity, variability modeling across PL is a challenging task. Moreover, this complexity is a major obstacle for achieving traceability across PL which is especially important for product verification. In order to support systems engineering by establishing traceability across PL and aid verification planning we propose Multi-View Variability Model (MVVM). MVVM introduces a set of variability models that represent variability in various development artifacts, e.g. architecture, requirements etc. and corresponding inter-model constraints. We provide a formalization of MVVM and perform a transformation of the MVVM model to a Constraint Satisfiability Problem (CSP) where we formulate queries for the CSP model in order to extract information about variability dependencies among MVVM views. Throughout the paper we use a real system from the automotive domain as the working example in order to illustrate the introduced concepts.

ISO 26262 is the new standard for automotive functional safety. This standard identifies major process steps across a large number of system stages as well as safety-related artifacts required as input and output of these steps. The VeriSpec project intends to identify the main challenges for the adoption of ISO 26262 by the heavy-vehicle industry and to provide useful and industrially relevant "components" (methods, tools etc.) required by the standard. The project work targets two main research goals: (i) requirement formalization support, including a usable front-end for specifying requirements by using patterns, and (ii) formal analysis of realizations in form of architectural models at various levels of abstraction, by model-checking the formal representations of the latter. In this paper, we present the current challenges facing industry and justifying VeriSpec, together with a preliminary roadmap for the research.

The importance of using formal methods and techniques for verification of requirements in the automotive industry has been greatly emphasized with the introduction of the new ISO26262 standard for road vehicles functional safety. The lack of support for formal modeling of requirements still represents an obstacle for the adoption of the formal methods in industry. This paper presents a case study that has been conducted in order to evaluate the difficulties inherent to the process of transforming the system requirements from their traditional written form into semi-formal notation. The case study focuses on a set of non-structured functional requirements for the Electrical and Electronic (E/E) systems inside heavy road vehicles, written in natural language, and reassesses the applicability of the extended Specification Pattern System (SPS) represented in a restricted English grammar. Correlating this experience with former studies, we observe that, as previously claimed, the concept of patterns is likely to be generally applicable for the automotive domain. Additionally, we have identified some potential difficulties in the transformation process, which were not reported by the previous studies and will be used as a basis for further research.

This paper considers the problem of selecting a set of residual generators for inclusion in a model-based diagnosis system, while fulfilling fault isolability requirements and minimizing the number of residual generators. Two novel algorithms for solving the selection problem are proposed. The first algorithm provides an exact solution fulfilling both requirements and is suitable for small problems. The second algorithm, which constitutes the main contribution, is suitable for large problems and provides an approximate solution by means of a greedy heuristic and by relaxing the minimal cardinality requirement. The foundation for the algorithms is a novel formulation of the selection problem which enables an efficient reduction of the search-space by taking into account realizability properties, with respect to the considered residual generation method. Both algorithms are general in the sense that they are aimed at supporting any computerized residual generation method. In a case study the greedy selection algorithm is successfully applied in an industrial sized automotive engine system.

In fault detection and isolation, diagnostic test results are commonly used to compute a set of diagnoses, where each diagnosis points at a set of components which might behave abnormally. In distributed systems consisting of multiple control units, the test results in each unit can be used to compute local diagnoses while all test results in the complete system give the global diagnoses. It is an advantage for both repair and fault-tolerant control to have access to the global diagnoses in each unit since these diagnoses represent all test results in all units. However, when the diagnoses, for example, are to be used to repair a unit, only the components that are used by the unit are of interest. The reason for this is that it is only these components that could have caused the abnormal behavior. However, the global diagnoses might include components from the complete system and therefore often include components that are superfluous for the unit. Motivated by this observation, a new type of diagnosis is proposed, namely, the condensed diagnosis. Each unit has a unique set of condensed diagnoses which represents the global diagnoses. The benefit of the condensed diagnoses is that they only include components used by the unit while still representing the global diagnoses. The proposed method is applied to an automotive vehicle, and the results from the application study show the benefit of using condensed diagnoses compared to global diagnoses.

To handle diagnosis with behavioral modes, a new generalized minimal hitting-set algorithm is presented. The key properties in comparison with that of the original minimal hitting-set algorithm given by de Kleer and Williams are that it can handle more than two modes per component and also nonpositive conflicts. The algorithm computes a logical formula that characterizes all diagnoses. Instead of minimal or kernel diagnoses, some specific conjunctions in the logical formula are used to characterize the diagnoses. These conjunctions are a generalization of both minimal and kernel diagnoses. From the logical formulas, it is also easy to derive the set of preferred diagnoses. One usage of the algorithm is fault isolation in the sense of fault detection and isolation (FDI). The algorithm is experimentally shown to provide significantly better performance compared to the fault isolation approach based on structured residuals, which is commonly used in FDI.

An essential step in the design of a model-based diagnosis system is to find a set of residual generators fulfilling stated fault detection and isolation requirements. To be able to find a good set, it is desirable that the method used for residual generation gives as many candidate residual generators as possible, given a model. This paper presents a novel residual generation method that enables simultaneous use of integral and derivative causality, i.e., mixed causality, and also handles equation sets corresponding to algebraic and differential loops in a systematic manner. The method relies on a formal framework for computing unknown variables according to a computation sequence. In this framework, mixed causality is utilized, and the analytical properties of the equations in the model, as well as the available tools for algebraic equation solving, are taken into account. The proposed method is applied to two models of automotive systems, a Scania diesel engine, and a hydraulic braking system. Significantly more residual generators are found with the proposed method in comparison with methods using solely integral or derivative causality.

In model-based diagnosis, diagnostic system construction is based on a model of the technical system to be diagnosed. To handle large differential algebraic models and to achieve fault isolation, a common strategy is to pick out small overconstrained parts of the model and to test these separately against measured signals. In this paper, a new algorithm for computing all minimal overconstrained subsystems in a model is proposed. For complexity comparison, previous algorithms are recalled. It is shown that the time complexity under certain conditions is much better for the new algorithm. This is illustrated using a truck engine model.