https://www.mdu.se/

Cyber-physical systems (CPSs) are complex systems that integrate physical, computational, and communication subsystems. The heterogeneous nature of these systems makes their safety assurance challenging. In this paper, we propose a novel automated approach for guardrailing cyber-physical systems using property-based tests (PBTs) generated by Large Language Models (LLMs). Our approach employs an LLM to extract properties from the code and documentation of CPSs. Next, we use the LLM to generate PBTs that verify the extracted properties on the CPS. The generated PBTs have two uses. First, they are used to test the CPS before it is deployed, i.e., at design time. Secondly, these PBTs can be used after deployment, i.e., at run time, to monitor the behavior of the system and guardrail it against unsafe states. We implement our approach in ChekProp and conduct preliminary experiments to evaluate the generated PBTs in terms of their relevance (how well they match manually crafted properties), executability (how many run with minimal manual modification), and effectiveness (coverage of the input space partitions). The results of our experiments and evaluation demonstrate a promising path forward for creating guardrails for CPSs using LLM-generated property-based tests.

Designing noise-robust parameterized quantum circuits (PQCs) is a central challenge in the noisy intermediate-scale quantum (NISQ) regime. Existing quantum architecture search methods rely on training large SuperCircuits and evaluating SubCircuits under noisy execution, resulting in high computational cost and architecture assessments that depend on task-specific optimization and device noise. In this work, we propose a training-free quantum architecture search framework based on information-theoretic expressibility measures rather than performance-based estimators. We empirically show that noise-free KL-divergence-based expressibility exhibits a consistent monotonic association with noisy task loss across diverse circuit architectures and realistic hardware noise models. Leveraging this relationship, we introduce an expressibility-guided evolutionary search that requires neither SuperCircuit training nor noisy execution during the search phase. Since expressibility is evaluated independently of hardware noise, the method is inherently device-agnostic, enabling architectures to be reused across multiple quantum devices without re-running the search. Experiments using IBM-derived Qiskit noise models demonstrate that the proposed approach achieves competitive performance compared to SuperCircuit-based baselines, while substantially reducing computational cost. These results establish expressibility as an effective information-theoretic surrogate for ranking PQC architectures under realistic noise.

Timing is a central concern in critical embedded systems. Such systems must interact with a physical environment in a timely fashion. The critical point here is not average performance but guaranteed performance which must be good enough for the given environment. In this introduction to the Festschrift dedicated to Wang Yi on the occasion of his 60th birthday, we give an overview on the contributions of Wang Yi to the analysis and the construction of real-time systems and to the related contributions to this volume.

This Festschrift reflects Professor Wang Yi's contributions to the fields of formal methods, real-time systems and scheduling, and multicore systems.

Wang Yi received a PhD in Computer Science from Chalmers University of Technology in 1991, since 2000 he has been Chair in Embedded Systems at Uppsala University. He has not only pushed the boundaries of theoretical research but also pioneered practical implementations in software tools that have had a profound impact on both academia and industry. He codeveloped the UPPAAL tool, the foremost system for verifying timed automata, now widely used in both academia and industry. Over the years he expanded his research to include scheduling theories, and he developed the TIMES and TIMES-Pro tools, which enhanced the analysis and implementation of real-time systems. His innovative work has significantly influenced the design and verification of complex, multicore real-time systems. Among many awards, honours, and responsibilities, Wang received a grant from the Knut and Alice Wallenberg Foundation, an ERC Advanced Grant from the European Research Council in 2019, Uppsala University’s Rudbeck Medal, the IEEE TCRTS Award for technical achievement and leadership in real-time computing, and the CAV Award; he is a Fellow of the ACM and the IEEE, and a member of the Royal Society of Sciences in Uppsala and the Academia Europaea; and he has chaired major software engineering and embedded system conferences and served on ACM SIGBED and IEEE TCRTS executive committees. 

His guidance and mentorship have shaped the careers of many researchers and professionals in the field, and the contributions in this volume celebrate his enduring impact.

The term ‘Sifu’ in Chinese denotes a ‘teacher’ or ‘master’ and is used to describe an individual who has attained significant expertise and mastery in a specific field, often within martial arts. In this paper, we describe the bond between us and our sifu in computer science, Professor Wang Yi. 

The type 1 diabetes community is coalescing around the benefits and advantages of early screening for disease risk. To be accepted by healthcare providers, regulatory authorities and payers, screening programmes need to show that the testing variables allow accurate risk prediction and that individualised risk-informed monitoring plans are established, as well as operational feasibility, cost-effectiveness and acceptance at population level. Artificial intelligence (AI) has the potential to contribute to solving these issues, starting with the identification and stratification of at-risk individuals. ASSET (AI for Sustainable Prevention of Autoimmunity in the Society; www.asset.healthcare) is a public/private consortium that was established to contribute to research around screening for type 1 diabetes and particularly to how AI can drive the implementation of a precision medicine approach to disease prevention. ASSET will additionally focus on issues pertaining to operational implementation of screening. The authors of this article, researchers and clinicians active in the field of type 1 diabetes, met in an open forum to independently debate key issues around screening for type 1 diabetes and to advise ASSET. The potential use of AI in the analysis of longitudinal data from observational cohort studies to inform the design of improved, more individualised screening programmes was also discussed. A key issue was whether AI would allow the research community and industry to capitalise on large publicly available data repositories to design screening programmes that allow the early detection of individuals at high risk and enable clinical evaluation of preventive therapies. Overall, AI has the potential to revolutionise type 1 diabetes screening, in particular to help identify individuals who are at increased risk of disease and aid in the design of appropriate follow-up plans. We hope that this initiative will stimulate further research on this very timely topic.

Have you thought of how it feels to be an AI brain in the world of humans? This book allows such a brain to tell us how it takes on its mission of helping humans to develop a more efficient, sustainable, diverse and inclusive society.

This book explains the principles and applications of artificial intelligence for a broad audience. Artificial intelligence, as part of computer science, is often inspired by human intelligence. At the same time, there is still reluctance in the applications and usability of artificial intelligence among citizens. Industries are deploying AI in their products and processes but the level of maturity is varying. The book is written as a first person narrative, from an AI perspective, having the AI brain tell the story. 

Automated test generation has been suggested as a way of creating tests at a lower cost. Nonetheless, it is not very well studied how such tests compare to manually written ones in terms of cost and effectiveness. This is particularly true for industrial control software, where strict requirements on both specification-based testing and code coverage typically are met with rigorous manual testing. To address this issue, we conducted a case study in which we compared manually and automatically created tests. We used recently developed real-world industrial programs written in the IEC 61131-3, a popular programming language for developing industrial control systems using programmable logic controllers. The results show that automatically generated tests achieve similar code coverage as manually created tests, but in a fraction of the time (an average improvement of roughly 90%). We also found that the use of an automated test generation tool does not result in better fault detection in terms of mutation score compared to manual testing. Specifically, manual tests more effectively detect logical, timer and negation type of faults, compared to automatically generated tests. The results underscore the need to further study how manual testing is performed in industrial practice and the extent to which automated test generation can be used in the development of reliable systems.

Architectural engineering of embedded systems comprehensively affects both the development processes and the abilities of the systems. Verification of architectural engineering is consequently essential in the development of safety- and mission-critical embedded system to avoid costly and hazardous faults. In this paper, we present the Architecture Quality Assurance Tool (AQAT), an application program developed to provide a holistic, formal, and automatic verification process for architectural engineering of critical embedded systems. AQAT includes architectural model checking, model-based testing, and selective regression verification features to effectively and efficiently detect design faults, implementation faults, and faults created by maintenance modifications. Furthermore, the tool includes a feature that analyzes architectural dependencies, which in addition to providing essential information for impact analyzes of architectural design changes may be used for hazard analysis, such as the identification of potential error propagations, common cause failures, and single point failures. Overviews of both the graphical user interface and the back-end processes of AQAT are presented with a sensor-to-actuator system example.