Fundamental Approaches to Software Engineering

Inhaltsverzeichnis

1. Frontmatter

   PDF-Version jetzt herunterladen

2. Capturing System Designs with Formal Executable Specifications

   • Open Access

   José Meseguer

   Abstract

   Basing system designs on informal specifications and applying formal methods after system implementation greatly reduces the benefits that formal methods can provide. Systems of high quality and trustworthiness can be developed in a faster and much more efficient way by capturing system designs with formal executable specifications and subjecting them to automated formal verification from the earliest stages of system design. Even greater benefits can be gained by making such formal designs highly composable and reusable by means of formal patterns. The experience on using the rewriting-logic-based language Maude and its tool environment and formal patterns for all these purposes is presented and illustrated with concrete examples. The benefits of combining model-based design approaches with the one based on formal executable specifications is also discussed an illustrated with examples.

   PDF-Version jetzt herunterladen

3. Towards Large Language Model Guided Kernel Direct Fuzzing

   • Open Access

   Xie Li, Zhaoyue Yuan, Zhenduo Zhang, Youcheng Sun, Lijun Zhang

   Abstract

   Direct kernel fuzzing is a targeted approach that focuses on specific areas of the kernel, effectively addressing the challenges of frequent updates and the inherent complexity of operating systems, which are critical infrastructure. This paper introduces SyzAgent, a framework integrating LLMs with the state-of-the-art kernel fuzzer Syzkaller, where the LLMs are used to guide the mutation and generation of test cases in real-time. We present preliminary results demonstrating that this method is effective on around 67% cases in our benchmark during the experiment.

   PDF-Version jetzt herunterladen

4. DeepCRCEval: Revisiting the Evaluation of Code Review Comment Generation

   • Open Access

   Junyi Lu, Xiaojia Li, Zihan Hua, Lei Yu, Shiqi Cheng, Li Yang, Fengjun Zhang, Chun Zuo

   Abstract

   Code review is a vital but demanding aspect of software development, generating significant interest in automating review comments. Traditional evaluation methods for these comments, primarily based on text similarity, face two major challenges: inconsistent reliability of human-authored comments in open-source projects and the weak correlation of text similarity with objectives like enhancing code quality and detecting defects.

   This study empirically analyzes benchmark comments using a novel set of criteria informed by prior research and developer interviews. We then similarly revisit the evaluation of existing methodologies. Our evaluation framework, DeepCRCEval, integrates human evaluators and Large Language Models (LLMs) for a comprehensive reassessment of current techniques based on the criteria set. Besides, we also introduce an innovative and efficient baseline, LLM-Reviewer, leveraging the few-shot learning capabilities of LLMs for a target-oriented comparison.

   Our research highlights the limitations of text similarity metrics, finding that less than 10% of benchmark comments are high quality for automation. In contrast, DeepCRCEval effectively distinguishes between high and low-quality comments, proving to be a more reliable evaluation mechanism. Incorporating LLM evaluators into DeepCRCEval significantly boosts efficiency, reducing time and cost by 88.78% and 90.32%, respectively. Furthermore, LLM-Reviewer demonstrates significant potential of focusing task real targets in comment generation.

   PDF-Version jetzt herunterladen

5. VOCE: A Virtual On-Call Engineer for Automated Alert Incident Analysis Using a Large Language Model

   • Open Access

   Jia Chen, Xiaolei Chen, Jie Shi, Peng Wang, Wei Wang

   Abstract

   In a service system, operations engineers generally deploy numerous monitoring mechanisms in system components to detect anomalies caused by system faults and generate alerts, also known as alarms, that record the phenomenon of anomalies. Due to the topological relationships between system components, a system fault in a system component may affect other components and result in various local anomalies and generate multiple alerts across different components. Therefore, to facilitate troubleshooting, alerts of the same system fault are usually correlated into one group, called alert incident. However, although there are existing approaches that can automatically correlate alerts for operations engineers, analyzing alert incidents still rely on manual work. In this paper, we propose an approach, VOCE (Virtual On-Call Engineer). Using the emerging capabilities of a large language model, VOCE can automatically comprehend the anomaly information described by alerts and emulate the process of operations engineers analyzing an alert incident. Extensive experiments conducted on real alert incidents and two popular large language models demonstrate the effectiveness and efficiency of VOCE in automatically analyzing alert incidents.

   PDF-Version jetzt herunterladen

6. Hybridize Functions: A Tool for Automatically Refactoring Imperative Deep Learning Programs to Graph Execution

   • Open Access

   Raffi Khatchadourian, Tatiana Castro Vélez, Mehdi Bagherzadeh, Nan Jia, Anita Raja

   Abstract

   Efficiency is essential to support responsiveness w.r.t. ever-growing datasets, especially for Deep Learning (DL) systems. DL frameworks have traditionally embraced deferred execution-style DL code—supporting symbolic, graph-based Deep Neural Network (DNN) computation. While scalable, such development is error-prone, non-intuitive, and difficult to debug. Consequently, more natural, imperative DL frameworks encouraging eager execution have emerged but at the expense of run-time performance. Though hybrid approaches aim for the “best of both worlds,” using them effectively requires subtle considerations to make code amenable to safe, accurate, and efficient graph execution—avoiding performance bottlenecks and semantically inequivalent results. We discuss the engineering aspects of a refactoring tool that automatically determines when it is safe and potentially advantageous to migrate imperative DL code to graph execution and vice-versa.

   PDF-Version jetzt herunterladen

7. Compositional Learning for Synchronous Parallel Automata

   • Open Access

   Mahboubeh Samadi, Aryan Bastany, Hossein Hojjat

   Abstract

   Automata learning is an approach for extracting a model in the shape of an automaton from a black-box system. This approach has recently gained much attention in both industry and academia. In this paper, we introduce a compositional automata learning algorithm for systems comprising synchronous parallel components. Our algorithm assumes no prior knowledge about the number of components, their individual alphabets, and the synchronizing alphabets. The learning process is automatic and figures out the alphabet symbols on-the-fly during learning the components. We prove that the proposed algorithm terminates and correctly learns the individual components. We use a number of case studies from the industrial automotive domain and synthetic benchmarks to evaluate the performance of the proposed algorithm. The experimental results show that the algorithm requires significantly fewer input symbols and resets to learn the system compositionally.

   PDF-Version jetzt herunterladen

8. Symbolic State Partitioning for Reinforcement Learning

   • Open Access

   Mohsen Ghaffari, Mahsa Varshosaz, Einar Broch Johnsen, Andrzej Wąsowski

   Abstract

   Tabular reinforcement learning methods cannot operate directly on continuous state spaces. One solution to this problem is to partition the state space. A good partitioning enables generalization during learning and more efficient exploitation of prior experiences. Consequently, the learning process becomes faster and produces more reliable policies. However, partitioning introduces approximation, which is particularly harmful in the presence of nonlinear relations between state components. An ideal partition should be as coarse as possible, while capturing the key structure of the state space for the given problem. This work extracts partitions from the environment dynamics by symbolic execution. We show that symbolic partitioning improves state space coverage with respect to environmental behavior and allows reinforcement learning to perform better for sparse rewards. We evaluate symbolic state space partitioning with respect to precision, scalability, learning agent performance and state space coverage for the learned policies.

   PDF-Version jetzt herunterladen

9. Formal Architectural Patterns for Adaptive Robotic Software

   • Open Access

   James Baxter, Bert van Acker, Morten Kristensen, Thomas Wright, Ana Cavalcanti, Cláudio Gomes

   Abstract

   It is often the case that a robot must adapt to unexpected changes in its environment. It is, however, important that these changes can be demonstrated to maintain the safe operation of the robot. The adaptive systems community has developed the MAPE-K pattern as a widely recognised conceptual architecture. We propose extending MAPE-K to incorporate runtime verification, resulting in an architecture we call MAPLE-K. In this paper, we capture and formalise both the MAPE-K and MAPLE-K architectures using a domain-specific language. Additionally, we provide support for translation from architectural models to software models and code to facilitate the deployment of verified applications. MAPE-K is rarely maintained at the implementation level, but our work ensures traceability between the code and its design, enabling the use of architectural information to verify the correctness of the software.

   PDF-Version jetzt herunterladen

10. RoboScene: Notation for Formal Verification of Human-Robot Interaction

    • Open Access

    Holly Hendry, Ana Cavalcanti, Cade McCall, Mark Chattington

    Abstract

    Proving properties about robotic systems with humans-in-the-loop relies on assumptions about human behaviour. Existing technologies require expertise not reasonably expected from psychologists and human-factors engineers, for instance. A user-needs analysis of industrial design techniques for human-robot interaction has identified a lack of standardised approach. We present RoboScene, a notation based on UML sequence diagrams that can be used to capture assumptions derived from human-factors artefacts, through novel constructs enabling consideration of stakeholders with different traits. We describe a tock-CSP semantics for RoboScene, and show how we can connect (mathematically) RoboScene diagrams to platform-independent software models. This is applied in the context of a Human-Centered Engineering process, demonstrated via an industrial case study.

    PDF-Version jetzt herunterladen

11. Stochastic Timed Graph Transformation Systems

    • Open Access

    Sven Schneider, Maria Maximova, Holger Giese

    Abstract

    The correct operation of safety-critical distributed embedded systems is crucial. Following a model-driven approach, the relevant system aspects must be captured and rigorous ideally fully-automatic analysis of (probabilistic) timed safety properties must be supported. Probabilistic Timed Graph Transformation Systems (PTGTSs) support the modeling of such systems and analysis of such properties via model checking or simulation. However, they only support the modeling of probabilistic choice with a fixed numbers of outcomes and non-deterministic timing delays via timing constraints limiting applicability (descriptive expressiveness) and usefulness (precision of analysis results).

    To remedy this drawback of PTGTSs, we (a) extend PTGTSs to Stochastic Timed Graph Transformation Systems (STGTSs) integrating discrete/continuous random variables to capture stochastic behavior and (b) outline an adaptation of PTGTS model checking for STGTSs to enable analysis w.r.t. probabilistic timed safety properties. Relying on a running example in which shuttles navigating on a track topology must avoid derailing, we exemplify STGTS support for modeling and analysis.

    PDF-Version jetzt herunterladen

12. Prove your Colorings: Formal Verification of Cache Coloring of Bao Hypervisor

    • Open Access

    Axel Ferréol, Laurent Corbin, Nikolai Kosmatov

    Abstract

    Hypervisors allow sharing of computing resources between applications—possibly of various levels of criticality—that makes them increasingly relevant for modern embedded systems. In this context, memory isolation properties (including low-level cache isolation) are essential to guarantee. This paper presents a case study on formal verification of the cache coloring mechanism implemented in the Bao hypervisor. It proposes an original technique for coloring memory pages and assigning to each virtual machine only pages of certain colors, aimed to provide strong isolation guarantees. The implementation presents several challenges for formal verification, such as bit-level operations, complex arithmetic operations, multiple levels of nested loops, and linked lists. We identify two subtle bugs in the existing implementation breaking the expected guarantees, and propose bug fixes. We provide formal specification for the key functions of the mechanism and verify their (fixed) version in the Frama-C verification platform with a few lemmas proved in the Coq proof assistant. We present our specification choices, verification approach and obtained results. Finally, we outline possible optimizations of the current implementation.

    PDF-Version jetzt herunterladen

13. Reasoning about Substitutability at the Level of JVM Bytecode

    • Open Access

    Marco Paganoni, Carlo A. Furia

    Abstract

    Subtyping in object-oriented languages is widely based on Liskov’s substitution principle, which offers static correctness guarantees of type safety while abstracting implementation details. Unfortunately, the type systems of languages like Java cannot statically enforce full behavioral substitutability, and in fact there are numerous examples of libraries some of whose components are related by inheritance but not substitutable (for example, because they do not implement “optional” operations).

    In this paper, we present a novel approach to precisely specify and reason about substitutability in JVM languages. A distinctive feature of our approach is that it targets JVM bytecode, as opposed to a program’s source code, as it is based on the ByteBack deductive verifier. To support reasoning about substitutability, we extended ByteBack with ghost specifications, a (restricted) form of class invariants, and substitutability-preserving specification inheritance (precondition weakening and postcondition strengthening). Equipped with these features, ByteBack can now reason precisely about behavioral substitutability violations in a way that is applicable to realistic examples (such as with optional operations of Java’s List interface). Our experiments also demonstrate that ByteBack can analyze substitutability in programs written in a combination of JVM languages, including multi-language code where Scala or Kotlin code interacts with Java libraries.

    PDF-Version jetzt herunterladen

14. Advances in Automatic Software Testing: Test-Comp 2025

    • Open Access

    Dirk Beyer

    Abstract

    The 7th edition of the Competition on Software Testing (Test-Comp 2025) provides an overview and comparative evaluation of automatic test-suite generators for C programs. The experimental evaluation was performed on a benchmark set of 11 226 test-generation tasks for C programs. Each test-generation task consisted of a program and a test specification. The test specifications included error coverage (generate a test suite that exhibits a bug) and branch coverage (generate a test suite that executes as many program branches as possible). Test-Comp 2025 evaluated 20 software systems for test generation that are all freely available. This included 13 test-suite generators that participated with active support from teams led by 12 different representatives from 8 countries (actively maintained software systems, participation in competition jury). Test-Comp 2025 had 1 new participant ( ) and 2 re-entries (ESBMC-incr, ESBMC-kind). The evaluation included also 7 test-generation tools from previous years.

    PDF-Version jetzt herunterladen

15. Fizzer with Local Space Fuzzing

    (Competition Contribution)

    • Open Access

    Martin Jonáš, Jan Strejček, Marek Trtík

    Abstract

    Fizzer is a gray-box fuzzer introduced at Test-Comp 2024. This paper summarizes the lessons learned with the original version and describes the major changes including new analyses implemented in the current version of Fizzer. In particular, Fizzer now uses dynamic taint-flow analysis and local space fuzzing. We also provide experimental results showing the progress between the two versions.

    PDF-Version jetzt herunterladen

16. ESBMC v7.7: Automating Branch Coverage Analysis Using CFG-Based Instrumentation and SMT Solving

    (Competition Contribution)

    • Open Access

    Chenfeng Wei, Tong Wu, Rafael Sa Menezes, Fedor Shmarov, Fatimah Aljaafari, Sangharatna Godboley, Kaled Alshmrany, Rosiane de Freitas, Lucas C. Cordeiro

    Abstract

    ESBMC, a bounded model checking (BMC) verifier based on SMT solving, has demonstrated its effectiveness in bug detection in recent software verification competitions. We extend its capabilities to enable branch coverage analysis and test suite generation. Our contributions are twofold: (1) we define a branch coverage property and instrument the control flow graph (CFG) to compute branch coverage using SMT solving, and (2) we propose an incremental multi-property reasoning algorithm for efficient and sound test case generation. ESBMC is ranked 7th in the Cover-Branches category of Test-Comp 2025.

    PDF-Version jetzt herunterladen

17. Backmatter

    PDF-Version jetzt herunterladen