Test or prove? These two approaches to software verification have long been presented as opposites. One is dynamic, the other static: A test executes the program, a proof only analyzes the program text. A different perspective is emerging, in which testing and proving are complementary rather than competing techniques for producing software of verified quality. Work performed over the past few years and reviewed here develops this complementarity by taking advantage of "design by contract," as available in Eiffel, and exploiting a feature of modern program-proving tools based on "satisfiability modulo theories" (SMT): counterexample generation. A counterexample is an input combination that makes the program fail. If we are trying to prove a program correct, we hope not to find any. One can, however, apply counterexample generation to incorrect programs, as a tool for automatic test generation . We can also introduce faults into a correct program and turn the counterexamples into an automatically generated regression test suite with full coverage. Additionally, we can use these mechanisms to help produce program fixes for incorrect programs, with a guarantee that the fixes are correct. All three applications, leveraging on the mechanisms of Eiffel and design by contract, hold significant promise to address some of the challenges of program testing, software maintenance, and automatic program repair.

Test or prove? These two approaches to software verification have long been presented as opposites. One is dynamic, the other static: a test executes the program, a proof only analyzes the program text. A different perspective is emerging, in which testing and proving are complementary rather than competing techniques for producing software of verified quality. Work performed over the past few years and reviewed here develops this complementarity by taking advantage of Design by Contract, as available in Eiffel, and exploiting a feature of modern program-proving tools based on “Satisfiability Modulo Theories” (SMT): counterexample generation. A counterexample is an input combination that makes the program fail. If we are trying to prove a program correct, we hope not to find any. One can, however, apply counterexample generation to incorrect programs, as a tool for automatic test generation. We can also introduce faults into a correct program and turn the counterexamples into an automatically generated regression test suite with full coverage. Additionally, we can use these mechanisms to help produce program fixes for incorrect programs, with a guarantee that the fixes are correct. All three applications, leveraging on the mechanisms of Eiffel and Design by Contract, hold significant promise to address some of the challenges of program testing, software maintenance and Automatic Program Repair.

Large language model (LLM)-based tools such as ChatGPT seem useful for classical programming assignments. The more specialized the field, the more likely they lack reliability because of the lack of data to train them. In the case of quantum computing, the quality of answers of generic chatbots is low. C4Q is a chatbot focused on quantum programs that addresses this challenge through a software architecture that integrates specialized LLMs to classify requests and specialized question answering modules with a deterministic logical engine to provide trustworthy quantum computing support. This article describes the latest version (2.0) of C4Q, which delivers several enhancements: ready-to-run Qiskit code for gate definitions and circuit operations, expanded features to solve software engineering tasks such as the travelling salesperson problem and the knapsack problem, and a feedback mechanism for iterative improvement. Extensive testing of the backend confirms the system's reliability, while empirical evaluations show that C4Q 2.0's classification LLM reaches near-perfect accuracy. The evaluation of the result consists in a comparative study with three existing chatbots highlighting C4Q 2.0's maintainability and correctness, reflecting on how software architecture decisions, such as separating deterministic logic from probabilistic text generation impact the quality of the results.

Automatic program repair usually relies heavily on test cases for both bug identification and fix validation. The issue is that writing test cases is tedious, running them takes much time, and validating a fix through tests does not guarantee its correctness. The novel idea in the Proof2Fix methodology and tool presented here is to rely instead on a program prover, without the need to run tests or to run the program at all. Results show that Proof2Fix automatically finds and fixes significant historical bugs.

MCDC, for "Modified Condition/Decision Coverage", is a test coverage criterion recommended in several important industrial software safety standards. The intuition behind MCDC is that it should be more effective than industry's default coverage criterion, branch coverage, since it uses a finer-grain decomposition of program conditions. Manually generating MCDC-compliant test suites is, however, tedious and error-prone; there is, as a result, little empirical evidence of whether that intuition holds up in practice. Does MCDC really provide enough of an advantage over branch coverage to justify the extra work and longer test runs? To help answer this question, the present work takes advantage of verification technology that combines tests and proofs, based on the Auto-Proof program verifier. For each decision point in the program, the approach proceeds in four steps. First, compute a set of conditions that satisfy MCDC. Then, inject into the program, for each combination, an incorrect instruction (a "seeded contradiction" in the terminology of previous work). Next, apply the prover to verify the instrumented program; the prover naturally fails, but in the process it produces a set of counterexamples covering all the combinations. Finally, turn this result into a directly usable test suite-guaranteed by construction to satisfy the MCDC criterion. The results, on a significant set of example programs, yield insights on how MCDC coverage compares to branch coverage and adaptive random testing when trying to detect faults.

Quantum computing is a growing field that promises many real-world applications such as quantum cryptography or quantum finance. The number of people able to use quantum computing is however still very small. This limitation comes from the difficulty to understand the concepts and to know how to start coding. Therefore, there is a need for tools that can assist non-expert in overcoming this complexity. One possibility would be to use existing conversational agents. Unfortunately ChatGPT and other Large-Language Models produce inaccurate results. This article presents C4Q, a chatbot that answers accurately basic questions and guides users when trying to code quantum programs. Contrary to other approaches C4Q uses a pre-trained large language model only to discover and classify user requests. It then generates an accurate answer using an own engine. Thanks to this architectural design, C4Q's answers are always correct, and thus C4Q can become a support tool that makes quantum computing more available to non-experts.

Upon release, ChatGPT3.5 shocked the software engineering community by its ability to generate answers to specialized questions about coding. Immediately, many educators wondered if it was possible to use the chatbot as a support tool that helps students answer their programming questions. This article evaluates this possibility at three levels: fundamental Computer Science knowledge (basic algorithms and data structures), core competency (design patterns), and advanced knowledge (quantum computing). In each case, we ask normalized questions several times to ChatGPT3.5, then look at the correctness of answers, and finally check if this creates issues. The main result is that the performances of ChatGPT3.5 degrades drastically as the specialization of the domain increases: for basic algorithms it returns answers that are almost always correct, for design patterns the generated code contains many code smells and is generally of low quality, but it is still sometimes able to fix it (if asked), and for quantum computing it is often blatantly wrong.

Quantum computing is a growing field with significant potential applications. Learning how to code quantum programs means understanding how qubits work and learning to use quantum gates. This is analogous to creating classical algorithms using logic gates and bits. Even after learning all concepts, it is difficult to create new algorithms, which hinders the acceptance of quantum programming by most developers. This article outlines the need for higher-level abstractions and proposes some of them in a developer-friendly programming language called Rhyme. The new quantum types are extensions of classical types, including bits, integers, floats, characters, arrays, and strings. We show how to use such types with code snippets.

It has become common for curricula to contain a Capstone project component. Usually, the idea behind a capstone project course is to form groups of 4 to 6 students to work on a longer and larger project. This allows them to experience working for some months on ideas coming either from industry or from a professor. The intent is to make this experience more "real" than a traditional small project. This article presents a new type of capstone projects, which we call "Tribal Capstone Project Course". It takes a cohort of students over 3 semesters and makes them work in larger groups of 15–25 students called "tribes". The course has run for two cohorts of masters students within the Constructor context and has started for a third cohort. We believe that this setup is more representative of a real-world product-building context.

ChatGPT3 is a chat engine that fulfils the promises of an AI-based chat engine: users can ask a question (prompt) and it answers in a reasonable manner. The coding-related skills of ChatGPT are especially impressive: informal testing shows that it is difficult to find simple questions that ChatGPT3 does not know how to answer properly. Some students are certainly already using it to answer programming assignments. This article studies whether it is safe for students to use ChatGPT3 to answer coding assignments ("safe" means that they will not be caught for plagiarism if they use it). The main result is that it is generally not safe for students to use ChatGPT3. We evaluated the safety of code generated with ChatGPT3, by performing a search with a Codequiry, a plagiarism detection tool, and searching plagiarized code in Google (only considering the first page of results). In 38% of the cases, Codequiry finds a piece of code that is partially copied by the answer of ChatGPT3. In 96% of the cases, the Google search finds a piece of code very similar to the generated code. Overall, it is not safe for students to use ChatGPT3 in 96% of the cases.

The regression test suite, a key resource for managing program evolution, needs to achieve 100% coverage, or very close, to be useful. Devising a test suite manually is unacceptably tedious, but existing automated methods are often inefficient. The method described in this article, “Seeding Contradiction”, inserts incorrect instructions into every basic block of the program, enabling an SMT-based Hoare-style prover to generate a counterexample for every branch of the program and, from the collection of all such counterexamples, a test suite. The method is static, works fast, and achieves excellent coverage.

In software verification, a successful automated program proof is the ultimate triumph. The road to such success is, however, paved with many failed proof attempts. The message produced by the prover when a proof fails is often obscure, making it very hard to know how to proceed further. The work reported here attempts to help in such cases by providing immediately understandable counterexamples. To this end, it introduces an approach called Counterexample Extraction and Minimization (CEAM). When a proof fails, CEAM turns the counterexample model generated by the prover into a a clearly understandable version; it can in addition simplify the counterex-amples further by minimizing the integer values they contain. We have implemented the CEAM approach as an extension to the AutoProof verifier and demonstrate its application to a collection of examples.

Bluetooth Low Energy (BLE), a low-power wireless protocol, is widely used in industrial automation for monitoring field devices. Although the BLE standard defines advanced security mechanisms, there are known security attacks for BLE and BLE-enabled field devices must be tested thoroughly against these attacks. This article identifies the possible attacks for BLE-enabled field devices relevant for industrial automation. It also presents a framework for defining and executing BLE security attacks and evaluates it on three BLE devices. All tested devices are vulnerable and this confirms that there is a need for better security testing tools as well as for additional defense mechanisms for BLE devices.

The main challenge of architecting modern industrial control and automation systems (ICASs) is that they need to fulfill quality attributes (QAs) traditional to real-time systems - such as timeliness and predictability - and modern software engineering - such as modularity or reusability. QAs often are conflicting, which entails difficult trade-offs. As a consequence, even the architecture of closely related ICAS products can differ substantially due to their different priorities on QAs. This article presents six essential, but partially conflicting quality attributes for ICAS and shows how the shift in priority of these QAs impacts the architecture of three functionally very similar ICAS platforms.

Embedded devices are often tightly constrained by CPU power and memory size. As a consequence, developers of embedded software avoid any kind of design abstractions, thinking that they imply large overhead. This results in complex designs with high coupling between the individual entities. The code of such designs is then difficult to maintain or reuse. This article presents FASAlight, a component-based software architecture for embedded devices with a focus on three main quality attributes that support maintenance and reuse: modularity, reusability, and portability. This architecture can be effectively implemented even for low-end embedded devices and only implies at worst a 14% on CPU and small overhead on memory on a device with a 120MHz ARM CPU and 128 kB of RAM.

To increase their dependability, distributed control systems (DCSs) need to agree in real time about which hosts have crashed, i.e., they need a real-time membership service. In this paper, we prove that such a service cannot be implemented deterministically if, besides host crashes, communication can also fail. We define implementable probabilistic variants of membership properties, which constitute what we call a synchronous membership service (SYMS). We present an algorithm, ViewSnoop, that implements SYMS with high-probability. We implement, deploy and evaluate ViewSnoop analytically as well as experimentally, within an industrial DCS framework. We show that ViewSnoop significantly improves the dependability of DCSs compared to membership schemes based on classic heartbeats, at low additional cost. Moreover, ViewSnoop distinguishes, with high probability, host crashes from message losses, enabling DCSs to counteract losses better than existing approaches.

Research on software engineering typically focuses on mainstream languages such as Java, .NET, and C. It is validated using projects easily executable and deployable on a desktop machine. Real, embedded, legacy code is however seldom made of such clean code. This article presents such a case. We performed the analysis and testing of legacy code, which is mix of C and DSP assembly. Such combinations of technologies cannot be analyzed by regular software engineering tools, creating a de facto software engineering desert island. Our solution relies on writing a parser for the DSP code, static analyzers, and using integration test cases. To run the tests, we also automate deployment on the target hardware and run the tests from an integration server.

Developing correct, efficient, and maintainable real-time control software for cyber-physical systems is a notoriously difficult interdisciplinary challenge. Ever more complex control algorithms and the advent of multi-core hardware in embedded systems have made this challenge even harder. Component-based software development promises to help reduce the complexity and to increase the timing predictability for time-critical software.This paper presents FASA, a component-based approach for scalable real-time systems. This approach offers a platform-independent development method with a high degree of predictability, supports multi-core systems by design, and simplifies maintenance. Two case studies validate FASA: an application handling a magnetic levitation device and an example of scalability.