Declarative specification languages like Alloy are critical for modeling and verifying complex software systems, yet repairing these specifications remains a significant challenge for ensuring software dependability. This study conducts the first comprehensive empirical evaluation comparing traditional systematic repair techniques with emerging Large Language Model (LLM)-based approaches across two established benchmarks, analyzing over 1,900 Alloy specifications. By systematically analyzing repair success rates, ground truth similarity, and repair generation strategies, we reveal nuanced performance characteristics of different repair methodologies. Our findings demonstrate that while traditional tools excel in systematic fault localization and achieving high ground truth similarity, LLM-based techniques—particularly multi-round prompting approaches—offer unique capabilities in addressing complex specification errors, with some hybrid approaches achieving repair rates of up to 85.5%. Critically, we show that integrating traditional fault localization techniques with LLM-based repair strategies can significantly enhance overall repair effectiveness and specification dependability. This research provides a large-scale empirical evaluation of how various Alloy repair techniques work in synergy, offering valuable insights that chart a promising path for future automated specification repair approaches and contribute to the development of more reliable and secure software systems.

Bounded formal analysis techniques (such as bounded model checking) are incredibly powerful tools for today's software engineers. However, such techniques often suffer from scalability challenges when applied to large-scale, real-world systems. It can be very difficult to ensure the bounds are set properly, which can have a profound impact on the performance and scalability of any bounded formal analysis. In this paper, we propose a novel approach---relational bound propagation---which leverages the semantics of the underlying relational logic formula encoded by the specification to automatically tighten the bounds for any relational specification. Our approach applies two sets of semantic rules to propagate the bounds on the relations via the abstract syntax tree of the formula, first upward to higher-level expressions on those relations then downward from those higher-level expressions to the relations. Thus, relational bound propagation can reduce the number of variables examined by the analysis and decrease the cost of performing the analysis. This paper presents formal definitions of these rules, all of which have been rigorously proven. We realize our approach in an accompanying tool, Propter, and present experimental results using Propter that test the efficacy of relational bound propagation to decrease the cost of relational bounded model checking. Our results demonstrate that relational bound propagation reduces the number of primary variables in 63.58% of tested specifications by an average of 30.68% (N=519) and decreases the analysis time for the subject specifications by an average of 49.30%. For large-scale, real-world specifications, Propter was able to reduce total analysis time by an average of 68.14% (N=25) while introducing comparatively little overhead (6.14% baseline analysis time).

Due to the growing presence of Internet of Things (IoT) apps and devices in smart homes and smart cities, there are more and more concerns about their security and privacy risks. IoT apps normally interact with each other and the physical world to offer utility to the users. In this paper, we investigate the safety and security risks brought by the interactive behaviors of IoT apps. Two major challenges ensue in identifying the interaction threats: i) how to discover the threats across both cyber and physical channels; and ii) how to ensure the scalability of the detection approach. To address these challenges, we first provide a taxonomy of interaction threats between IoT apps, which contains seven classes of coordination threats categorized based on their interaction behaviors. Then, we presentIoTCom, a compositional threat detection system capable of automatically detecting and verifying unsafe interactions between IoT apps and devices.IoTComapplies static analysis to automatically infer relevant apps’ behaviors, and uses a novel strategy to trim the extracted app's behaviors prior to translating them into analyzable formal specifications, mitigating the state explosion associated with formal analysis. Our experiments with numerous bundles of real-world IoT apps have corroboratedIoTCom's ability to effectively identify a broad spectrum of interaction threats triggered through cyber and physical channels, many of which were previously unknown. Finally,IoTComuses an automatic verifier to validate the discovered threats. Our experimental results show thatIoTComsignificantly outperforms the existing techniques in terms of the computational time, and maintains the capability to perform its analysis across different IoT platforms.

With the ever-increasing popularity of mobile devices over the last decade, mobile applications and the frameworks upon which they are built frequently change, leading to a confusing jumble of devices and applications utilizing differing features even within the same framework. For Android apps and devices—the largest such framework and marketplace— mismatches between the version of the app API installed on a device and the version targeted by the developers of an app running on that device can lead to run-time crashes, providing a poor user experience. This paper presents SAINTDroid, a holistic compatibility analysis approach that seamlessly examines both the application code and the framework code by gradually loading and analyzing classes as needed during the compatibility analysis to enable efficient and scalable identification of various types of crash-leading Android compatibility issues. We applied SAINTDroid to 3,590 real-world apps and compared the analysis results against the state-of-the-art techniques, which corroborates that SAINTDroid is up to 76% more successful in detecting compatibility issues while issuing significantly fewer false alarms. The experimental results also show that SAINTDroid is remarkably (up to 8.3 times and four times on average) faster than the state-of-the-art techniques.

Software engineers have long employed formal verification to ensure the safety and validity of their system designs. As the system changes---often via predictable, domain-specific operations---their models must also change, requiring system designers to repeatedly execute the same formal verification on similar system models. State-of-the-art formal verification techniques can be expensive at scale, the cost of which is multiplied by repeated analysis. This paper presents a novel analysis technique---implemented in a tool called SoRBoT---which can automatically determine domain-specific optimizations that can dramatically reduce the cost of repeatedly analyzing evolving systems. Different from all prior approaches, which focus on either tightening the bounds for analysis or reusing all or part of prior solutions, SoRBoT's automated derivation of domain-specific optimizations combines the benefits of both solution reuse and bound tightening while avoiding the main pitfalls of each. We experimentally evaluate SoRBoT against state-of-the-art techniques for verifying evolving specifications, demonstrating that SoRBoT substantially exceeds the run-time performance of those state-of-the-art techniques while introducing only a negligible overhead, in contrast to the expensive additional computations required by the state-of-the-art verification techniques.

Formal analysis is an invaluable tool for software engineers, yet state-of-the-art formal analysis techniques suffer from well-known limitations in terms of scalability. In particular, some software design domains—such as tradeoff analysis and security analysis—require systematic exploration of potentially huge model spaces, which further exacerbates the problem. Despite this present and urgent challenge, few techniques exist to support the systematic exploration of large model spaces. This paper introduces Parasol, an approach and accompanying tool suite, to improve the scalability of large-scale formal model space exploration. Parasol presents a novel parallel model space synthesis approach, backed with unsupervised learning to automatically derive domain knowledge, guiding a balanced partitioning of the model space. This allows Parasol to synthesize the models in each partition in parallel, significantly reducing synthesis time and making large-scale systematic model space exploration for real-world systems more tractable. Our empirical results corroborate that Parasol substantially reduces (by 460% on average) the time required for model space synthesis, compared to state-of-the-art model space synthesis techniques relying on both incremental and parallel constraint solving technologies as well as competing, non-learning-based partitioning methods.

Public projects can succeed or fail for many reasons such as the feasibility of the original goal and coordination among contributors. One major reason for failure is that insufficient work leaves the project partially completed. For certain types of projects anything short of full completion is a failure (e.g., feature request on software projects in GitHub). Therefore, project success relies heavily on individuals allocating sufficient effort. When there are multiple public projects, each contributor needs to make decisions to best allocate his/her limited effort (e.g., time) to projects while considering the effort allocation decisions of other strategic contributors and his/her parameterized utilities based on values and costs for the projects. In this paper, we introduce a game-theoretic effort allocation model of contributors to public projects for modeling effort allocation of strategic contributors. We study the related Nash equilibrium (NE) computational problems and provide NP-hardness results for the existence of NE and polynomial-time algorithms for finding NE in restricted settings. Finally, we investigate the inefficiency of NE measured by the price of anarchy and price of stability.

Self-adaptive systems often employ dynamic programming or similar techniques to select optimal adaptations at run-time. These techniques suffer from the "curse of dimensionality", increasing the cost of run-time adaptation decisions. We propose a novel approach that improves upon the state-of-the-art proactive self-adaptation techniques to reduce the number of possible adaptations that need be considered for each run-time adaptation decision. The approach, realized in a tool called Thallium, employs a combination of automated formal modeling techniques to (i) analyze a structural model of the system showing which configurations are reachable from other configurations and (ii) compute the utility that can be generated by the optimal adaptation over a bounded horizon in both the best- and worst-case scenarios. It then constructs triangular possibility values using those optimized bounds to automatically compare adjacent adaptations for each configuration, keeping only the alternatives with the best range of potential results. The experimental results corroborate Thallium's ability to significantly reduce the number of states that need to be considered with each adaptation decision, freeing up vital resources at run-time.

The ubiquity of Internet of Things (IoT) and our growing reliance on IoT apps are leaving us more vulnerable to safety and security threats than ever before. Many of these threats are manifested at the interaction level, where undesired or malicious coordinations between apps and physical devices can lead to intricate safety and security issues. This paper presents IoTCOM, an approach to automatically discover such hidden and unsafe interaction threats in a compositional and scalable fashion. It is backed with auto-mated program analysis and formally rigorous violation detection engines. IoTCOM relies on program analysis to automatically infer the relevant app’s behavior. Leveraging a novel strategy to trim the extracted app’s behavior prior to translating them to analyzable formal specifications,IoTCOM mitigates the state explosion associated with formal analysis. Our experiments with numerous bundles of real-world IoT apps have corroborated IoTCOM’s ability to effectively detect a broad spectrum of interaction threats triggered through cyber and physical channels, many of which were previously unknown, and to significantly outperform the existing techniques in terms of scalability.

While the polling or request/response paradigm adopted by many network and systems management approaches form the backbone of modern monitoring and management systems, the most important and interesting events, faults, alerts and log messages arrive at the management agent in a push-based asynchronous manner. However, in the management infrastructure itself, at the point where events are initially processed and matched to subscribers, there have been few attempts to identify relationships or dependencies between events. This means that most of this burden is placed on the management application, or indeed the managers themselves. This research investigates enhancing the expressiveness of a knowledge-based networking middleware with the addition of three temporal operators to be used in subscriptions to select matching events. A prototype design is presented and a number of implementations are compared. The approach is also motivated using two scenarios for temporal correlation of warnings and faults in managed networks. The effect on the scalability of the extended knowledge-based network system is also evaluated.

Mobile wireless sensor networks are gaining increasinguse in both military and civilian applications. Priorto deployment, it is often necessary to test the communication capabilities and power consumption of these networks. Typically network simulators, such as ns-2 and TOSSIM, are used to carry out these performance tests. However, the analysis of results is restricted to comparison with others obtained using the same simulator. Therefore, the creation of a tool which allows for the comparison of results obtained with different simulators would be of great interest to the research community.This work details an extension developed for the incorporation of mobility into TOSSIM 2.x. An analysis of the working mechanisms for mobility in ns-2 was also carriedout and a tool which converts ns-2 settings into ones suitable for use in TOSSIM implemented. This tool bridges the gap between ns-2 and TOSSIM for the simulation of dynamic network scenarios. Finally, an analysis of two test simulation scenarios which include mobility is presented; these show how mobility impacts on communication in both simulators and also indicates how results obtained with the two simulators can be readily compared.