Narrow Results

We consider in this paper systems modeled by timed automata. The timing bounds involved in the action guards and location invariants of our timed automata are not constants, but parameters. Those parametric timed automata allow the modelling of various kinds of timed systems, e.g. communication protocols or asynchronous circuits. We will also assume that we are given an initial tuple π₀ of values for the parameters, which corresponds to values for which the system is known to behave properly. Our goal is to compute a constraint K₀ on the parameters, satisfied by π₀, guaranteeing that, under any parameter valuation satisfying K₀, the system behaves in the same manner: for any two parameter valuations satisfying K₀, the behaviors of the timed automata are (time-abstract) equivalent, i.e., the traces of execution viewed as alternating sequences of actions and locations are identical. We present an algorithm InverseMethod that terminates in the case of acyclic models, and discuss how to extend it to the cyclic case. We also explain how to combine our method with classical synthesis methods which are based on the avoidance of a given set of bad states. A prototype implementation has been done, and various experiments are described.

This paper deals with the problem of distributed causal model-based diagnosis on interacting Behavioral Petri Nets (BPNs). The system to be diagnosed comprises different interacting subsystems (each modeled as a BPN) and the diagnostic system is defined as a multi-agent system where each agent is designed to diagnose a particular subsystem on the basis of its local model, the local received observation and the information exchanged with the neighboring agents. The interactions between subsystems are captured by tokens that may pass from one net model to another via bordered places. The diagnostic reasoning scheme is accomplished locally within each agent by analyzing the P-invariants of the corresponding BPN model. Once local diagnoses are obtained, agents begin to communicate to ensure that such diagnoses are consistent and recover completely the results obtained by a centralized agent having a global view about the whole system.

A Self modifying code is code that modifies its own instructions during execution time. It is nowadays widely used, especially in malware to make the code hard to analyse and to detect by anti-viruses. Thus, the analysis of such self modifying programs is a big challenge. Pushdown systems (PDSs) is a natural model that is extensively used for the analysis of sequential programs because they allow to accurately model procedure calls and mimic the program’s stack. In this work, we propose to extend the PushDown System model with self-modifying rules. We call the new model Self-Modifying PushDown System (SM-PDS). A SM-PDS is a PDS that can modify its own set of transitions during execution. We show how SM-PDSs can be used to naturally represent self-modifying programs and provide efficient algorithms to compute the backward and forward reachable configurations of SM-PDSs. We implemented our techniques in a tool and obtained encouraging results. In particular, we successfully applied our tool for the detection of self-modifying malware.

Multiway Decision Graphs (MDGs) have recently been proposed as an efficient representation for RTL designs. In this paper, we illustrate the MDG-based formal verification technique on the example of the Island Tunnel Controller. We investigate several techniques on how to deal with the nontermination problem of abstract state exploration, including a novel method based on retiming and circuit transformation. We provide comparative experimental results for the verification of a number of properties for the example using two well-known ROBDD-based verification tools, namely, SMV (Symbolic Model Verifier) and VIS (Verification Interacting with Synthesis), and we show the strength of the MDG approach to handling arbitrary data widths.

This paper proposes a symbolic reachability analysis method for multiple-clock system design, which is the first approach to deal with both synchronization problems caused by metastability and rate mismatch problems caused by clock frequency mismatches in a single framework. Three methods are described to reproduce problems that occur with multiple-clock system design during reachability analysis: (1) alternate evaluation for a system with two clocks as the base-line model, (2) nondeterministic delayed evaluation to reproduce a synchronization problem, and (3) double evaluation to reproduce a clock frequency mismatch. Experimental results on ISCAS 89 benchmark show an improvement factor of average CPU time as compared to Clarke's method by 1.29, 55.41, 2.19 and 45.23 times when alternate evaluation, double evaluation, alternate evaluation with NDDE and double evaluation with NDDE is applied, respectively.

Stochastic Shortest Path problems (SSPs) can be efficiently dealt with by the Real-Time Dynamic Programming algorithm (RTDP). Yet, RTDP requires that a goal state is always reachable. This article presents an algorithm checking for goal reachability, especially in the complex case of an uncertain SSP where only a possible interval is known for each transition probability. This gives an analysis method for determining if SSP algorithms such as RTDP are applicable, even if the exact model is not known. As this is a time-consuming algorithm, we also present a simple process that often speeds it up dramatically. Yet, the main improvement still needed is to turn to a symbolic analysis in order to avoid a complete state-space enumeration.

Studies have shown that rehabilitation training with the unaffected side guiding affected side is more consistent with the natural movement pattern of human upper limb compared with unilateral rehabilitation training, which is conducive to improve rehabilitation effect of the affected limb motor function. In this paper, a bilateral end-effector upper limb rehabilitation robot (BEULRR) based on two modern commercial manipulators is developed first, then the kinematics, reachability, and dexterity analysis of BEULRR are performed, respectively. Finally, a bilateral symmetric training protocol with the unaffected side guiding the affected side is proposed and evaluated through healthy human subject experiment testing based on BEULRR. The simulation results show that the developed BEULRR could perform spatial rehabilitation training and its rehabilitation training workspace can fully cover the physiological workspace of human upper limb. The preliminary experiment results from the healthy human subject show that the BEULRR system could provide reliable bilateral symmetric training protocol. These simulation and experiment results demonstrated that the developed BEULRR system could be used in bilateral rehabilitation training application, and also show that the BEULRR system has the potential to be applied to clinical rehabilitation training in the further step. In the close future, the proposed BEULRR and bilateral symmetric training protocol are planned to be applied in elderly volunteers and patients with upper limb motor dysfunction for further evaluating.

Grasping can be seen as two steps: placing the hand at a grasping pose and closing the fingers. In this paper, we introduce an efficient algorithm for grasping pose generation. By the use of preshaping and eigen-grasping actions, the dimension of the space of possible hand configurations is reduced. The object to be grasped is decomposed into boxes of a discrete set of different sizes. By performing finger reachability analysis on the boxes, the kinematic feasibility of a grasp can be determined. If a reachable grasp is force-closure and can be performed by the robotic arm, its grasping forces are optimized and can be executed. The novelty of our algorithm is that it takes into account both the object geometrical information and the kinematic information of the hand to determine the grasping pose, so that a reachable grasping pose can be found very quickly. Real experiments with two different robotic hands show the efficiency and feasibility of our method.

In this work we show how precomputed reachability information can be used to efficiently solve complex inverse kinematics (IK) problems such as bimanual grasping or re-grasping for humanoid robots. We present an integrated approach which generates collision-free IK solutions in cluttered environments while handling multiple potential grasping configurations for an object. Therefore, the spatial reachability of the robot's workspace is efficiently encoded by discretized data structures and sampling-based techniques are used to handle arbitrary kinematic chains. The algorithms are employed for single-handed and bimanual grasping tasks with fixed robot base position and methods are developed that allow to efficiently incorporate the search for suitable robot locations. The approach is evaluated in different scenarios with the humanoid robot ARMAR-III.

In this study, applicability of verification and correct-by-design hybrid systems modeling and reachability-based controllers for vehicular automation are investigated. Two perspectives in hybrid systems modeling will be introduced, and then reachability analysis techniques will be developed to compute exact reachable sets from a specified unsafe set. Using level set methods, a Hamilton–Jacobi–Isaacs equation is derived whose solutions describe the boundaries of the finite time backward reachable set, which will be manipulated to design a safe controller that guarantees the safety of a given system. An automated longitudinal controller with a fully integrated collision avoidance functionality will be designed as a hybrid system and validated through simulations with a number of different scenarios in order to illustrate the potential of verification methods in automated vehicles.