Modern autonomous systems are composed of interacting components for control, scheduling, and learning, each operating under practical limitations such as timing uncertainty and imperfect perception. Traditional design and verification approaches aim for component-level perfection, an assumption that is increasingly untenable for complex systems. This paper advocates a shift toward quantitative, system-level safety that explicitly accounts for imperfect components and characterizes how their combined effects impact closed-loop behavior. We introduce safety metrics based on trajectory deviation and reachable set expansion, develop methods to check and synthesize safe schedules under deadline misses, and extend the framework to learning-enabled systems via edge–cloud control and safety-driven resource allocation. Together, these results demonstrate how safe autonomous systems can be systematically designed without requiring their individual components to be perfect.

Smart contracts have achieved significant success, however, their security remains a long-standing challenge. The immutability and transparency of smart contracts require establishing a strong mechanism to prevent private leakage and trusted data tampering. Apart from traditional logic and code-level vulnerabilities arising from insufficient control over contract variables and function parameters, smart contracts may store private-dependent information in blockchain records, which is a critical type of vulnerability, but often overlooked in existing security analysis. In this paper, we present an automated approach for synthesizing security policies, named SmartIFSyn, to eliminate information flow vulnerabilities in smart contracts. We formalize the semantics of Solidity, the most widely used smart contract language, and analyze information flow security of Solidity smart contracts from two perspectives: local-variable security and global-interaction security. We present a type system to guide the elimination of local-variable vulnerabilities by inferring a policy and resort to constraint solving to synthesize a desired policy in case that the type system fails. The policy ensures both local-variable and global-interaction security while it is maximally aligned with user preference. Furthermore, the policy can be subsequently converted into enforceable specifications. We implement our approach in a tool and evaluate it on 17,160 real-world Ethereum smart contracts. The experimental results demonstrate the efficacy of our approach, e.g., detected 243 vulnerabilities in 223 real-world Ethereum smart contracts.

Verifying the safety of latency-aware cyber-physical systems is both critical and challenging due to the interaction between continuous physical dynamics and discrete computational constraints. This paper introduces SOTERIA, a formal framework that integrates digital twins for ensuring safety in these systems. SOTERIA models both the physical dynamics and computational behavior, enabling integrated verification within a specific operating environment. This approach goes beyond conventional methods that either treat physical and computational aspects separately or rely on overly conservative worst-case analyses. By modeling hybrid dynamics alongside computational models and operating environments, SOTERIA verifies both functional and timing correctness. Leveraging established verification tools, SOTERIA determines whether end-to-end latencies meet formal specifications, bridging the gap between computational and physical requirements. We first introduce a simple example of a 1D adaptive cruise control system to illustrate its effectiveness. We then present findings from a case study using the F1Tenth racing car platform and the UPPAAL tool to demonstrate SOTERIA's effectiveness in realistic scenarios, enabling safety verification that was previously infeasible with conventional schedulability analyses. This work underscores the importance of an integrated verification approach for enhancing safety and reliability in autonomous systems.

Earth System Models (ESMs) are critical for understanding past climates and projecting future scenarios. However, the complexity of these models, which include large code bases, a wide community of developers, and diverse computational platforms, poses significant challenges for software quality assurance. The increasing adoption of GPUs and heterogeneous architectures further complicates verification efforts. Traditional verification methods often rely on bitwise reproducibility, which is not always feasible, particularly under new compilers or hardware. Manual expert evaluation, on the other hand, is subjective and time-consuming. Formal methods offer a mathematically rigorous alternative, yet their application in ESM development has been limited due to the lack of climate model-specific representations and tools. Here, we advocate for the broader adoption of formal methods in climate modeling. In particular, we identify key aspects of ESMs that are well suited to formal specification and introduce abstraction approaches for a tailored framework. To demonstrate this approach, we present a case study using CIVL model checker to formally verify a bug fix in an ocean mixing parameterization scheme. Our goal is to develop accessible, domain-specific formal tools that enhance model confidence and support more efficient and reliable ESM development.

Autonomous systems are increasingly used in safety-critical domains, including industrial automation, autonomous vehicles, and the industrial Internet of Things. Verifying both the functional and temporal correctness of these systems is essential to ensure safety before deployment. However, end-to-end verification is challenging due to the interaction of continuous-time physical processes with discrete-time computational systems. Existing formal methods often assume simplified or static computational models, while traditional real-time systems focus on meeting timing constraints without explicitly linking them to physical safety. We address this gap by proposing a physics-informed mixed-criticality (MC) verification framework for cyber-physical systems, which allows the integration of computational and physical models for dynamic, fine-grained safety assurance. Our framework incorporates feedback from the local environment to guide criticality-based mode switching, ensuring adaptive responses to real-time physical states rather than relying on global worst-case assumptions. We demonstrate the feasibility of our approach with a prototype implementation on an autonomous F1 Tenth vehicle using preemptive EDF scheduling on ROS 2. Verification is conducted using UPPAAL to validate system behavior, mode transitions, and physical safety constraints. Results show that our framework effectively manages MC requirements, enhancing responsiveness and safety in dynamic environments.

Autonomous systems are heavily used in many safety-critical systems, such as industrial automation, autonomous cars, Industrial Internet of Things (I-IoT), etc. Verification of the functional and temporal correctness of such systems is necessary before deployment to ensure their safety. However, due to the presence of physical systems in the continuous-time domain and computational models in the discrete-time domain, end-to-end verification of these systems is highly challenging. Existing formal methods focus on verifying physical models assuming static or simplified computation models. In contrast, existing real-time systems focus on satisfying strict timing bounds but do not care how those bounds are obtained and how they relate to physical safety. Our approach bridges these two domains, and constitutes an end-to-end verification framework for arbitrary physical models and computational models incorporated within a cyber-physical automated system. By allowing the interaction between the computational and physical models, our verification framework enables a fine-grained scheme that verifies against the local environment instead of verifying against global worst-case assumptions. Moreover, to support locally varying worst-case scenarios, a mixed-criticality system is proposed where the system supports several critical models and switches among the modes based on environmental uncertainty. Finally, a proof-of-concept evaluation of the proposed framework is reported.

Bond graphs represent the structure and functionality of mechatronic systems from a power flow perspective. Unfortunately, presentations of bond graphs are replete with ambiguity, significantly impeding understanding. We extend the formalisation in preceding work to address the phenomenon of ‘causality’, intended to help formulate solution strategies for bond graphs, but usually presented in such vague terms that the claims made are easily shown to be false. We show that ‘causality’ only works as advertised in the simplest cases, where it mimics the mathematical definition of bond graph semantics. Counterexamples severely limit the applicability of the notion.

Bond graphs represent the structure and functionality of mechatronic systems from a power flow perspective. Unfortunately, presentations of bond graphs are replete with ambiguity, significantly impeding understanding. A formalisation of the essentials of bond graphs is given, together with a formalisation of bond graph transformation, which can directly express abstraction and refinement of bond graphs.

HPC practitioners make use of techniques, such as parallelism and sparse data structures, that are difficult to reason about and debug. Here we explore the role of data refinement, a correct-by-construction approach, in verifying HPC applications via bounded model checking. We show how single program, multiple data (SPMD) parallelism can be modeled in Alloy, a declarative specification language, and describe common issues that arise when performing scope-complete refinement checks in this context.

AUTOSAR (AUTomotive Open System ARchitecture) is a development partnership whose primary goal is the standardization of basic system functions and functional interfaces for electronic control units in automobiles. As an open specification, its layered software architecture promotes the interoperability of real-time embedded vehicle systems and components. It also opens up the possibility of formal modelling and verification approaches, centred around the specification, that can be used to support analysis in the early stages of design. In this paper, we describe a methodology and associated tool, called A2A, that automatically models systems defined by the AUTOSAR specifications as timed au-tomata, and then verifies their timing properties using UPPAAL. It contains 22 groups of timed automata templates, together with two auxiliary test templates, that model the AUTOSAR architecture and timing properties, allowing time-related behaviours to be extracted from the three-layer architecture, i.e., the AUTOSAR Software, AUTOSAR Runtime Environment, and Basic Software layers, and templates to be automatically instantiated. The timing properties are specified using timed computation tree logic (TCTL) in UPPAAL to verify the system model. We demonstrate the capabilities of the methodology by applying it to an AUTOSAR architecture that describes an internal vehicle light control system, thereby showing its effectiveness. (c) 2023 Elsevier Inc. All rights reserved.

We introduce Sterling, a web-based visualization tool that provides interactive views of relational models and allows users to create custom visualizations using modern JavaScript libraries like D3 and Cytoscape. We outline its design goals and architecture, and describe custom visualizations developed with Sterling that enable verification studies of scientific software used in production. While development is driven primarily by the Alloy community, other relational modeling languages are accommodated by Sterling's data agnostic architecture.

The document is the Final Technical Report for the Nuclear Energy University Program’s Integrated Research Project (IRP) on “Development and Application of a Data-Driven Methodology for Validation of Risk-Informed Safety Margin Characterization (RISMC) Models”. The project goal is to develop and demonstrate a data-driven methodology for validation of advanced computer models used in nuclear power plant safety analysis. Specifically, the advanced computer models are those in the toolkit developed to support risk-informed safety margin characterization (RISMC), an integrated deterministic/probabilistic safety analysis methodology developed in the Department of Energy’s Light Water Reactor Sustainability (LWR-S) program.

Traditionally, external hazards are considered in the design of a building through the various combinations of loads prescribed in relevant design codes and standards. It is often the case that the design is governed by a single dominant hazard at a given geographic location. This is particularly true for earthquake and wind hazards, both of which impart time-dependent dynamic loads on the structure. Engineers may nevertheless wonder if a building designed for one of the two dominant hazards will satisfactorily withstand the other. Prior studies have indicated that in some cases, when a building is designed for a single dominant hazard, it does not necessarily provide satisfactory performance against the other hazard. In this paper, we propose a novel framework that builds upon performance-based design requirements and determines whether the design of a building is governed primarily by a single hazard or multiple hazards. It integrates site-dependent hazard characteristics with the performance criteria for a given building type and building geometry. The framework is consistent with the burgeoning area of probabilistic risk assessment, and yet can easily be extended to traditional, deterministically characterized design requirements as illustrated herein.

NOTE: The first page of text has been automatically extracted and included below in lieu of an abstract I .— - Session 3215 , ...... —.. - A Controlled Comparison of Traditional Classroom Instruction with Computer Based Instruction in an Engineering Class Joseph E. Hummer, John W. Baugh, Jr., Bhavani P. Konuru, and Steven M. Click North Carolina State University ABSTRACT Educators have long considered using computer-based instruction (CBI) because it promises both self- paced, interactive education for students and greater efficiency for instructors. In the past, the resources necessary for CBI were in short supply, but now that many universities maintain powerful computing environments, questions about the effectiveness and efficiency of CBI arise. To investigate the effectiveness of CBI, the project team developed three CBI units--one each for design, analysis, and background information--for use in a junior-level transportation engineering class. The team then conducted controlled experiments with the units. The team divided the participating class randomly in half. An exam covering material other than that in the CBI units was used to ensure that neither group had superior students. One group received traditional classroom instruction while the other used the CBI unit. The team administered surveys to both groups before and after the use of the CBI units to determine student opinions. The same homework problem was given to both groups immediately after instruction. Finally, all students were tested over the material during an in-class exam. The team determined effectiveness of the CBI units via statistical analysis of homework scores, test scores, and survey responses from the two groups. Based on the analysis of group scores, CBI was as effective as traditional classroom instruction. In addition, student attitudes toward the class and toward the engineering profession in general were not affected by the use of CBI. The results indicate that CBI has potential; however, questions on the efficiency of CBI remain. INTRODUCTION Educators have long considered using computer-based instruction (CBI) because it promises interactive, self-paced, highly visual, easily measured learning. In the past, a lack of available computing power made CBI infeasible at many universities. However, now that powerfid computing platforms are routinely available, new questions arise: Do students using CBI learn as well as students receiving traditional classroom instruction? Which courses and types of problems are best suited to CBI? Are the hopes of educators justified? A number of authors have published results on the effectiveness of CB11>2>3. However, most of these experiments were performed in the humanities, and little research has been done on the effectiveness of CBI in engineering. In an attempt to determine CBI’S effectiveness in engineering, three CBI units--one each for design (open-ended problems with no single “right answer”), analysis (closed-type problems with a single “right answer”), and review of background information--were developed for use in a junior-level transportation engineering class4. Experiments then compared the effectiveness of two of these units with traditional classroom ‘ . . ..- - $iii’1996 ASEE Annual Conference Proceedings } ‘..,~yy’,?

In earthquake-prone zones of the world, severe damage to buildings and life endangering harm to people pose a major risk when severe earthquakes happen. In recent decades, active and passive measures to prevent building damage have been designed and deployed. A simple model of an active damage prevention system, founded on earlier work, is investigated from a model based formal development perspective, using Hybrid Event-B. The non-trivial physical behaviour in the model is readily captured within the formalism. However, when the usual approximation and discretization techniques from engineering and applied mathematics are used, the rather brittle refinement techniques used in model based formal development start to break down. Despite this, the model developed stands up well when compared via simulation with a standard approach. The requirements of a richer formal development framework, better able to cope with applications exhibiting non-trivial physical elements are discussed.

We show how to model and reason about the structure and behavior of sparse matrices, which are central to many applications in scientific computation. Our approach is state-based, relying on a formalism called Alloy to show that one model is a refinement of another. We present examples of sparse matrix-vector multiplication, transpose, and translation between formats using ELLPACK and compressed sparse row formats to demonstrate the approach. To model matrix computations in a declarative language like Alloy, a new idiom is presented for bounded iteration with incremental updates. Mechanical verification is performed using SAT solvers built into the tool.

Large-scale numerical software requires substantial computer resources that complicate testing and debugging. A single run of a climate model may require many millions of core-hours and terabytes of disk space, making trial-and-error experiments burdensome and time consuming. In this study, we apply hybrid theorem proving from the field of cyber-physical systems to problems in scientific computation, and show how to verify the correctness of discrete updates that appear in the simulation of continuous physical systems. By viewing numerical software as a hybrid system that combines discrete and continuous behavior, test coverage and confidence in findings can be increased. We describe abstraction approaches for modeling numerical software and demonstrate the applicability of the approach in a case study that reproduces undesirable behavior encountered in a parameterization scheme, called the K-profile parameterization, widely used in ocean components of large-scale climate models. We then identify and model a fix in the configuration of the scheme, and verify that the undesired behavior is eliminated for all possible execution sequences. We conclude that hybrid theorem proving is an effective and efficient approach that can be used to verify and reason about properties of large-scale numerical software.

A 2-D unstructured finite element model is used to study how local and remote atmospheric forcing, sea level rise, and shoreline variation affect typhoon-induced storm surge in a small shallow bay, Zhanjiang Harbor (ZH). In this research, the spatial distribution of storm surge is divided into three patterns in ZH, denoted E-W, N-S, and S-N, using a quantitative method. In the Bay, local atmospheric effects (LAE) and remote atmospheric effects (RAE) both play important roles in the maximum residual water level. The contribution of RAE to the inflow is higher than that of the LAE, but the former is less important in the spatial distribution in ZH. In addition, the typhoon track influences the time of occurrence of the maximum surge by forcing the outer waters to ZH, then the spatial distribution of the surge residual in the bay is controlled by local winds, and different regions are threatened during different kinds of storm surge processes. Two sea level rise scenarios are set up in the paper as well, and the results show that the trends of the changes in LAE and RAE in the inner-bay are the opposite in the case of sea level rise; however, the total changes of the distribution are not the same in different categories. In general, the E-W category storm surge is weakened, while the N-S and S-N category storm surges have inverse changes in the north and south of ZH. There is a downward trend of the maximum surge gradient within the Bay, but relative to sea level rise itself this effect is not obvious. The establishment of the sea embankment increased the storm surge within the bay though it is not significant.

Control systems, protocols, and hardware design are among the most common applications of state-based formal methods, and yet the types of modeling and analysis they enable are also well-suited to problems in scientific computation, where quality, reproducibility, and productivity are growing concerns. We survey the challenges faced by developers of scientific software, characterize the nature of the programs they write, and offer some perspective on the role that state-based methods can play in scientific domains.