A semantic-driven tradespace framework to accelerate aircraft manufacturing system design

During the design phase of an aircraft manufacturing system, different industrial scenarios need to be evaluated according to key performance indicators to achieve the optimal system performance. It is a highly complex process involving multidisciplinary stakeholders, various digital tools and protocols. To address the digital discontinuity challenge during this process, this paper proposes a tradespace framework based on semantic technology and model-based systems engineering. It aims at functionality integration of requirement management, architecture definition, manufacturing system design, solution verification and visualization. An application ontology is developed to integrate assembly system domain knowledge, industrial requirements and system architecture model information. The proposed framework is implemented in a case study to support the fuselage orbital joint process design, which is part of the aircraft final assembly line. A toolchain is presented to support the implementation, which consists of a set of enabling software corresponding to the functional modules of the framework. Different manufacturing system architectures are first designed by industrial system engineers supported by the application ontology stored in a graph database. They are then analyzed through Discrete Event Simulations and 3D simulations. The simulation results are presented through a web-based portal to show the key performance values of each architecture. This study serves as a part of the proof-of-concept of the recently proposed Cognitive Digital Twin concept.

Ontology-based system to support industrial system design for aircraft assembly

Jinzhi Lu, Xiaochen Zheng

The development of an aircraft industrial system is a complex process which faces the challenge of digital discontinuity in multidisciplinary engineering due to various interfaces between different digital tools, leading to extra development time and costs. This paper proposes an ontology-based system, aiming at functionality integration and design process automation, by Models for Manufacturing methodology principles. A tool-agnostic modelling, simulation and validation platform with Discrete Event Simulation and 3D simulation is enabled and demonstrated in a real case study. An ontology layer collecting the domain knowledge enables integration of the proposed system, accelerating the design process and enhancing design quality. Copyright (c) 2022 The Authors.This is an open access article under the CC BY-NC-ND license (http://creativecommons.org/licenses/by-nc-nd/4.0/)

ELSEVIER2022

Algorithmic Verification of Component-based Systems

Qiang Wang

This dissertation discusses algorithmic verification techniques for concurrent component-based systems modeled in the Behavior-Interaction-Priority (BIP) framework with both bounded and unbounded concurrency. BIP is a component framework for mixed software/hardware system design in a rigorous and correct-by-construction manner. System design is defined as a formal, accountable and coherent process for deriving trustworthy and optimised implementations from high-level system models and the corresponding execution platform descriptions. The essential properties of a system model are guaranteed at the earliest possible design phase, and a correct implementation is then automatically generated from the validated high-level system model through a sequence of property preserving model transformations, which progressively refines the model with details specific to the target execution platform. The first major contribution of this dissertation is an efficient safety verification technique for BIP system models, where the number of participating components is fixed and the data variables can have infinite domains, but their manipulation is limited to linear arithmetic. The key insight of our technique is to take advantage of the structure features of the BIP system and handle the computation in the components and coordination between the components in the verification separately. On the computation level, we apply the state-of-the-art counterexample abstraction techniques to reason about the behavior of components and explore all the possible reachable states ; while on the coordination level, we exploit both partial order techniques and symmetry reduction techniques to handle the state space explosion problem due to concurrency, and reduce the redundant interleavings of concurrent interactions. We have implemented the proposed techniques in a prototype tool and carried out a comprehensive performance evaluation on a set of BIP system models. The second major contribution of this dissertation is a uniform design and verification framework for parameterized systems based on BIP. Parameterized systems are systems consisting of homogeneous processes, and the parameter indicates the number of such processes in the system. A parameterized system, therefore, describes an infinite family of systems, where instances of the family can be obtained by fixing the value of the parameter. Verification of correctness of such systems amounts to verifying the correctness of every member of the infinite family described by the system. First of all, we propose the first order interaction logic (FOIL) as a formal language for parameterized system architectures and communication primitives. This logic is powerful enough to express architectures found in distributed systems, including the classical architectures : token-passing rings, rendezvous cliques, broadcast cliques, rendezvous stars. We also identify a fragment of FOIL that is well-suited for the specification of parameterized BIP systems and prove its decidability. Second, we provide a framework for the integration of mathematical models from the parameterized model checking literature in an automated way. With our new framework, we close the gap between the mathematical formalisms and algorithms from the parameterized verification research and the practice of parameterized verification, which is usually done by engineers who are not familiar with the details of the literature.

EPFL2017

Circuit Design, Architecture and CAD for RRAM-based FPGAs

Xifan Tang

Field Programmable Gate Arrays (FPGAs) have been indispensable components of embedded systems and datacenter infrastructures. However, energy efficiency of FPGAs has become a hard barrier preventing their expansion to more application contexts, due to two physical limitations: (1) The massive usage of routing multiplexers causes delay and power overheads as compared to ASICs. To reduce their power consumption, FPGAs have to operate at low supply voltage but sacrifice performance because the transistors drive degrade when working voltage decreases. (2) Using volatile memory technology forces FPGAs to lose configurations when powered off and to be reconfigured at each power on. Resistive Random Access Memories (RRAMs) have strong potentials in overcoming the physical limitations of conventional FPGAs. First of all, RRAMs grant FPGAs non-volatility, enabling FPGAs to be "Normally powered off, Instantly powered on". Second, by combining functionality of memory and pass-gate logic in one unique device, RRAMs can greatly reduce area and delay of routing elements. Third, when RRAMs are embedded into datpaths, the performance of circuits can be independent from their working voltage, beyond the limitations of CMOS circuits. However, researches and development of RRAM-based FPGAs are in their infancy. Most of area and performance predictions were achieved without solid circuit-level simulations and sophisticated Computer Aided Design (CAD) tools, causing the predicted improvements to be less convincing. In this thesis,we present high-performance and low-power RRAM-based FPGAs fromtransistorlevel circuit designs to architecture-level optimizations and CAD tools, using theoretical analysis, industrial electrical simulators and novel CAD tools. We believe that this is the first systematic study in the field, covering: From a circuit design perspective, we propose efficient RRAM-based programming circuits and routing multiplexers through both theoretical analysis and electrical simulations. The proposed 4T(ransitor)1R(RAM) programming structure demonstrates significant improvements in programming current, when compared to most popular 2T1R programming structure. 4T1R-based routingmultiplexer designs are proposed by considering various physical design parasitics, such as intrinsic capacitance of RRAMs and wells doping organization. The proposed 4T1R-based multiplexers outperformbest CMOS implementations significantly in area, delay and power at both nominal and near-Vt regime. From a CAD perspective, we develop a generic FPGA architecture exploration tool, FPGASPICE, modeling a full FPGA fabric with SPICE and Verilog netlists. FPGA-SPICE provides different levels of testbenches and techniques to split large SPICE netlists, in order to obtain better trade-off between simulation time and accuracy. FPGA-SPICE can capture area and power characteristics of SRAM-based and RRAM-based FPGAs more accurately than the currently best analyticalmodels. From an architecture perspective, we propose architecture-level optimizations for RRAMbased FPGAs and quantify their minimumrequirements for RRAM devices. Compared to the best SRAM-based FPGAs, an optimized RRAM-based FPGA architecture brings significant reduction in area, delay and power respectively. In particular, RRAM-based FPGAs operating in the near-Vt regime demonstrate a 5x power improvement without delay overhead as compared to optimized SRAM-based FPGA operating at nominal working voltage.

EPFL2017

Circuit Design, Architecture and CAD for RRAM-based FPGAs

Xifan Tang

EPFL2017

Algorithmic Verification of Component-based Systems

Qiang Wang

EPFL2017