Software systems are increasingly required to autonomously adapt their architectural structures and/or behaviors to runtime environmental changes. However, existing architecture-based self-adaptation approaches mostly focus on structural adaptations within a predefined space of architectural alternatives (e.g., switching between two alternative services) while merely considering quality constraints (e.g., reliability and performance). In this paper, we propose a new architecture-based self-adaptation approach, which performs behavioral adaptations with automatically generated alternatives and supports relaxed functional constraints from the perspective of business value. Specifically, we propose a technique to automatically generate behavioral alternatives of a software system from the currently-employed architectural behavioral specification. We employ business value to comprehensively evaluate the behavioral alternatives while capturing the trade-offs among relaxed functional and quality constraints. We also introduce a genetic algorithm-based planning technique to efficiently search for the optimal (sometimes a near-optimal) behavioral alternative that can provide the best business value. The experimental study on an online order processing benchmark has shown promising results that the proposed approach can improve adaptation flexibility and business value with acceptable performance overhead.

Automated negotiations play an important role in various domains modeled as multiagent systems, where agents represent human users and adopt different negotiation strategies. Generally, given a multiagent system, a negotiation strategy should be robust in the sense that most agents in the system have the incentive to choose it rather than other strategies. Empirical game-theoretic (EGT) analysis is a game-theoretic analysis approach to investigate the robustness of different strategies based on a set of empirical results. In this study, we propose that model-checking techniques can be adopted to improve EGT analysis for negotiation strategies. The dynamics of strategy profiles can be modeled as a labeled transition system using the counter abstraction technique. We define single-agent best deviation to represent the strategy deviations during negotiation, which focuses on each agent's best deviation benefit and is different from best single-agent deviation used in previous work. Two interesting properties in EGT analysis, i.e., empirical pure strategy Nash equilibrium and best reply cycle, are automatically verified to investigate the robustness of different strategies. For demonstration, the top-six strategies from the automated negotiating agents competition 2010-2012 are studied in terms of their robustness performance. In addition to identifying the most robust strategies, we supply complete rankings among them in different settings. We show that model checking is applicable and efficient to perform robustness analysis of negotiation strategies.

Commitment protocols provide an effective formalism for the regulation of agent interaction. Although existing work mainly focus on the design-time development of static commitment protocols, recent studies propose methods to create them dynamically at run-time with respect to the goals of the agents. These methods require agents to verify new commitment protocols taking their goals, and beliefs about the other agents’ behavior into account. Accordingly, in this paper, we first propose a probabilistic model to formally capture commitment protocols according to agents’ beliefs. Secondly, we identify a set of important properties for the verification of a new commitment protocol from an agent’s perspective and formalize these properties in our model. Thirdly, we develop probabilistic model checking algorithms with advanced reduction for efficient verification of these properties. Finally, we implement these algorithms as a tool and evaluate the proposed properties over different commitment protocols.

The analysis of software architecture plays an important role in understanding the system structures and facilitate proper implementation of user requirements. Despite its importance in the software engineering practice, the lack of formal description and verification support in this domain hinders the development of quality architectural models. To tackle this problem, in this work, we develop an approach for modeling and verifying software architectures specified using Monterey Phoenix (MP) architecture description language. MP is capable of modeling system and environment behaviors based on event traces, as well as supporting different architecture composition operations and views. First, we formalize the syntax and operational semantics for MP; therefore, formal verification of MP models is feasible. Second, we extend MP to support shared variables and stochastic characteristics, which not only increases the expressiveness of MP, but also widens the properties MP can check, such as quantitative requirements. Third, a dedicated model checker for MP has been implemented, so that automatic verification of MP models is supported. Finally, several experiments are conducted to evaluate the applicability and efficiency of our approach.

Multi-agent systems, which are composed of autonomous agents, have been successfully employed as a modeling paradigm in many scenarios. However, it is challenging to guarantee the correctness of their behaviors due to the complex nature of the autonomous agents, especially when they have stochastic characteristics. In this work, we propose to apply probabilistic model checking to analyze multi-agent systems. A modeling language called PMA is defined to specify such kind of systems, and LTL property and logic of knowledge combined with probabilistic requirements are supported to analyze system behaviors. Initial evaluation indicates the effectiveness of our current progress; meanwhile some challenges and possible solutions are discussed as our ongoing work.