1,721,028 research outputs found
A Contract-Based Requirement Engineering Framework for the Design of Industrial Cyber-Physical Systems
Full text linkThis work-in-progress paper presents our current effort toward the development of compositional modeling formalisms and scalable algorithms for high-assurance design of industrial cyber-physical systems, with emphasis on smart manufacturing systems. A require-ment engineering methodology is implemented within CHASE, a software framework supporting contract-based representations of systems and components to facilitate analysis and design space exploration. We provide an overview of CHASE and discuss its application to the design of a robotic arm. This paper is accompanied by a poster describing the architecture of CHASE and a demonstration of its application to the case study
Quantitative Verification and Design Space Exploration under Uncertainty with Parametric Stochastic Contracts
No full textThis paper proposes an automated framework for quantitative verification and design space exploration of cyber-physical systems in the presence of uncertainty, leveraging assume-guarantee contracts expressed in Stochastic Signal Temporal Logic (StSTL). We introduce quantitative semantics for StSTL and formulations of the quantitative verification and design space exploration problems as bi-level optimization problems. We show that these optimization problems can be effectively solved for a class of stochastic systems and a fragment of bounded-time StSTL formulas. Our algorithm searches for partitions of the upper-level design space such that the solutions of the lower-level problems satisfy the upper-level constraints. A set of optimal parameter values are then selected within these partitions. We illustrate the effectiveness of our framework on the design of a multi-sensor perception system and an automatic cruise control system
Task Assignment, Scheduling, and Motion Planning for Automated Warehouses for Million Product Workloads
Full text linkWe address the Warehouse Servicing Problem (WSP) in automated warehouses, which use teams of mobile robots to move products from shelves to packaging stations. Given a list of products, the WSP amounts to finding a motion plan which brings every product on the list from a shelf to a packaging station within a given time limit. The WSP consists of four subproblems, namely, deciding where to source and deposit a product (task formulation), who should transport each product (task assignment) and when (scheduling) and how (motion planning). These problems are NP-Hard individually and made more challenging by their interdependence. The difficulty of the WSP is compounded by the scale of automated warehouses, which use teams of hundreds of agents to transport thousands of products. In this paper, we present Contract-based Cyclic Motion Planning (CCMP), a novel contract-based methodology for solving the WSP at scale. CCMP decomposes a warehouse into a set of traffic system components. By assigning each component a contract which describes the traffic flows it can support, CCMP can generate a traffic flow which satisfies a given WSP instance. CCMP then uses a novel motion planner to transform this traffic flow into a motion plan for a team of robots. Evaluation shows that CCMP can solve WSP instances taken from real industrial scenarios with up to 1 million products while outperforming other methodologies for solving the WSP by up to 2.9x
Efficient Exploration of Cyber-Physical System Architectures Using Contracts and Subgraph Isomorphism
Full text linkWe present ContrArc, a methodology for the exploration of cyber-physical system architectures aiming to minimize a cost function while adhering to a set of heterogeneous constraints. We assume a system topology, defined as a graph, where components (nodes) are selected from an implementation library, and connections between components (edges) are drawn from a finite set of possible connection choices. ContrArc uses assume-guarantee contracts to formalize different viewpoints in the system requirements, such as timing and power consumption, as well as the interface of different components, and translate the exploration problem into a mixed integer linear programming problem. It then searches for efficient solutions by relying on contract decompositions and a method based on sub graph isomorphism to iteratively prune infeasible architectures out of the search space. Experiments on a reconfigurable production line and an aircraft power distribution network show up to two orders of magnitude acceleration in architectural exploration with respect to comparable approaches
Special issue: Formal verification of cyber-physical systems
No full textThis is the preface to the Special Issue of Information and Computation related to formal verification of cyber-physical systems
Co-Design of Topology, Scheduling, and Path Planning in Automated Warehouses
No full textWe address the warehouse servicing problem (WSP) in automated warehouses, which use teams of mobile agents to bring products from shelves to packing stations. Given a list of products, the WSP amounts to finding a plan for a team of agents which brings every product on the list to a station within a given timeframe. The WSP consists of four subproblems, concerning what tasks to perform (task formulation), who will perform them (task allocation), and when (scheduling) and how (path planning) to perform them. These subproblems are NP-hard individually and are made more challenging by their interdependence. The difficulty of the WSP is compounded by the scale of automated warehouses, which frequently use teams of hundreds of agents. In this paper, we present a methodology that can solve the WSP at such scales. We introduce a novel, contract-based design framework which decomposes an automated warehouse into traffic system components. By assigning each of these components a contract describing the traffic flows it can support, we can syn-thesize a traffic flow satisfying a given WSP instance. Component-wise search-based path planning is then used to transform this traffic flow into a plan for discrete agents in a modular way. Evaluation shows that this methodology can solve WSP instances on real automated warehouses
Constraint-driven nonlinear reachability analysis with automated tuning of tool properties
No full textThe effectiveness of reachability analysis often depends on choosing appropriate values for a set of tool-specific properties which need to be manually tailored to the specific system involved and the reachable set to be evolved. Such property tuning is a time-consuming task, especially when dealing with nonlinear systems. In this paper, we propose, instead, a methodology to automatically and dynamically choose property values for reachability analysis along the system evolution, based on the actual verification objective, i.e., the verification or falsification of a set of constraints. By leveraging an initial solution to the reachable set, we estimate bounds on the numerical accuracy required from each integration step to provide a definite answer to the satisfaction of the constraints. Based on these accuracy bounds, we design a cost function which we use, after mapping the property space to an integer space, to search for locally optimal property values that yield the desired accuracy. Results from the application of our methodology to the nonlinear reachability analysis tool ARIADNE show that the frequency of correct answers to constraint satisfaction problems increases significantly with respect to a manual approach
Architectural Exploration and Design of Time-Interleaved SAR Arrays for Low-Power and High Speed A/D Converters
No full textTime-interleaved (TI) analog-to-digital converters (ADCs) are frequently advocated as a power-efficient solution to realize the high sampling rates required in single-chip transceivers for the emerging communication schemes: ultra-wideband, fast serial links, cognitive-radio and software-defined radio. However, the combined effects of multiple distortion sources due to channel mismatches (bandwidth, offset, gain and timing) severely affect system performance and power consumption of a TI ADC and need to be accounted for since the earlier design phases. In this paper, system-level design of TI ADCs is addressed through a platform-based methodology, enabling effective investigation of different speed/resolution scenarios as well as the impact of parallelism on accuracy, yield, sampling-rate, area and power consumption. Design space exploration of a TI successive approximation ADC is performed top-down via Monte Carlo simulations, by exploiting behavioral models built bottorn-up after characterizing feasible implementations of the main building blocks in a 90-nm 1-V CMOS process. As a result, two implementations of the TI ADC are proposed that are capable to provide an outstanding figure-of-merit below 0.15 pJ/conversion-step
- …
