Development of a digital assistant to facilitate the use of model checking in product engineering processes

Abstract

With increasing computing power and advances in electronic technology, embedded systems which consist of a combination of hardware and software to perform a certain function, can nowadays execute more sophisticated software, leading to the implementation of more functions and capabilities. Systems with high functionality, such as autonomous systems, are unfortunately often also safety-critical systems. In safety-critical systems, failures can cause high costs and even endanger human lives. Experience has shown that the impact of software failures can range from minor inconvenience to catastrophic consequences, such as the explosion of the Ariane 5 heavy lift launch system. The high complexity of the software system makes it extremely difficult to detect subtle errors or to replicate them during testing or prior to deployment. The concept of verifying the correctness of software or hardware through testing has often proven inadequate for these complex systems. In this paper, the focus is placed on the Product Engineering Processes (PEP) of the automotive industry, in particular on discrete manufacturing, in which goods, e.g. automobiles, are produced that consist of many individual parts that must be assembled along a production line. The need to ensure the reliability and integrity of the embedded software systems in the automotive industry has led to the introduction of the Automotive Software Performance Improvement and Capability dEtermination (A-SPICE) standard, which supervises the manufacturing and operation of software systems and requires verification of the correctness of these systems. Essentially, A-SPICE provides guidelines and best practices for automotive suppliers to ensure safety and thus prevent the occurrence of catastrophic events. One method of ensuring safety of embedded systems, preventing errors and defects in software, and thus, complying with the A-SPICE standard, is the formal verification technique such as model checking. Model checking is a method of verifying the correctness of a system by considering all possible behaviours of a system. Probabilistic model checking, a mature technique that evolved from model checking, extends conventional model checking with tools and techniques for analysing systems that exhibit random or stochastic phenomena. Unfortunately, although model checking is a powerful tool for verifying the correctness of a system, its complex language and unfamiliar specification methods make it difficult for an organization to fully implement it or for auditors to assess compliance of the systems with ASPICE. Therefore, this work is concerned with the development of a digital assistant that reduces the difficulty and effort to perform model checking and thus facilitates model checking for everyone. In its development, the digital assistant applies state-of-the-art methods of Natural Language Processing (NLP), which is part of Artificial Intelligence that makes natural texts in human language understandable to computers and machines. The process begins with the user asking the digital assistant for a specific model checking result such as probability, duration or cost. The digital assistant then sends the data to the Probabilistic Symbolic Model Checker (PRISM) on the backend to compute the results based on the user's request. The digital assistant then retrieves the results from PRISM and sends the requested answer back to the user.