Eunsuk Kang

In self-adaptive software systems, the role of context is paramount, especially for proactive self-adaptation. Current research, however, does not fully explore context's impact, for example on priorities of the requirements. To address this gap, we introduce a novel contextual goal model to capture these factors and their influence on the system. Using this, we propose a two-layer control mechanism with a context-aware model predictive control to achieve proactive adaptation for the software system and adaptation for the controller itself. By contextual prediction and a more accurate system model, our approach utilizes model predictive control to facilitate timely and efficient system adaptations, improving both performance and adaptability. Meanwhile, we perform requirement adaptation to update the contextual goal model, which in turn updates the objective function and constraints of the controller. Our experimental evaluations across two scenarios demonstrate the significant benefits of our approach in enhancing system performance.

Formal modeling tools rely on visualizations to help users explore models, identify errors, and build confidence in system correctness. However, visualizers often produce inconsistent layouts across instances, making it difficult to track structural similarities and changes. In this paper, we present the first human-subject study of visual consistency in formal modeling, examining how consistent layouts influence users’ ability to understand and debug models. Through a controlled experiment, participants completed tasks using either manually created consistent visualizations or visualizations created by the Alloy formal modeling tool. Our findings show that full (strict) visual consistency significantly improves both the speed and correctness of bug detection and localization. We also observe that partial consistency – where diagrams need not be fully identical but preserve enough recognizable structure for users to perceive similarities – offers a similar set of improvements to user performance, offering a practical alternative to full consistency. Subjective findings through post-experiment interviews reveal that consistency lowers cognitive overhead by helping participants more naturally and efficiently detect differences and track corresponding elements across states.

Large language model (LLM)-based AI agents extend LLM capabilities by enabling access to tools such as data sources, APIs, search engines, code sandboxes, and even other agents. While this empowers agents to perform complex tasks, LLMs may invoke unintended tool interactions and introduce risks, such as leaking sensitive data or overwriting critical records, which are unacceptable in enterprise contexts. Current approaches to mitigate these risks, such as model-based safeguards, enhance agents’ reliability but cannot guarantee system safety. Methods like information flow control (IFC) and temporal constraints aim to provide guarantees but often require extensive human annotation. We propose a process that starts with applying System-Theoretic Process Analysis (STPA) to identify hazards in agent workflows, derive safety requirements, and formalize them as enforceable specifications on data flows and tool sequences. To enable this, we introduce a capability-enhanced Model Context Protocol (MCP) framework that requires structured labels on capabilities, confidentiality, and trust level. Together, these contributions aim to shift LLM-based agent safety from ad hoc reliability fixes to proactive guardrails with formal guarantees, while reducing dependence on user confirmation and making autonomy a deliberate design choice.

Human error is often associated with system failures. The complexity of human-automation interaction can make it difficult to anticipate what errors can occur and how they contribute to failures. Previous research has shown that task analytic behavior modeling with the enhanced operator function model and the cognitive reliability analysis method (CREAM) can be combined with statistical model checking to make predictions about human error rates, their stochastic impact on system failures, and the effect of negative transfer of design changes on these predictions. These efforts were successful, but the validation studies used artificial examples with limited data. Predictions also slightly overestimated error rates. This article addresses these deficiencies by conducting a validation study based on the prescription order entry interface of the OpenEMR electronic medical record. As part of this, we explored how prediction accuracy for the OpenEMR application changed based on the inclusion/exclusion of planning errors: errors based on people’s ability to formulate task plans, which we hypothesized contributed to error rate overestimation. Results found that our method’s predictions aligned with those observed in the experiment, especially when planning errors were excluded. Negative transfer conditions did not manifest significant differences in error rates experimentally or in model predictions. These results suggest that negative transfer’s impact on human–computer interaction may be overstated in the literature. Finally, higher error rates were observed between the original OpenEMR prescription order entry interface compared to an alternative that we tested. We highly suggest that OpenEMR adopt the alternative.

Signal Temporal Logic (STL) offers a concise yet expressive framework for specifying and reasoning about spatio-temporal behaviors of robotic systems. Attractively, STL admits the notion of robustness, the degree to which an input signal satisfies or violates an STL specification, thus providing a nuanced evaluation of system performance. In particular, the differentiability of STL robustness enables direct integration to robotic workflows that rely on gradient-based optimization, such as trajectory optimization and deep learning. However, existing approaches to evaluating and differentiating STL robustness rely on recurrent computations, which become inefficient with longer sequences, limiting their use in time-sensitive applications. In this letter, we present STLCG++, a masking-based approach that parallelizes STL robustness evaluation and backpropagation across timesteps, achieving significant speed-ups compared to a recurrent approach. We also introduce a smoothing technique to enable the differentiation of time interval bounds, thereby expanding STL's applicability in gradient-based optimization tasks involving spatial and temporal variables. Finally, we demonstrate STLCG++’s benefits through three robotics use cases and provide JAX and PyTorch libraries for seamless integration into modern robotics workflows.