No description available.

With the growing importance of software on which human lives increasingly depend, the correctness requirement of the underlying software becomes especially critical. However, the increasing complexities and sizes of modern software systems pose special challenges on the effectiveness as well as efficiency of software verification. Two major obstacles include the quality of test generation in terms of error detection in software testing and the state space explosion problem in software formal verification (model checking). In this dissertation, we investigate several hybrid techniques that explore dynamic (with program execution), static (without program execution) as well as the synergies of multiple approaches in software verification from the perspectives of testing and model checking. For software testing, a new simulation-based internal variable range coverage metric is proposed with the goal of enhancing the error detection capability of the generated test data when applied as the target metric. For software model checking, we utilize various dynamic analysis methods, such as data mining, swarm intelligence (ant colony optimization), to extract useful high-level information from program execution data. Despite being incomplete, dynamic program execution can still help to uncover important program structure features and variable correlations. The extracted knowledge, such as invariants in different forms, promising control flows, etc., is then used to facilitate code-level program abstraction (under-approximation/over-approximation), and/or state space partition, which in turn improve the performance of property verification. In order to validate the effectiveness of the proposed hybrid approaches, a wide range of experiments on academic and real-world programs were designed and conducted, with results compared against the original as well as the relevant verification methods. Experimental results demonstrated the effectiveness of our methods in improving the quality as well as performance of software verification. For software testing, the newly proposed coverage metric constructed based on dynamic program execution data is able to improve the quality of test cases generated in terms of mutation killing — a widely applied measurement for error detection. For software model checking, the proposed hybrid techniques greatly take advantage of the complementary benefits from both dynamic and static approaches: the lightweight dynamic techniques provide flexibility in extracting valuable high-level information that can be used to guide the scope and the direction of static reasoning process. It consequently results in significant performance improvement in software model checking. On the other hand, the static techniques guarantee the completeness of the verification results, compensating the weakness of dynamic methods. / Ph. D.

Integrated circuits, from general purpose microprocessors to application specific designs (ASICs), have become ubiquitous in modern technology. As our applications have become more complex, so too have the circuits used to drive them. Moore's law predicts that the number of transistors on a chip doubles every 18-24 months. This explosion in circuit size has also lead to significant growth in testing effort required to verify the design. In order to cope with the required effort, the testing problem must be approached from several different design levels. In particular, exploiting the Register Transfer Level for test generation allows for the use of relational information unavailable at the structural level. This dissertation demonstrates several novel methods for generating tests applicable for both structural and functional tests. These testing methods allow for significantly faster test generation for functional tests as well as providing high levels of fault coverage during structural test, typically outperforming previous state of the art methods. First, a semi-formal method for functional verification is presented. The approach utilizes a SMT-based bounded model checker in combination with an ant colony optimization based search engine to generate tests with high branch coverage. Additionally, the method is utilized to identify unreachable code paths within the RTL. Compared to previous methods, the experimental results show increased levels of coverage and improved performance. Then, an ant colony optimization algorithm is used to generate high quality tests for fault coverage. By utilizing co-simulation at the RTL and gate level, tests are generated for both levels simultaneously. This method is shown to reach previously unseen levels of fault coverage with significantly lower computational effort. Additionally, the engine was also shown to be effective for behavioral level test generation. Next, an abstraction method for functional test generation is presented utilizing program slicing and data mining. The abstraction allows us to generate high quality test vectors that navigate extremely narrow paths in the state space. The method reaches previously unseen levels of coverage and is able to justify very difficult to reach control states within the circuit. Then, a new method of fault grading test vectors is introduced based on the concept of operator coverage. Operator coverage measures the behavioral coverage in each synthesizable statement in the RTL by creating a set of coverage points for each arithmetic and logical operator. The metric shows a strong relationship with fault coverage for coverage forecasting and vector comparison. Additionally, it provides significant reductions in computation time compared to other vector grading methods. Finally, the prior metric is utilized for creating a framework of automatic test pattern generation for defect coverage at the RTL. This framework provides the unique ability to automatically generate high quality test vectors for functional and defect level testing at the RTL without the need for synthesis. In summary, We present a set of tools for the analysis and test of circuits at the RTL. By leveraging information available at HDL, we can generate tests to exercise particular properties that are extremely difficult to extract at the gate level. / Ph. D.

Fire ants link their legs and jaws together to form functional structures called self- assemblages. Examples include floating rafts, towers, bridges, and bivouacs. We investigate these self-assemblages of fire ants. Our studies are motivated in part by the vision of providing guidance for programmable robot swarms. The goal for such systems is to develop a simple programmable element from which complex patterns or behaviors emerge on the collective level. Intelligence is decentralized, as is the case with social insects such as fire ants. In this combined experimental and theoretical study, we investigate the construction of two fire ant self-assemblages that are critical to the colony’s survival: the raft and the tower. Using time-lapse photography, we record the construction processes of rafts and towers in the laboratory. We identify and characterize individual ant behaviors that we consistently observe during assembly, and incorporate these behaviors into mathematical models of the assembly process. Our models accurately predict both the assemblages’ shapes and growth patterns, thus providing evidence that we have identified and analyzed the key mechanisms for these fire ant self-assemblages. We also develop novel techniques using scanning electron microscopy and micro-computed tomography scans to visualize and quantify the internal structure and packing properties of live linked fire ants. We compare our findings to packings of dead ants and similarly shaped granular material packings to understand how active arranging affects ant spacing and orientation. We find that ants use their legs to increase neighbor spacing and hence reduce their packing density by one-third compared to packings of dead ants. Also, we find that live ants do not align themselves in parallel with nearest neighbors as much as dead ants passively do. Our main contribution is the development of parsimonious mathematical models of how the behaviors of individuals result in the collective construction of fire ant assemblages. The models posit only simple observed behaviors based on local information, yet their mathe- matical analysis yields accurate predictions of assemblage shapes and construction rates for a wide range of ant colony sizes.

In swarm robotics, the control of a group of robots is often fully distributed and does not rely on any leader. In this thesis, we are interested in understanding how to design collective decision making processes in such groups. Our approach consists in taking inspiration from nature, and especially from self organization in social insects, in order to produce effective collective behaviors in robot swarms. We have devised four robotics experiments that allow us to study multiple facets of collective decision making. The problems on which we focus include cooperative transport of objects, robot localization, resource selection, and resource discrimination. <p><p>We study how information is transferred inside the groups, how collective decisions arise, and through which particular interactions. Important properties of the groups such as scalability, robustness, and adaptivity are also investigated. We show that collective decisions in robot swarms can effectively arise thanks to simple mechanisms of imitation and amplification. We experimentally demonstrate their implementation with direct or indirect information transfer, and with robots that can distinguish the available options partially or not at all. / Doctorat en Sciences de l'ingénieur / info:eu-repo/semantics/nonPublished

We investigate the use of self-assembly in a robotic system as a means of responding<p>to different environmental contingencies. Self-assembly is the mechanism through which<p>agents in a multi-robot system autonomously form connections with one another to create<p>larger composite robotic entities. Initially, we consider a simple response mechanism<p>that uses stochastic self-assembly without any explicit control over the resulting morphology<p> / Doctorat en Sciences de l'ingénieur / info:eu-repo/semantics/nonPublished

In this thesis, we investigate the problem of path formation and prey retrieval in a swarm of robots. We present two swarm intelligence control mechanisms used for distributed robot path formation. In the first, the robots form linear chains. We study three variants of robot chains, which vary in the degree of motion allowed<p>to the chain structure. The second mechanism is called vectorfield. In this case,<p>the robots form a pattern that globally indicates the direction towards a goal or<p>home location. Both algorithms were designed following the swarm robotics control<p>principles: simplicity of control, locality of sensing and communication, homogeneity<p>and distributedness.<p><p>We test each controller on a task that consists in forming a path between two<p>objects—the prey and the nest—and to retrieve the prey to the nest. The difficulty<p>of the task is given by four constraints. First, the prey requires concurrent, physical<p>handling by multiple robots to be moved. Second, each robot’s perceptual range<p>is small when compared to the distance between the nest and the prey; moreover,<p>perception is unreliable. Third, no robot has any explicit knowledge about the<p>environment beyond its perceptual range. Fourth, communication among robots is<p>unreliable and limited to a small set of simple signals that are locally broadcast.<p><p>In simulation experiments we test our controllers under a wide range of conditions,<p>changing the distance between nest and prey, varying the number of robots<p>used, and introducing different obstacle configurations in the environment. Furthermore,<p>we tested the controllers for robustness by adding noise to the different sensors,<p>and for fault tolerance by completely removing a sensor or actuator. We validate the<p>chain controller in experiments with up to twelve physical robots. We believe that<p>these experiments are among the most sophisticated examples of self-organisation<p>in robotics to date. / Doctorat en Sciences de l'ingénieur / info:eu-repo/semantics/nonPublished

In this thesis, we propose an approach to achieve autonomous task partitioning in swarms of robots. Task partitioning is the process by which tasks are decomposed into sub-tasks and it is often an advantageous way of organizing work in groups of individuals. Therefore, it is interesting to study its application to swarm robotics, in which groups of robots are deployed to collectively carry out a mission. The capability of partitioning tasks autonomously can enhance the flexibility of swarm robotics systems because the robots can adapt the way they decompose and perform their work depending on specific environmental conditions and goals. So far, few studies have been presented on the topic of task partitioning in the context of swarm robotics. Additionally, in all the existing studies, there is no separation between the task partitioning methods and the behavior of the robots and often task partitioning relies on characteristics of the environments in which the robots operate.<p>This limits the applicability of these methods to the specific contexts for which they have been built. The work presented in this thesis represents the first steps towards a general framework for autonomous task partitioning in swarms of robots. We study task partitioning in foraging, since foraging abstracts practical real-world problems. The approach we propose in this thesis is therefore studied in experiments in which the goal is to achieve autonomous task partitioning in foraging. However, in the proposed approach, the task partitioning process relies upon general, task-independent concepts and we are therefore confident that it is applicable in other contexts. We identify two main capabilities that the robots should have: i) being capable of selecting whether to employ task partitioning and ii) defining the sub-tasks of a given task. We propose and study algorithms that endow a swarm of robots with these capabilities. / Doctorat en Sciences de l'ingénieur / info:eu-repo/semantics/nonPublished

In this thesis, we examine algorithms for the division of labour in a group of robot. The algorithms make no use of direct communication. Instead, they are based only on the interactions among the robots and between the group and the environment.<p><p>Division of labour is the mechanism that decides how many robots shall be used to perform a task. The efficiency of the group of robots depends in fact on the number of robots involved in a task. If too few robots are used to achieve a task, they might not be successful or might perform poorly. If too many robots are used, it might be a waste of resources. The number of robots to use might be decided a priori by the system designer. More interestingly, the group of robots might autonomously select how many and which robots to use. In this thesis, we study algorithms of the latter type.<p><p>The robotic literature offers already some solutions, but most of them use a form of direct communication between agents. Direct, or explicit, communication between the robots is usually considered a necessary condition for co-ordination. Recent studies have questioned this assumption. The claim is based on observations of animal colonies, e.g. ants and termites. They can effectively co-operate without directly communicating, but using indirect forms of communication like stigmergy. Because they do not rely on communication, such colonies show robust behaviours at group level, a condition that one wishes also for groups of robots. Algorithms for robot co-ordination without direct communication have been proposed in the last few years. They are interesting not only because they are a stimulating intellectual challenge, but also because they address a situation that might likely occur when using robots for real-world out-door applications. Unfortunately, they are still poorly studied.<p><p>This thesis helps the understanding and the development of such algorithms. We start from a specific case to learn its characteristics. Then we improve our understandings through comparisons with other solutions, and finally we port everything into another domain.<p><p>We first study an algorithm for division of labour that was inspired by ants' foraging. We test the algorithm in an application similar to ants' foraging: prey retrieval. We prove that the model used for ants' foraging can be effective also in real conditions. Our analysis allows us to understand the underlying mechanisms of the division of labour and to define some way of measuring it.<p><p>Using this knowledge, we continue by comparing the ant-inspired algorithm with similar solutions that can be found in the literature and by assessing their differences. In performing these comparisons, we take care of using a formal methodology that allows us to spare resources. Namely, we use concepts of experiment design to reduce the number of experiments with real robots, without losing significance in the results.<p><p>Finally, we apply and port what we previously learnt into another application: Sensor/Actor Networks (SANETs). We develop an architecture for division of labour that is based on the same mechanisms as the ants' foraging model. Although the individuals in the SANET can communicate, the communication channel might be overloaded. Therefore, the agents of a SANET shall be able to co-ordinate without accessing the communication channel. / Doctorat en sciences appliquées / info:eu-repo/semantics/nonPublished

A swarm intelligence system is a type of multiagent system with the following distinctive characteristics: (i) it is composed of a large number of agents, (ii) the agents that comprise the system are simple with respect to the complexity of the task the system is required to perform, (iii) its control relies on principles of decentralization and self-organization, and (iv) its constituent agents interact locally with one another and with their environment. <p><p>Interactions among agents, either direct or indirect through the environment in which they act, are fundamental for swarm intelligence to exist; however, there is a class of interactions, referred to as "interference", that actually blocks or hinders the agents' goal-seeking behavior. For example, competition for space may reduce the mobility of robots in a swarm robotics system, or misleading information may spread through the system in a particle swarm optimization algorithm. One of the most visible effects of interference in a swarm intelligence system is the reduction of its efficiency. In other words, interference increases the time required by the system to reach a desired state. Thus, interference is a fundamental problem which negatively affects the viability of the swarm intelligence approach for solving important, practical problems.<p><p>We propose a framework called "incremental social learning" (ISL) as a solution to the aforementioned problem. It consists of two elements: (i) a growing population of agents, and (ii) a social learning mechanism. Initially, a system under the control of ISL consists of a small population of agents. These agents interact with one another and with their environment for some time before new agents are added to the system according to a predefined schedule. When a new agent is about to be added, it learns socially from a subset of the agents that have been part of the system for some time, and that, as a consequence, may have gathered useful information. The implementation of the social learning mechanism is application-dependent, but the goal is to transfer knowledge from a set of experienced agents that are already in the environment to the newly added agent. The process continues until one of the following criteria is met: (i) the maximum number of agents is reached, (ii) the assigned task is finished, or (iii) the system performs as desired. Starting with a small number of agents reduces interference because it reduces the number of interactions within the system, and thus, fast progress toward the desired state may be achieved. By learning socially, newly added agents acquire knowledge about their environment without incurring the costs of acquiring that knowledge individually. As a result, ISL can make a swarm intelligence system reach a desired state more rapidly. <p><p>We have successfully applied ISL to two very different swarm intelligence systems. We applied ISL to particle swarm optimization algorithms. The results of this study demonstrate that ISL substantially improves the performance of these kinds of algorithms. In fact, two of the resulting algorithms are competitive with state-of-the-art algorithms in the field. The second system to which we applied ISL exploits a collective decision-making mechanism based on an opinion formation model. This mechanism is also one of the original contributions presented in this dissertation. A swarm robotics system under the control of the proposed mechanism allows robots to choose from a set of two actions the action that is fastest to execute. In this case, when only a small proportion of the swarm is able to concurrently execute the alternative actions, ISL substantially improves the system's performance. / Doctorat en Sciences de l'ingénieur / info:eu-repo/semantics/nonPublished