Thrust 1: Resilient Processes and Factory Floors

For a manufacturing network to be successful in theory and practice, we must have guaranteed safety and performance at the process and node level. In this thrust, we focus on the physical layer of our system, where nodes and processes must interact and run in a correct and reliable manner. We will develop a formalism for abstracting and modeling general processes so that the systems across the shop floor and/or factory will meet the required specifications for each transaction and high-level process.

Modeling Components for Verifiability

To provide resilient processes, the formalism and modeling of the intelligent system must be one that facilitates analysis. To do this, we will extend CPS theory to formalize models that capture continuous and discrete behavior as well as uncertainty. We will build off of prior work dealing with continuous functions as values which will be further extended to local languages and the verification of continuity assumptions in refinement. Then, an abstract machine model is defined using discrete time points such that at each such time point the mode locations modelling discrete behavior may be updated, while the continuous behavior associated with pliant locations is captured by functions over intervals. Such abstract machines must be shown to capture the behavioral model and must then be presented in a user-friendly modelling language for smooth integration. To further provide resilient performance in the face of uncertainty, we will extend our models handle uncertainty through probabilistic logic exploiting sequents with associated probabilities.

Combining the (theoretical) work on reflection with the (practical) three-layered machine architecture, interaction middleware will enable the monitoring of bulk data from available sources. Here, methods for data analysis and machine learning will be exploited (as will be discussed in Thrust 2). Adaptivity is captured by the behavioral model and its associated machine model being reflective, i.e. permitting updatable self-description. The reification of the theory suggests the adoption of a three-layered machine stack addressing normal behavior, monitoring and data analysis, and adaptation. Monitoring is concerned with the collection of bulk data from available sources (status of manufacturing process, condition of equipment, external factors, sensors, etc.) that is fed into intelligent learning algorithms. The aggregated learning outcomes trigger on-the-fly adaptation, which requires methods for interruption, partial rollback, and restart to be integrated into the abstract machine model.
The results of these models are to be fed into a development methodology and supporting tools for the validation an

d verification of ground models and their stepwise refinement. The intended contribution concerns the handling of continuous aspects and compositionality based on retrenchment. Furthermore, pragmatic aspects of view-centric refinement will be studied. Concerning tool support the emphasis will be on the development of a simulator and a verifier, which will can be integrated into OSCM. The crucial issue is the integration of discrete simulation for the time-dependent behavior of continuous components into the execution of the abstract machines. The verifier will rely on natural deduction calculi and associated proof strategies and heuristics. The foundational research here will integrate in-depth theoretical models with exemplification on practical applications addressing communicating work cells in charge of realizing a joint manufacturing task (e.g., pick and place, assembly), propulsion platforms of e-vehicles controlled by software, and networks of manufacturing machines.

Requirements for Safety and Resilience

Current development processes, even when following rigorously defined steps, heavily rely on heuristic processes whereby simulation, verification, validation, and testing play important roles. In the long chain of dependencies, this means that a labor-intensive process is needed to reduce residual design and implementation errors to a minimum. In the context of safety this might not be sufficient, as residual errors may compound and lead to a catastrophe. To reduce these uncertainties, a more rigorous mathematically and logically based approach is needed. Evidence is required that answers the question if the systems’ state space is sufficiently covered to reduce the system’s failure to a minimum. The only way forward is to obtain mathematical evidence across all system domains: analog, continuous, and discrete whereby the domains are integrated and exchange state values.
Using the developed compositional models, we will explore: the formal capture of classes of constraints expressing resilience, safety and security requirements;  the specification of detection algorithms that uncover any constraint violation; and (the specification of repair and adaptation algorithms that restore the constraints. To facilitate validation and verification, we will develop methods and tools for component driven specification. The most crucial challenges concern the handling of continuous aspects and compositionality, for which the research will provide the mathematical justification of retrenchment to enable more flexibility with respect to timing aspects and to avoid mathematically undesired effects. In parallel, pragmatic aspects of refinement will be studied, including hardware constraints; symbolic and numerical solution methods; and concurrent systems. Simulations of the interacting layers are required for testing the integration of components and for allowing us to use existing prover tools. Further, we will define Assured Reliability and Resilience Level (ARRL) for all components, systems on the shop floor, and nodes in the network . ARRL defines architectural properties and processes that must be in place to meet the requirements of a given level by considering the fault behavior and mitigation measures.

Specifically, we will explore methods for modular validation. We have been developing methods in adaptive testing of complex systems, effectively searching the state-space for potential failures. Using insights from reinforcement learning solvers, this method allows us to find most likely failure modes that may not be easily found by domain experts. We have demonstrated this approach in the transportation domain. This technique can be applied to manufacturing pipelines in a modular fashion to identify vulnerabilities or sources of error. Further, we have explored online monitoring techniques that can guarantee safe performance in when systems are interacting with human agents. Typically, such verification and validation approaches are designed for static, well-modeled systems. As these systems adapt and expand, we will explore new methods for adapting these tools for dynamic and evolving systems by integrating domain and user insight=. We have demonstrated how these monitoring, verification, and validation tools can be used to develop more robust planning.

To mitigate these potential failure modes and avoid Byzantine faults, we will investigate how to incorporate backwards reachability into the manufacturing process and the shop floor and close the loop on robust decision-making and control. To guarantee consistency of our verification, we must explore the safety requirements in the temporal extensions of the logic. The project will advance adaptation algorithms as recovery mechanisms, which are based on a redundancy and replacement principle. With respect to these recovery actions, the situation is similar to security requirements, as a new class of proof obligations will be required emphasizing that the system will recover from an error situation, once it has been detected and repair actions have been initiated, after a pre-determined maximum number of steps. Thus, the project will advance the state of the art by investigating this class of proof obligations. When defining safety constraints, we must consider the compositionality of constraints under both hard and soft constraints. Further, we must develop detection and prediction methods for violations for use in real-world manufacturing settings.