Metamorphic robots have gained the attention of many researchers due to their ability to change shape and adapt to various tasks. In order to utilize the versatility of metamorphic systems, we need to be able to find a shape-shifting (reconfiguration) plan efficiently; however, finding these plans is challenging due to the high degree of freedom of modular systems. Reconfiguration algorithms proposed so far either scale poorly with a growing number of modules, impose specific restrictions on modules, or produce plans that are unrealistic outside of zero-gravity environments. This paper presents a new approach to the reconfiguration problem of chain-type metamorphic robots. Our algorithm relies on forming tentacles and using them to transport modules, which allows us to search through a reduced state space by computing many smaller planning instances. As a result, we obtain a heuristic solution that is more scalable than optimal planners, while producing realistic plans that impose no specific module requirements.

We present a new approach to tackle the problem of metamorphic robots' reconfiguration. Given the chain-type metamorphic robot's initial and target configuration, we compute a reconfiguration plan that is provably physically collision-free. Our solution employs a specific heuristic. The robot initially reconfigures to a shape that resembles an octopus with many tentacles. After that, the tentacles gradually reconnect to each other using inverse kinematics, separating one tentacle from the body and keeping the other one connected. This strategy eventually leads to a snake-like structure of the robot. For the target configuration, we compute the reconfiguration plan with the same procedure, however, we reverse the plan to reconfigure the robot from the snake-like structure to the target shape. According to our experimental evaluation, our newly introduced strategy for finding reconfiguration plans is successful. It efficiently finds collision-free plans even for robots consisting of hundreds of modules.

We present a new approach to tackle the problem of lattice-type metamorphic robots reconfiguration. We base our approach on a reduction to satisfiability modulo theory (SMT). Unlike the current state-of-the-art solutions, we consider the spatial limitations of the modules themselves and produce collision-free plans. We give an in-depth description of the reduction and discuss several optimizations for our technique. We also show an experimental evaluation of our approach and list possible future improvements to our technique.

In this paper, we present a combination of existing and new tools that together make it possible to apply formal verification methods to programs in the form of ×86_64 machine code. Our approach first uses a decompilation tool (remill) to extract low-level intermediate representation (LLVM) from the machine code. This step consists of instruction translation (i.e. recovery of operation semantics), control flow extraction and address identification.The main contribution of this paper is the second step, which builds on data flow analysis and refinement of indirect (i.e. data-dependent) control flow. This step makes the processed bitcode much more amenable to formal analysis.To demonstrate the viability of our approach, we have compiled a set of benchmark programs into native executables and analysed them using two LLVM-based tools: DIVINE, a software model checker and KLEE, a symbolic execution engine. We have compared the outcomes to direct analysis of the same programs.

We present RoFICoM, a new retractable connection device that allows for mechanical, electric, and data communication connection between separable robotic modules. The device is intentionally designed to be used in lattice-type metamorphic robots, however, its applicability is much wider. The main novelty of our solution lies primarily in a new unique flat design and spatial compactness of the connector. With a flat connector, much more space is left for the body of a robotic module in the structure. Moreover, the connector is also fully self-contained device with well defined mechanical, electrical and data interfaces, hence it can be easily embedded in various robotic solutions. Our RoFICoM connector is easy to produce, it is open-hardware and free for non-commercial use. In the paper, we give construction details and report on a couple of experiments we performed to demonstrate key features of the connection achieved with two RoFICoM devices.

DIVINE is an LLVM -based verification tool focusing on analysis of real-world C and C++ programs. Such programs often interact with their environment, for example via inputs from users or network. When these programs are analyzed, it is desirable that the verification tool can deal with inputs symbolically and analyze runs for all inputs. In DIVINE , it is now possible to deal with input data via symbolic computation instrumented into the original program at the level of LLVM bitcode. Such an instrumented program maintains symbolic values internally and operates directly on them. Instrumentation allows us to enhance the tool with support for symbolic data without substantial modifications of the tool itself. Namely, this competition contribution uses SMT formulae for representation of input data.

An important step toward adoption of formal methods in software development is support for mainstream programming languages. Unfortunately, these languages are often rather complex and come with substantial standard libraries. However, by choosing a suitable intermediate language, most of the complexity can be delegated to existing execution-oriented (as opposed to verification-oriented) compiler frontends and standard library implementations. In this paper, we describe how support for C++ exceptions can take advantage of the same principle. Our work is based on DiVM, an LLVM-derived, verification-friendly intermediate language. Our implementation consists of 2 parts: an implementation of the 'libunwind' platform API which is linked to the program under test and consists of 9 C functions. The other part is a preprocessor for LLVM bitcode which prepares exception-related metadata and replaces associated special-purpose LLVM instructions.

In various areas of computer science, the problem of dealing with a set of constraints arises. If the set of constraints is unsatisfiable, one may ask for a minimal description of the reason for this unsatisifiability. Minimal unsatisfiable subsets (MUSes) and maximal satisfiable subsets (MSSes) are two kinds of such minimal descriptions. The goal of this work is the enumeration of MUSes and MSSes for a given constraint system. As such full enumeration may be intractable in general, we focus on building an online algorithm, which produces MUSes/MSSes in an on-the-fly manner as soon as they are discovered. The problem has been studied before even in its online version. However, our algorithm uses a novel approach that is able to outperform the current state-of-the art algorithms for online MUS/MSS enumeration. Moreover, the performance of our algorithm can be adjusted using tunable parameters. We evaluate the algorithm on a set of benchmarks.

Abstract In the last decade it became a common practice to formalise software requirements to improve the clarity of users’ expectations. In this work we build on the fact that functional requirements can be expressed in temporal logic and we propose new sanity checking techniques that automatically detect flaws and suggest improvements of given requirements. Specifically, we describe and experimentally evaluate approaches to consistency and redundancy checking that identify all inconsistencies and pinpoint their exact source (the smallest inconsistent set). We further report on the experience obtained from employing the consistency and redundancy checking in an industrial environment. To complete the sanity checking we also describe a semi-automatic completeness evaluation that can assess the coverage of user requirements and suggest missing properties the user might have wanted to formulate. The usefulness of our completeness evaluation is demonstrated in a case study of an aeroplane control system.

Automatic verification of programs and computer systems with data nondeterminism (e.g., reading from user input) represents a significant and well-motivated challenge. The case of parallel programs is especially difficult, because then also the control flow nontrivially complicates the verification process. We apply the techniques of explicit-state model checking to account for the control aspects of a program to be verified and use set-based reduction of the data flow, thus handling the two sources of nondeterminism separately. We build the theory of set-based reduction using first-order formulae in the bit-vector theory to encode the sets of variable evaluations representing program data. These representations are tested for emptiness and equality (state matching) during the verification, and we harness modern satisfiability modulo theory solvers to implement these tests. We design two methods of implementing the state matching, one using quantifiers and one that is quantifier-free, and we provide both analytical and experimental comparisons. Further experiments evaluate the efficiency of the set-based reduction method, showing the classical, explicit approach to fail to scale with the size of data domains. Finally, we propose and evaluate two heuristics to decrease the number of expensive satisfiability queries, together yielding a 10-fold speedup.

Verification of parallel programs with input variables represents a significant and well-motivated challenge. This paper addresses the challenge with a verification method that combines explicit and symbolic approaches to the state space representation. The state matching between non-canonical representations proved to be the bottleneck of such a combination, since its computation entailed deciding satisfiability of quantified bit-vector formulae. This limitation is here addressed by an alternative state matching, based on quantifier-free satisfiability, and a heuristics optimising the state space searching. The experimental evaluation shows that the alternative state matching causes only a minor increase in the number of states and that, in combination with the heuristics, it considerably extends the scope of applicability of the proposed LTL model checking.

Verification of embedded systems has become increasingly important in many industrial domains. Safety-critical embedded systems, such as those developed in aerospace industry, are regularly subject to automated formal verification process. In this paper we extend our tool integration chain of parallel, explicit-state LTL model checker DIVINE and Matlab Simulink tool suit with an improved support of counterexample simulation. In particular, we show how to provide the verification engineer with a direct connection between the error discovered by the model checker and the simulation in Matlab Simulink. This work has been conducted within the Artemis project industrial Framework for Embedded Systems Tools (iFEST).

An important problem in current computational systems biology is to analyze models of biological systems dynamics under parameter uncertainty. This paper presents a novel algorithm for parameter synthesis based on parallel model checking. The algorithm is conceptually universal with respect to the modeling approach employed. We introduce the algorithm, show its scalability, and examine its applicability on several biological models.

The problem of decomposing a directed graph into its strongly connected components is a fundamental graph problem inherently present in many scientific and commercial applications. In this paper we show how some of the existing parallel algorithms can be reformulated in order to be accelerated by NVIDIA CUDA technology. In particular, we design a new CUDA-aware procedure for pivot selection and we adapt selected parallel algorithms for CUDA accelerated computation. We also experimentally demonstrate that with a single GTX 480 GPU card we can easily outperform the optimal serial CPU implementation by an order of magnitude in most cases, 40 times on some sufficiently big instances. This is an interesting result as unlike the serial CPU case, the asymptotic complexity of the parallel algorithms is not optimal.

We study existing parallel algorithms for the decomposition of a partitioned graph into its strongly connected components (SCCs). In particular, we identify several individual procedures that the algorithms are assembled from and show how to assemble a new and more efficient algorithm, called Recursive OBF (OBFR), to solve the decomposition problem. We also report on a thorough experimental study to evaluate the new algorithm. It shows that it is possible to perform SCC decomposition in parallel efficiently and that OBFR, if properly implemented, is the best choice in most cases.

Recently, the CUDA technology has been used to accelerate many computation demanding tasks. For example, in our previous work we have shown how CUDA technology can be employed to accelerate the process of Linear Temporal Logic (LTL) Model Checking. While the raw computing power of a CUDA enabled device is tremendous, the applicability of the technology is quite often limited to small or middle-sized instances of the problems being solved. This is because the memory that a single device is equipped with, is simply not large enough to cope with large or realistic instances of the problem, which is also the case of our CUDA-aware LTL Model Checking solution. In this paper we suggest how to overcome this limitations by employing multiple (two in our case) CUDA devices for acceleration of our fine-grained communication-intensive parallel algorithm for LTL Model Checking.

Partial order reduction and distributed-memory processing are the two essential techniques to fight the well-known state space explosion problem in explicit state model checking. Unfortunately, these two techniques have not been integrated yet to a satisfactory degree. While for verification of safety properties, there are a few rather successful approaches to parallel partial order reduction, for LTL model checking all suggested approaches are either too technically involved to be smoothly incorporated with the existing parallel algorithms, or they are simply weak in the sense that the achieved reduction in the size of the state space is minor. The main source of difficulties is the cycle proviso that requires one fully expanded state on every cycle in the reduced state space graph. This can be easily achieved in the sequential case by employing depth-first search strategy for state space generation. Unfortunately, this strategy is incompatible with parallel (hence distributed-memory) processing, which limits application of partial order reduction technique to the sequential case. In this paper we suggest a new technique that guarantees correct construction of the reduced state space graph w.r.t. the cycle proviso. Our new technique is fully compatible with the parallel graph traversal procedure while at the same time it provides competitive reduction of the state space if compared to the serial case. The new technique has been implemented within the parallel and distributed-memory LTL model checker DiVinE and its performance is reported in this paper.

The current interest in systems biology is to gain a better understanding of how the complex dynamic behaviour of the cell emerges from mutual interactions of molecular species. When solving such a nontrivial goal, biological data have to be necessarily integrated with mathematical modelling and computer analysis. Since the key aspect of biological modelling is based on unifying several kinds of data captured in terms of large-scale biological networks, scalable and automatized methods are necessary to obtain novel predictions and understanding. In this review, we provide a brief description of the tool DiVinE adapted for automatized analysis of biological systems dynamics. The tool employs high-performance computing techniques to enable analysis of large models.

Recent technological developments made available various many-core hardware platforms. For example, a SIMD-like hardware architecture became easily accessible for many users who have their computers equipped with modern NVIDIA GPU cards with CUDA technology. In this paper we redesign the maximal accepting predecessors algorithm [7] for LTL model checking in terms of matrix-vector product in order to accelerate LTL model checking on many-core GPU platforms. Our experiments demonstrate that using the NVIDIA CUDA technology results in a significant speedup of verification process.

Model checking is a popular technique to systematically and automatically verify system properties. Unfortunately, the well-known state explosion problem often limits the extent to which it can be applied to realistic specifications, due to the huge resulting memory requirements. Distributed-memory model checkers exist, but have thus far only been evaluated on small-scale clusters, with mixed results. We examine one well-known distributed model checker, DiVinE, in detail, and show how a number of additional optimizations in its runtime system enable it to efficiently check very demanding problem instances on a large-scale, multi-core compute cluster. We analyze the impact of the distributed algorithms employed, the problem instance characteristics and network overhead. Finally, we show that the model checker can even obtain good performance in a high-bandwidth computational grid environment.

I/O-efficient algorithms take the advantage of large capacities of external memories to verify huge state spaces even on a single machine with low-capacity RAM. On the other hand, parallel algorithms are used to accelerate the computation and their usage may significantly increase the amount of available RAM memory if clusters of computers are involved. Since both the large amount of memory and high speed computation are desired in verification of large-scale industrial systems, extending I/O-efficient model checking to work over a network of computers can bring substantial benefits. In this paper we propose an explicit state cluster-based I/O efficient LTL model checking algorithm that is capable to verify systems with approximately $10^{10}$ states within hours.

In this paper we summarize parallel algorithms for enumerative model checking of properties formulated in linear time temporal logic (LTL) as well as a fragment of the \mu- calculus which naturally subsumes the branching time logic CTL (computation tree logic). We also indicate how to provide parallel model checking applications as services for integrated modelling, analysis, and verification using the FMICS-jETI platform.

We propose a practical parallel on-the-fly algorithm for enumerative LTL (linear temporal logic) model checking. The algorithm is designed for a cluster of workstations communicating via MPI (message passing interface). The detection of cycles (faulty runs) effectively employs the so called back-level edges. In particular, a parallel level-synchronized breadth-first search of the graph is performed to discover back-level edges. For each level, the back-level edges are checked in parallel by a nested depth-first search to confirm or refute the presence of a cycle. Several optimizations of the basic algorithm are presented and advantages and drawbacks of their application to distributed LTL model-checking are discussed. Experimental implementation of the algorithm shows promising results.