Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Internal Challenges <s> This article deals with the problem of dynamic role-playing in Multi-Agent organisations. The approach presented uses a formal specification notation and is based upon a formal framework which defines the concepts of role, interaction and organisation. Within this framework the problem of dynamic role-playing specification is related to the merging of specifications. The formal notation used composes Object-Z and Statecharts. The main features of this approach are: enough expressive power to represent Multi-Agents dynamic aspects, tools for specification analysis and mechanisms allowing the refinement of a high level specification into a low level specification which can be easily implemented. The last part of this paper presents an application with the specification of a reactive and cooperative MAS model named Satisfaction Altruism. An analysis of the specification validates the agents' behaviours. <s> BIB001 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Internal Challenges <s> The development of theoretical-based methods for the assessment of multi-agent systems properties is of critical importance. This work is a preliminary investigation on methodologies for modeling, analysis and design of multi-agent systems. Multi-agent systems are regarded as discrete-event dynamic systems and Petri nets are used as a modeling tool to assess the structural properties of the multi-agent system. Our methodology consists of defining a simple multi-agent system based on the abstract architecture for intelligent agents. The abstract architecture is modeled as a discrete-event system using Petri nets and structural analysis of the net provides an assessment of the communication and coordination properties of the multi-agent system. Deadlock avoidance in the multi-agent system is considered as an initial key property, and it is evaluated using liveness and boundedness properties of the Petri net model. <s> BIB002 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Internal Challenges <s> Given a robot model and a class of admissible environments, this paper provides a framework for automatically and verifiably composing controllers that satisfy high level task specifications expressed in suitable temporal logics. The desired task specifications can express complex robot behaviors such as search and rescue, coverage, and collision avoidance. In addition, our framework explicitly captures sensor specifications that depend on the environment with which the robot is interacting, resulting in a novel paradigm for sensor-based temporal logic motion planning. As one robot is part of the environment of another robot, our sensor-based framework very naturally captures multi-robot specifications. Our computational approach is based on first creating discrete controllers satisfying so-called general reactivity formulas. If feasible, the discrete controller is then used in order to guide the sensor-based composition of continuous controllers resulting in a hybrid controller satisfying the high level specification, but only if the environment is admissible. <s> BIB003 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Internal Challenges <s> Organic computing systems are systems which have the capability to autonomously (re-)organize and adapt themselves. The benefit of such systems with self-x properties is that they are more dependable, as they can compensate for some failures. They are easier to maintain, because they can automatically configure themselves and are more convenient to use because of automatic adaptation to new situations. While organic computing systems have a lot of desired properties, there still exists only little knowledge on how they can be designed and built.In this paper an approach for specification and construction of a class of organic computing systems is presented, called the (RIA). The core idea is that the behaviour of an organic computing system can be split into productive phases and self-x phases. This allows for a generic description of how ``organic'' aspects can be specified and implemented. The approach will be illustrated by applying it to a design methodology for organic computing systems and further refining it to an explicit case study in the domain of production automation. <s> BIB004 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Internal Challenges <s> Autonomous robots are complex systems that require the interaction/cooperation of numerous heterogeneous software components. Nowadays, robots are critical systems and must meet safety properties including in particular temporal and real-time constraints. We present a methodology for modeling and analyzing a robotic system using the BIP component framework integrated with an existing framework and architecture, the LAAS Architecture for Autonomous System, based on GenoM. The BIP componentization approach has been successfully used in other domains. In this study, we show how it can be seamlessly integrated in the preexisting methodology. We present the componentization of the functional level of a robot, the synthesis of an execution controller as well as validation techniques for checking essential “safety” properties. <s> BIB005 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Internal Challenges <s> Autonomous robots are complex systems that require the interaction/cooperation of numerous heterogeneous software components. Nowadays, robots are getting closer to humans and as such are becoming critical systems which must meet safety properties including in particular logical, temporal and real-time constraints. We present an evolution of the LAAS Architecture for Autonomous System and its tool GenoM. This evolution is based on the BIP (Behaviors Interactions Priorities) component based design framework which has been successfully used in other domains (e.g. embedded systems). In this study, we show how we seamlessly integrate BIP in the preexisting methodology. We present the componentization of the functional level of a robot, the synthesis of an execution controller as well as validation techniques for checking essential safety properties. This approach has been integrated in the LAAS architecture and we have performed a number of experiment in simulation but also on a real robot (DALA). <s> BIB006 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Internal Challenges <s> This paper presents the latest developments of the Extensible Agent Behavior Specication Language (XABSL), a modular and scalable tool for engineering complex multiagent behavior. It is based on hierarchical nite state machines. By the new extensions the development of cooperative multi agent behavior is supported through language elements which allow to conveniently specify how the state machines of multiple agents interact. Basic properties of XABSL are illustrated in direct comparison with Petri Net Plans and the COLBERT language using examples of basic robot behavior. More complex examples from robot soccer are used to illustrate the new extensions of XABSL. The complete system is available online on the XABSL website (http://www.xabsl.de). <s> BIB007 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Internal Challenges <s> It is a characteristic of swarm robotics that modelling the overall swarm behaviour in terms of the low-level behaviours of individual robots is very difficult. Yet if swarm robotics is to make the transition from the laboratory to real-world engineering realisation such models would be critical for both overall validation of algorithm correctness and detailed parameter optimisation. We seek models with predictive power: models that allow us to determine the effect of modifying parameters in individual robots on the overall swarm behaviour. This paper presents results from a study to apply the probabilistic modelling approach to a class of wireless connected swarms operating in unbounded environments. The paper proposes a probabilistic finite state machine (PFSM) that describes the network connectivity and overall macroscopic behaviour of the swarm, then develops a novel robot-centric approach to the estimation of the state transition probabilities within the PFSM. Using measured data from simulation the paper then carefully validates the PFSM model step by step, allowing us to assess the accuracy and hence the utility of the model. <s> BIB008 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Internal Challenges <s> This paper presents a formal specification-based software monitoring approach that can dynamically and continuously monitor the behaviors of a target system and explicitly recognize undesirable behaviors in the implementation with respect to its formal specification. The key idea of our approach is in building a monitoring module that connects a specification animator with a program debugger. The requirements information about expected dynamic behaviors of the target system are gathered from the formal specification animator, while the actual behaviors of concrete implementations of the target system are obtained through the program debugger. Based on the information obtained from both sides, the judgement on the conformance of the concrete implementation with respect to the formal specification is made timely while the target system is running. Furthermore, the proposed formal specification-based software monitoring technique does not embed any instrumentation codes to the target system nor does it annotate the target system with any formal specifications. It can detect implementation errors in a real-time manner, and help the developers and users of the system to react to the problems before critical failure occurs. <s> BIB009 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Internal Challenges <s> Michigan/AFRL Collaborative Center on Control Sciences, AFOSR (grant no. FA 8650-07-2-3744) <s> BIB010 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Internal Challenges <s> The paper addresses formal systems verification of autonomous underwater vehicles (AUV). The verification process includes hybrid system modelling and formulation of the discrete representation using natural language programming (sEnglish) via compositional abstraction - employing data, perception and action abstraction methods; the translation of the discrete abstraction into interpreted script programming language (ISPL) of a mainstream multi-agent model checker (MCMAS) for reachability verification of undesirable states, and ultimately the bridging into the discrete event system representation in Stateflow formalism. Using this technique, modelling and model checking can include the complete physical system of the autonomous vehicle, its multi-agent software on board and also the human interface represented as an agent. <s> BIB011 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Internal Challenges <s> Self-adaptive software systems are an emerging class of systems that adjust their behavior at runtime to achieve certain functional or quality of service objectives. The construction of such systems has shown to be significantly more challenging than traditional systems, partly because researchers and practitioners have been struggling with the lack of a precise method of describing, comparing, and evaluating alternative architectural choices. In this paper, we introduce a reference model, entitled FOrmal Reference Model for Self-adaptation (FORMS), which intends to alleviate this pressing issue. FORMS consists of a small number of formally specified modeling primitives that correspond to the key variation points within self-adaptive software systems, and a set of relationships that guide their composition. We present our experiences with applying FORMS to several existing systems, which not only demonstrates its ability to precisely illuminate their underlying characteristics, but also its potential as a method of rigorously specifying architectural patterns for this domain. <s> BIB012 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Internal Challenges <s> We present a computational framework for automatic synthesis of control and communication strategies for a robotic team from task specifications given as regular expressions about servicing requests in an environment. Our approach is based on two main ideas. First, we extend recent results from formal synthesis of distributed systems to check for the distributability of the task specification and to generate local specifications, while accounting for the service and communication capabilities of the robots. Second, by using a technique inspired from LTL model checking, we generate individual control and communication strategies. We illustrate the method with experimental results in our Robotic Urban-Like Environment. <s> BIB013 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Internal Challenges <s> Robot swarms provide a way for a number of simple robots to work together to carry out a task. While swarms have been found to be adaptable, fault-tolerant and widely applicable, designing individual robot algorithms so as to ensure effective and correct swarm behaviour is very difficult. In order to assess swarm effectiveness, either experiments with real robots or computational simulations of the swarm are usually carried out. However, neither of these involve a deep analysis of all possible behaviours. In this paper we will utilise automated formal verification techniques, involving an exhaustive mathematical analysis, in order to assess whether our swarms will indeed behave as required. <s> BIB014 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Internal Challenges <s> Programming the behavior of multi-robot systems is a challenging task which has a key role in developing effective systems in many application domains. In this paper, we present Petri Net Plans (PNPs), a language based on Petri Nets (PNs), which allows for intuitive and effective robot and multi-robot behavior design. PNPs are very expressive and support a rich set of features that are critical to develop robotic applications, including sensing, interrupts and concurrency. As a central feature, PNPs allow for a formal analysis of plans based on standard PN tools. Moreover, PNPs are suitable for modeling multi-robot systems and the developed behaviors can be executed in a distributed setting, while preserving the properties of the modeled system. PNPs have been deployed in several robotic platforms in different application domains. In this paper, we report three case studies, which address complex single robot plans, coordination and collaboration. <s> BIB015 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Internal Challenges <s> We model the dynamics of self-organized robot aggregation inspired by a study on the aggregation of gregarious arthropods. In swarms of German cockroaches, aggregation into clusters emerges solely from local interactions between the individuals, whereas the probabilities of joining or leaving a cluster are a function of the cluster size. We propose a non-spatial population dynamics model that keeps track of the number of robots in clusters of specific size using control parameters of the individual robots and the probability of detecting another robot in the environment. The model is able to quantitatively and qualitatively predict the dynamics observed in extensive realistic multi-robot simulation, and provides qualitative agreement with data obtained from aggregation of Blattela germanica larvae. In particular, we show by analysis, numerical and realistic simulation that the emergence of a single aggregate requires a minimal communication range between individuals. <s> BIB016 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Internal Challenges <s> A robot swarm is a collection of simple robots designed to work together to carry out some task. Such swarms rely on: the simplicity of the individual robots; the fault tolerance inherent in having a large population of often identical robots; and the self-organised behaviour of the swarm as a whole. Although robot swarms are being deployed in increasingly sophisticated areas, designing individual control algorithms that can guarantee the required global behaviour is difficult. In this paper we apply and assess the use of formal verification techniques, in particular that of model checking, for analysing the emergent behaviours of robotic swarms. These techniques, based on the automated analysis of systems using temporal logics, allow us to analyse all possible behaviours and so identify potential problems with the robot swarm conforming to some required global behaviour. To show this approach we target a particular swarm control algorithm, and show how automated temporal analysis can help to refine and analyse such an algorithm. <s> BIB017 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Internal Challenges <s> Verification of component-based systems still suffers from limitations such as state space explosion since a large number of different components may interact in an heterogeneous environment. Those limitations entail the need for complementary verification methods such as runtime verification based on dynamic analysis and prone to scalability. In this paper, we integrate runtime verification into the BIP (Behavior, Interaction, and Priority) framework. BIP is a powerful component-based framework for the construction of heterogeneous systems. Our method augments BIP systems with monitors checking a user-provided specification. This method has been implemented in RV-BIP, a prototype tool that we used to validate the whole approach on a robotic application. <s> BIB018 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Internal Challenges <s> In this paper, we develop a computational framework for fully automatic deployment of a team of unicycles from a global specification given as an LTL formula over some regions of interest. Our hierarchical approach consists of four steps: (i) the construction of finite abstractions for the motions of each robot, (ii) the parallel composition of the abstractions, (iii) the generation of a satisfying motion of the team; (iv) mapping this motion to individual robot control and communication strategies. The main result of the paper is an algorithm to reduce the amount of inter-robot communication during the fourth step of the procedure. <s> BIB019 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Internal Challenges <s> Recent work in robotics has applied formal verification tools to automatically generate correct-by-construction controllers for autonomous robots. However, when it is not possible to create such a controller, these approaches do not provide the user with feedback on the source of failure, making the experience of debugging a specification somewhat ad hoc and unstructured, and a source of frustration for the user. This paper describes an extension to the LTLMoP toolkit for robot mission planning that encloses the control-generation process in a layer of automated reasoning to identify the cause of failure, and targets the users attention to flawed portions of the specification. <s> BIB020 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Internal Challenges <s> The challenges of pervasive and mobile computing environments, which are highly dynamic and unpredictable, have motivated the development of self-adaptive software systems. Although noteworthy successes have been achieved on many fronts, the construction of such systems remains significantly more challenging than traditional systems. We argue this is partially because researchers and practitioners have been struggling with the lack of a precise vocabulary for describing and reasoning about the key architectural characteristics of self-adaptive systems. Further exacerbating the situation is the fact that existing frameworks and guidelines do not provide an encompassing perspective of the different types of concerns in this setting. In this article, we present a comprehensive reference model, entitled FOrmal Reference Model for Self-adaptation (FORMS), that targets both issues. FORMS provides rigor in the manner such systems can be described and reasoned about. It consists of a small number of formally specified modeling elements that correspond to the key concerns in the design of self-adaptive software systems, and a set of relationships that guide their composition. We demonstrate FORMS's ability to precisely describe and reason about the architectural characteristics of distributed self-adaptive software systems through its application to several existing systems. FORMS's expressive power gives it a potential for documenting reusable architectural solutions (e.g., architectural patterns) to commonly encountered problems in this area. <s> BIB021 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Internal Challenges <s> We have recently started an effort to combine a state of the art tool for developing functional modules of robotic systems (G^e^noM) with a component based framework for implementing embedded real-time systems (BIP). Unlike some works which study the connection between formal approaches and the highest (decisional) level of the robot software architecture, where deliberative activities such as planning, diagnostics, and execution control are conducted, we tackle the problem of using formal methods for developing modules of the functional level of robots. Little attention has been drawn to the development of these modules whose robustness is paramount to the robustness of the overall platform. To this end, we have successfully developed the G^e^noM/BIP component based design approach and applied it to the functional level of a complex exploration rover. Here, we report on this work, and show how we: (i) produce a very fine grained formal computational model of the robot functional level; (ii) run the BIP engine on the real robot, which executes and enforces the model semantics at runtime; and (iii) check the model offline for deadlock-freedom, as well as other safety properties. Moreover, we also extended this paradigm in a number of promising directions: (i) introduced a real-time BIP engine which can now use and control a timed BIP model; (ii) distributed the model and the engine over multiple CPUs; (iii) proposed a user-friendly language for specifying constraints on the model; and (iv) linked the model with a temporal plan execution controller. Interestingly, although our approach was initially proposed for the lowest level of robot architectures, these more recent extensions now allow us to model and manage the deliberation taking place at the decisional layer. <s> BIB022 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Internal Challenges <s> In this paper, we propose a novel top-down design method for the development of collective behaviors of swarm robotics systems called property-driven design. Swarm robotics systems are usually designed and developed using a code-and-fix approach, that is, the developer devises, tests and modifies the individual robot behaviors until a desired collective behavior is obtained. The code-and-fix approach can be very time consuming and relies completely on the ingenuity and expertise of the designer. The idea of property-driven design is that a swarm robotics system can be described by specifying formally a set of desired properties. In an iterative process similar to test-driven development, the developer produces a model of the system that satisfies the desired properties. Subsequently, the system is implemented in simulation and using real robots. Property-driven design helps to minimize the risk of developing a system that does not satisfy the required properties, and to promote the reuse of hardware independent models. In this paper, we start by giving a general description of the method. We then present a possible way to apply it by using Discrete Time Markov Chains (DTMC) and Probabilistic Computation Tree Logic* (PCTL*). Finally, we conclude by presenting the application of the proposed method to the design and development of a swarm robotics system performing aggregation. <s> BIB023 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Internal Challenges <s> We present a computational framework for automatic synthesis of control and communication strategies for a robotic team from task specifications that are given as regular expressions about servicing requests in an environment. We assume that the location of the requests in the environment and the robot capacities and cooperation requirements to service the requests are known. Our approach is based on two main ideas. First, we extend recent results from formal synthesis of distributed systems to check for the distributability of the task specification and to generate local specifications, while accounting for the service and communication capabilities of the robots. Second, by using a technique that is inspired by linear temporal logic model checking, we generate individual control and communication strategies. We illustrate the method with experimental results in our robotic urban-like environment. <s> BIB024 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Internal Challenges <s> A robot swarm is a collection of simple robots designed to work together to carry out some task. Such swarms rely on the simplicity of the individual robots; the fault tolerance inherent in having a large population of identical robots; and the self-organised behaviour of the swarm as a whole. Although robot swarms present an attractive solution to demanding real-world applications, designing individual control algorithms that can guarantee the required global behaviour is a difficult problem. In this paper we assess and apply the use of formal verification techniques for analysing the emergent behaviours of robotic swarms. These techniques, based on the automated analysis of systems using temporal logics, allow us to analyse whether all possible behaviours within the robot swarm conform to some required specification. In particular, we apply model-checking, an automated and exhaustive algorithmic technique, to check whether temporal properties are satisfied on all the possible behaviours of the system. We target a particular swarm control algorithm that has been tested in real robotic swarms, and show how automated temporal analysis can help to refine and analyse such an algorithm. <s> BIB025 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Internal Challenges <s> We propose a methodology for decentralized multi-agent control from Linear Temporal Logic (LTL) specifications. Each agent receives an independent specification to formally synthesize its own hybrid controller. Mutual satisfiability is not a priori guaranteed. Due to limited communication, the agents utilize meeting events to exchange their controller automata and verify satisfiability through model checking. Local interaction only when common atomic propositions exist reduces the overall computational cost, facilitating scalability. Provably correct collision avoidance and convergence is ensured by Decentralized Multi-Agent Navigation Functions. <s> BIB026 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Internal Challenges <s> An alternative to deploying a single robot of high complexity can be to utilise robot swarms comprising large numbers of identical, and much simpler, robots. Such swarms have been shown to be adaptable, fault-tolerant and widely applicable. However, designing individual robot algorithms to ensure effective and correct overall swarm behaviour is actually very difficult. While mechanisms for assessing the effectiveness of any swarm algorithm before deployment are essential, such mechanisms have traditionally involved either computational simulations of swarm behaviour, or experiments with robot swarms themselves. However, such simulations or experiments cannot, by their nature, analyse all possible swarm behaviours. In this paper, we will develop and apply the use of automated probabilistic formal verification techniques to robot swarms, involving an exhaustive mathematical analysis, in order to assess whether swarms will indeed behave as required. In particular we consider a foraging robot scenario to which we apply probabilistic model checking. <s> BIB027 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Internal Challenges <s> In this paper we propose a generic framework for real-time motion planning based on model-checking and revision. The task specification is given as a Linear Temporal Logic formula over a finite abstraction of the robot motion. A preliminary motion plan is first generated based on the initial knowledge of the system model. Then real-time information obtained during the runtime is used to update the system model, verify and further revise the motion plan. The implementation and revision of the motion plan are performed in real-time. This framework can be applied to partially-known workspaces and workspaces with large uncertainties. Computer simulations are presented to demonstrate the efficiency of the framework. <s> BIB028 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Internal Challenges <s> Self-adaptation enables a software system to deal autonomously with uncertainties, such as dynamic operating conditions that are difficult to predict or changing goals. A common approach to realize self-adaptation is with a MAPE-K feedback loop that consists of four adaptation components: Monitor, Analyze, Plan, and Execute. These components share Knowledge models of the managed system, its goals and environment. To provide guarantees of the adaptation goals, state of the art approaches propose using formal models of the knowledge. However, less attention is given to the formalization of the adaptation components themselves, which is important to provide guarantees of correctness of the adaptation behavior (e.g., does the execute component execute the plan correctly?). We propose Active FORmal Models for Self-adaptation (ActivFORMS) that uses an integrated formal model of the adaptation components and knowledge models. The formal model is directly executed by a virtual machine to realize adaptation, hence active model. The contributions of ActivFORMS are: (1) the approach assures that the adaptation goals that are verified offline are guaranteed at runtime, and (2) it supports dynamic adaptation of the active model to support changing goals. We show how we have applied ActivFORMS for a small-scale robotic system. <s> BIB029 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Internal Challenges <s> Human‐robot teams are likely to be used in a variety of situations wherever humans require the assistance of robotic systems. Obvious examples include healthcare and manufacturing, in which people need the assistance of machines to perform key tasks. It is essential for robots working in close proximity to people to be both safe and trustworthy. In this paper we examine formal verification of a high-level planner/scheduler for autonomous personal robotic assistants such as CareO-bot R . We describe how a model of Care-O-bot and its environment was developed using Brahms, a multiagent workflow language. Formal verification was then carried out by translating this to the input language of an existing model checker. Finally we present some formal verification results and describe how these could be complemented by simulation-based testing and realworld end-user validation in order to increase the practical and perceived safety and trustworthiness of robotic assistants. <s> BIB030 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Internal Challenges <s> Designing software systems that have to deal with dynamic operating conditions, such as changing availability of resources and faults that are difficult to predict, is complex. A promising approach to handle such dynamics is self-adaptation that can be realized by a MAPE-K feedback loop (Monitor-Analyze-Plan-Execute plus Knowledge). To provide evidence that the system goals are satisfied, given the changing conditions, the state of the art advocates the use of formal methods. However, little research has been done on consolidating design knowledge of self-adaptive systems. To support designers, this paper contributes with a set of formally specified MAPE-K templates that encode design expertise for a family of self-adaptive systems. The templates comprise: (1) behavior specification templates for modeling the different components of a MAPE-K feedback loop (based on networks of timed automata), and (2) property specification templates that support verification of the correctness of the adaptation behaviors (based on timed computation tree logic). To demonstrate the reusability of the formal templates, we performed four case studies in which final-year Masters students used the templates to design different self-adaptive systems. <s> BIB031 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Internal Challenges <s> A new agent architecture called Limited Instruction Set Agent (LISA) is introduced for autonomous control. The new architecture is based on previous implementations of AgentSpeak and it is structurally simpler than its predecessors with the aim of facilitating design-time and run-time verification methods. The process of abstracting the LISA system to two different types of discrete probabilistic models (DTMC and MDP) is investigated and illustrated. The LISA system provides a tool for complete modelling of the agent and the environment for probabilistic verification. The agent program can be automatically compiled into a Discrete-Time Markov Chain (DTMC) or a Markov Decision Process (MDP) model for verification with PRISM. The automatically generated PRISM model can be used for both design-time and run-time verification. The run-time verification is investigated and illustrated in the LISA system as an internal modelling mechanism for prediction of future outcomes. <s> BIB032 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Summary of Internal Challenges <s> It is essential for robots working in close proximity to people to be both safe and trustworthy. We present a case study on formal verification for a high-level planner/scheduler for the Care-O-bot, an autonomous personal robotic assistant. We describe how a model of the Care-O-bot and its environment was developed using Brahms, a multiagent workflow language. Formal verification was then carried out by automatically translating this model to the input language of an existing model checker. Four sample properties based on system requirements were verified. We then refined the environment model three times to increase its accuracy and the persuasiveness of the formal verification results. The first refinement uses a user activity log based on real-life experiments, but is deterministic. The second refinement uses the activities from the user activity log nondeterministically. The third refinement uses “conjoined activities” based on an observation that many user activities can overlap. The four samples properties were verified for each refinement of the environment model. Finally, we discuss the approach of environment model refinement with respect to this case study. <s> BIB033
This section identified three internal challenges to the specification and verification of robotic systems related to how the robotic system is designed and built. These challenges are agent based, multirobot, and reconfigurable systems. Set Based BIB004 , BIB001 , BIB009 , BIB012 , BIB021 5 0 State-Transition BIB022 , BIB005 ,  , BIB006 , BIB023 , BIB002 , BIB024 , BIB013 , BIB016 ,  , BIB017 , BIB025 , BIB018 , BIB026 , BIB028 ,  ,  , BIB029 , BIB031 , BIB032 , BIB010 , BIB019 , BIB014 , BIB027 , BIB003 ,  , BIB011 , BIB020 , BIB007 , BIB030 , BIB033 , BIB008 , BIB015 33 0