A formal framework for design and verification of robotic agents

Intelligent robots are autonomous and are used in environments where human interaction is hazardous or impossible. Verification of software for intelligent robots is mandatory because in situations where intelligent robots are employed online, error recovery is almost impossible. In this paper, we provide a formal framework for offline verification of software used in robotic applications. The specification enables one to design a robotic agent which represents a class of real-life robots. Forward and inverse kinematic operations of the robotic agent are specified using the specification for rigid solids and their primitive operations. An object-oriented design of the robotic agent derived from the specifications is given. We use the specification technique VDM for our purpose.This work was partially supported by FCAR, Quebec and NSERC, Canada.     

A formal methodology for integral security design and verification of network protocols

In this work we propose a methodology for incorporating the verification of the security properties of network protocols as a fundamental component of their design. This methodology can be separated in two main parts: context and requirements analysis along with its informal verification; and formal representation of protocols and the corresponding procedural verification. Although the procedural verification phase does not require any specific tool or approach, automated tools for model checking and/or theorem proving offer a good trade-off between effort and results. In general, any security protocol design methodology should be an iterative process addressing in each step critical contexts of increasing complexity as result of the considered protocol goals and the underlying threats. The effort required for detecting flaws is proportional to the complexity of the critical context under evaluation, and thus our methodology avoids wasting valuable system resources by analyzing simple flaws in the first stages of the design process. In this work we provide a methodology in coherence with the step-by-step goals definition and threat analysis using informal and formal procedures, being our main concern to highlight the adequacy of such a methodology for promoting trust in the accordingly implemented communication protocols. Our proposal is illustrated by its application to three communication protocols: MANA III, WEP's Shared Key Authentication and CHAT-SRP.     

MASCF: A generic process-centered methodological framework for analysis and design of multi-agent supply chain systems

Multi-agent systems (MAS) are becoming popular for modeling complex systems such as supply chains. However, development of multi-agent systems remain quite involved and extremely time consuming. Currently, there exist no generic methodologies for modeling supply chains using multi-agent systems. In this research, we propose a generic process-centered methodological framework, Multi-Agent Supply Chain Framework (MASCF), to simplify MAS development for supply chain (SC) applications. MASCF introduces the notion of process-centered organization metaphor, and creatively adopts Supply Chain Operations Reference (SCOR) model to a well-structured generic MAS analysis and design methodology, Gaia, for multi-agent supply chain system (MASCS) development. The popular Tamagotchi case was designed and analyzed using MASCF. The validity of the framework was established by implementing MASCF output of Tamagotchi SC using the Java Agent DEvelopment Framework (JADE).     

A formal framework for software product lines

ContextA Software Product Line is a set of software systems that are built from a common set of features. These systems are developed in a prescribed way and they can be adapted to fit the needs of customers. Feature models specify the properties of the systems that are meaningful to customers. A semantics that models the feature level has the potential to support the automatic analysis of entire software product lines.ObjectiveThe objective of this paper is to define a formal framework for Software Product Lines. This framework needs to be general enough to provide a formal semantics for existing frameworks like FODA (Feature Oriented Domain Analysis), but also to be easily adaptable to new problems.MethodWe define an algebraic language, called SPLA, to describe Software Product Lines. We provide the semantics for the algebra in three different ways. The approach followed to give the semantics is inspired by the semantics of process algebras. First we define an operational semantics, next a denotational semantics, and finally an axiomatic semantics. We also have defined a representation of the algebra into propositional logic.ResultsWe prove that the three semantics are equivalent. We also show how FODA diagrams can be automatically translated into SPLA. Furthermore, we have developed our tool, called AT, that implements the formal framework presented in this paper. This tool uses a SAT-solver to check the satisfiability of an SPL.ConclusionThis paper defines a general formal framework for software product lines. We have defined three different semantics that are equivalent; this means that depending on the context we can choose the most convenient approach: operational, denotational or axiomatic. The framework is flexible enough because it is closely related to process algebras. Process algebras are a well-known paradigm for which many extensions have been defined.     

A formal framework of multi-agent systems with requirement/service cooperative style

Adopting three kinds of speech acts:request,promise,and inform,this paper analyses the interaction among agents in a kind of multi-agent systems with requirements/services cooperation style(MASr-s).The paper gives the objective model the theoretic satisfaction conditions of three kinds of speech acts in MASr-s.The formal definition of MASr-s has been presented.To evaluate concrete implementation architecture and mechanism of the variant MASr-s.including client/server computing architecture and mechanism,a spectrum of MASr-s has been proposed,which captures direct request/passive service mechanism,direct request /active service mechanism,indirect request/active service mechanism,and peer to-peer request /service mechanism.The Spectrum shows a thread to improve traditional client/server computing.     

A new framework of consensus protocol design for complex multi-agent systems

This paper aims to find a simple but efficient method for consensus protocol design. This paper presents two consensus protocols to solve the consensus problem of complex multi-agent systems that consist of inhomogeneous subsystems. The limitations of current studies are analyzed, and a novel model based on transfer functions is presented. This model can be used to describe both homogeneous and inhomogeneous multi-agent systems in a unified framework. Based on this model, two sufficient and necessary conditions for the consensus of complex multi-agent systems have been obtained. One is for the systems without any external input, and the other is for the systems with the same external input. Then, two corresponding distributed consensus protocols are presented. Considering that the complex multi-agent systems may require different outputs sometimes, the relationship between inputs and outputs is analyzed. Finally, some simulations are given to demonstrate the performance and effectiveness of the proposed approaches.     

A framework for simulating real-time multi-agent systems

In this paper, we describe an implementation of use in demonstrating the effectiveness of architectures for real-time multi-agent systems. The implementation provides a simulation of a simplified RoboCup Search and Rescue environment, with unexpected events, and includes a simulator for both a real-time operating system and a CPU. We present experimental evidence to demonstrate the benefit of the implementation in the context of a particular hybrid architecture for multi-agent systems that allows certain agents to remain fully autonomous, while others are fully controlled by a coordinating agent. In addition, we discuss the value of the implementation for testing any models for the construction of real-time multi-agent systems and include a comparison to related work.

A survey of security in multi-agent systems

Multi-agent systems (MAS) are a relatively new software paradigm that is being widely accepted in several application domains to address large and complex tasks. However, with the use of MAS in open, distributed and heterogeneous applications, the security issues may endanger the success of the application. The goal of this research is to identify the security issues faced by MAS and to survey the current state of the art of this field of knowledge. In order to do it, this paper examines the basic concepts of security in computing, and some characteristics of agents and multi-agent systems that introduce new threats and ways to attack. After this, some models and architectures proposed in the literature are presented and analyzed.     

A framework for the design and automated implementation of communication aspects in multi-agent systems

This paper presents REFCON, a framework for the automated development of Agent Communication Contexts (ACCs) in multi-agent systems (MASs). ACCs are intended to capture the interaction requirements of a MAS.A formal specification framework is first presented, aimed at modelling an ACC as a set of rules for filtering and filling messages, based on their contents, and the names and roles of the exchanging agents. A XML-based specification language is then introduced, which encodes the specification formalism for the sake of its computer processing. Finally, an object-oriented software architecture capable of supporting ACC-based MAS development is presented.REFCON key characteristic is that it allows a seamless integration of ACC support (even) into an existing MAS, at run-time, independently of the agent platform used for the implementation. This is made possible by a layered software architecture based on computational reflection, a technology that allows transparent evolution and adaptation of existing systems. The REFCON framework is also dynamic, in the two-fold sense that it is capable of both adding new rules and handling multiple contexts, which it can easily switch among, at run-time. The ACC-based design of an example MAS for document sharing is briefly discussed, as a demonstration of the principles put forward.     

A framework for meta-level control in multi-agent systems

Sophisticated agents operating in open environments must make decisions that efficiently trade off the use of their limited resources between dynamic deliberative actions and domain actions. This is the meta-level control problem for agents operating in resource-bounded multi-agent environments. Control activities involve decisions on when to invoke and the amount to effort to put into scheduling and coordination of domain activities. The focus of this paper is how to make effective meta-level control decisions. We show that meta-level control with bounded computational overhead allows complex agents to solve problems more efficiently than current approaches in dynamic open multi-agent environments. The meta-level control approach that we present is based on the decision-theoretic use of an abstract representation of the agent state. This abstraction concisely captures critical information necessary for decision making while bounding the cost of meta-level control and is appropriate for use in automatically learning the meta-level control policies.     

A framework for facilitating cooperation in multi-agent systems

This work introduces a multi-agent framework that facilitates cooperation in multi-agent robotic systems. It uses a layered approach based on Coloured Petri Nets for modelling complex, concurrent conversations among agents. In this approach each agent employs a Coloured Petri Net model that allows agents to follow a plan specifying their interactions. It also allows programmers to plan for the concurrent feature of the conversation and make sure that all possible states of the problem space are considered. The framework assists the agents to identify and adapt different strategies for teammates and task selection dynamically. The agents can change their strategies in the course of dynamic environments to improve their performance. We have examined the performance of the agents in this framework by developing some task selection and teammate selection strategies for agents in a disaster scenario.     

A formal framework for business process modelling and design

We present a formal framework for enterprise and business process modelling. The concepts of our framework (objectives and goals, roles and actors, actions and processes, responsibilities and constraints) allow business analysts to capture enterprise knowledge in a way that is both intuitive and mathematically formal. We also outline the basic steps of a methodology that allows business analysts to produce detailed, formal specifications of business processes from high-level enterprise objectives. The use of a formal language permits us to verify that the specifications possess certain correctness properties, namely that the responsibilities assigned to roles are fulfilled, and that constraints are maintained as a result of process execution.     

A framework for determining design correctness

Quality is one of the main concerns in today's systems and software development and use. One important instrument in verification is the use of formal methods, which means that requirements and designs are analyzed formally to determine their relationships. Furthermore, since professional software design is to an increasing extent a distributed process, the issue of integrating different systems to an entity is of great importance in modern system development and design. Various candidates for formalizing system development and integration have prevailed, but very often, particularly for dynamic conflict detection, these introduce non-standard objects and formalisms, leading to severe confusion, both regarding the semantics and the computability. In contrast to such, we introduce a framework for defining requirement fulfillment by designs, detecting conflicts of various kinds as well as integration of heterogeneous schemata. The framework introduced transcends ordinary logical consequence, as it takes into account static and dynamic aspects of design consistency and, in particular, the specific features of the state space of a specification. Another feature of the approach is that it provides a unifying framework for design conflict analysis and schema integration.     

Towards a formal framework for software reuse

It is reasonable to expect that the use of formal methods in software reuse will help improve the practice of this discipline as well as enhance our understanding of its products and processes. We have identified the following technical activities that take place in software reuse as candidates for a formal modeling: representing reusable assets, representing reuse queries, defining matching criteria, defining a storage structure, deriving measures of distance and deriving a calculus of program modification. In this paper we discuss how a simple mathematical model based on set theory and relation theory allows us to capture these activities in a unified, coherent framework.     

A formal verification framework for static analysis

Static analysis tools, such as resource analyzers, give useful information on software systems, especially in real-time and safety-critical applications. Therefore, the question of the reliability of the obtained results is highly important. State-of-the-art static analyzers typically combine a range of complex techniques, make use of external tools, and evolve quickly. To formally verify such systems is not a realistic option. In this work, we propose a different approach whereby, instead of the tools, we formally verify the results of the tools. The central idea of such a formal verification framework for static analysis is the method-wise translation of the information about a program gathered during its static analysis into specification contracts that contain enough information for them to be verified automatically. We instantiate this framework with costa, a state-of-the-art static analysis system for sequential Java programs, for producing resource guarantees and KeY, a state-of-the-art verification tool, for formally verifying the correctness of such resource guarantees. Resource guarantees allow to be certain that programs will run within the indicated amount of resources, which may refer to memory consumption, number of instructions executed, etc. Our results show that the proposed tool cooperation can be used for automatically producing verified resource guarantees.     

A new algebraic structure for formal concept analysis

Formal concept analysis (FCA) originally proposed by Wille [39], is an important theory for data analysis and knowledge discovery. Concept lattice is the core of the mathematical theory of formal concept analysis. To address the requirements of real word applications, concept lattice has been extended to many other forms from the theoretical point of view and possible applications. In this paper, with the aim of deriving the mathematical properties of formal concepts from the point of algebra, we propose a new algebra system for the formal context. Under the frame of the proposed system, some interesting properties of formal concepts are explored, which could be applied to explore concept hierarchy and ontology merging.     

A formal analysis of bluetooth device discovery

This paper presents a formal analysis of the device discovery phase of the Bluetooth wireless communication protocol. The performance of this process is the result of a complex interaction between several devices, some of which exhibit random behaviour. We use probabilistic model checking and, in particular, the tool PRISM to compute the best- and worst-case performance of device discovery: the expected time for the process to complete and the expected power consumption. We illustrate the utility of performing an exhaustive, low-level analysis to produce exact results in contrast to simulation techniques, where additional probabilistic assumptions must be made. We demonstrate an example of how seemingly innocuous assumptions can lead to incorrect performance estimations. We also analyse the effectiveness of improvements made between versions 1.1 and 1.2 of the Bluetooth specification.     

'Soft' systems thinking and information systems: a framework for client-led design

Abstract. Since the mid-1980s there has been a growing interest in the application of soft systems methodology (SSM) to the information systems design process. This interest has resulted from attempts to overcome the recognized deficiencies of conventional computer systems analysis methods and techniques. A particular problem which has received attention over the past 5 years is the epistemological and operational differences between the investigative process of the pre-design stage and the technological specification. We suggest that this argument is somewhat unproductive and advocate a necessary rethinking about the nature of information systems and the use of technology to support their activities. A re-evaluation of the way that we set about designing computer-based information systems suggests that many of the problems of conventional systems analysis methods may be alleviated by an approach that allows the 'client', or 'user', to have a greater control over the identification, specification and development of their information system(s). The authors' belief in this course of action has led to the development of client-led design as an underpinning philosophy for user participation in the design of computer-based information systems. Client-led design draws upon and develops concepts and tools from 'interpretive', or 'soft', systems thinking and, in particular, can be seen as providing a framework for the type of subjective inquiry that Checkland & Scholes (1990) referred to as 'ideal-type' mode 2 SSM. This paper is related to the papers published in the Journal of Information Systems (Vol. 3, No. 3), which was a special edition to illustrate the influence of 'soft' systems thinking upon information systems design and development.     

A formal mathematical framework for modeling probabilistic hybrid systems

The development of autonomous agents, such as mobile robots and software agents, has generated considerable research in recent years. Robotic systems, which are usually built from a mixture of continuous (analog) and discrete (digital) components, are often referred to as hybrid dynamical systems. Traditional approaches to real-time hybrid systems usually define behaviors purely in terms of determinism or sometimes non-determinism. However, this is insufficient as real-time dynamical systems very often exhibit uncertain behavior. To address this issue, we develop a semantic model, Probabilistic Constraint Nets (PCN), for probabilistic hybrid systems. PCN captures the most general structure of dynamic systems, allowing systems with discrete and continuous time/variables, synchronous as well as asynchronous event structures and uncertain dynamics to be modeled in a unitary framework. Based on a formal mathematical paradigm exploiting abstract algebra, topology and measure theory, PCN provides a rigorous formal programming semantics for the design of hybrid real-time embedded systems exhibiting uncertainty.