Formal modeling of multi-agent systems is an active area of research. The use of precise and unambiguous notation of formal methods is used to accurately describe and reason about the system under consideration at the design time. Multi-agent systems deployed in dynamic and unpredictable environment needs to have the ability of self-adaptation, making them adaptable to the failures. State of the art encourages the use of MAPE-K feedback loop for the provision of self-adaptation in any system. There is a dire need of formal vocabulary that can be used for the conceptual design of any real-time multi-agent system with self-adaptation. In this paper, we have proposed a set of predefined interfaces for the provision of self-adaptation in real-time multi-agent systems. The interfaces are based on monitor, analyze, plan, and execute phases of the MAPE-K feedback loop. We formally specify our interfaces using timed-communicating object-Z language. The complete framework is elaborated using a trivial case-study of conveyor belt system based on a real-time agent architecture.

In this study we have formally specified and verified the actions of communicating real-time software agents (RTAgents). Software agents are expected to work autonomously and deal with unfamiliar situations astutely. Achieving cent percent test cases coverage for these agents has always been a problem due to limited resources. Also a high degree of dependability and predictability is expected from real-time software agents. In this research we have used Timed-Arc Petri Net's for formal specification and verification. Formal specification of e-agents has been done in the past using Linear Temporal Logic (LTL) but we believe that Timed-Arc Petri Net's being more visually expressive provides a richer framework for such formalism. A case study of Stock Market System (SMS) based on Real Time Multi Agent System framework (RTMAS) using Timed-Arc Petri Net's is taken to illustrate the proposed modeling approach. The model was verified used AF, AG, EG, and EF fragments of Timed Computational Tree Logic (TCTL) via translations to timed automata

Background: Software agents are expected to work autonomously and deal with unfamiliar situations astutely. Achieving cent percent test case coverage for these agents has always been a problem due to limited resources. Also a high degree of dependability is expected from autonomous software agents. Formal verification of these systems can be done by specifying the possible actions of the agents to increase the confidence in the correctness of such systems. Methods: We have used social approach of agent communication where actions of the agents are described as social obligation between the participants. Formal specification of e-agents was done using μ-calculus as it is more expressive than Linear Temporal Logic (LTL). An algorithm has been given for syntactic conversion of μ-calculus formulas to TAPA model checker environment. Results: Using converstion algorithm syntactically modified μ-calculus formulas will be executed on TAPA model checker to verify the system being modelled for the specified properties. Application: The study will help to provide future directions for formal modelling of e-agents for their correct functioning.

Energy efficiency in mobile computing is really an important issue these days. Owing to the popularity and prevalence of Android operating system among the people, a great number of Android smartphone applications have been developed and proliferated by the software developers. While developing these applications, developers have to keep energy consumption factor in mind, as the efficiency of an application is largely affected by it. Thus, designers and programmers endeavour to choose the best designing approaches to develop energy-efficient applications. It is imperative to assist the programmers in choosing appropriate techniques and strategies to manage power consumption. In the present research, we have investigated the effect of Android application design on its energy utilisation. For this purpose, we have practically implemented design patterns on two Android applications and evaluated their energy consumption before and after implementing these patterns. We have modelled the high-level design of these two Android applications by using software design patterns in such a way as to abate their energy requirement. We have also checked how the quality, maintainability, and efficiency of code are affected by these design patterns. The outcomes of the research can facilitate programmers to utilise these details while developing energy efficient solutions.

Self-adaptive systems (SASs) have the capability to evaluate and change their behavior according to changes occurring in the environment. Research in this field is being held since mid-60, and over the last decade, the importance of self-adaptivity is being increased. In the proposed research, colored petri nets (CPN) formal language is being used to model self-adaptive multiagent system. CPN is increasingly used to model self-adaptive complex concurrent systems due to its flexible formal specification and formal verification behavior. CPN being visually more expressive than simple, Petri Nets enable diverse modeling approaches and provides a richer framework for such a complex formalism. The main goal of this research is to apply self-adaptive multi-agent concurrent system (SMACS) for complex architectures. In our previous research, the SMACS framework is proposed and verified through traffic monitoring system. All agents of SMACS are also known as intelligent agents due to their self-adaptation behavior. Due to decentralized approach in this framework, each agent will intelligently adapt its behavior in the environment and send updates to other agents. In this research, we are choosing smart computer lab (SCL) as a case study. For internal structure of each agent modal, μ -calculus will be used, and then a model checker TAPAs: a tool for the analysis of process algebras will be applied to verify these properties. CPN-based state space analysis will also be done to verify the behavioral properties of the model. The general objective of the proposed system is to maximize the utility generated over some predetermined time horizon.

Concurrency in Intuitionistic Linear-Time μ-Calculus: A Case study of Manufacturing System