The effects of personnel scheduling on the quality of care and working conditions for healthcare personnel have been thoroughly documented. However, the ever-present demand and large variation of constraints make healthcare scheduling particularly challenging. This problem has been studied for decades, with limited research aimed at applying Satisfiability Modulo Theories (SMT). SMT has gained momentum within the formal verification community in the last decades, leading to the advancement of SMT solvers that have been shown to outperform standard mathematical programming techniques.In this work, we propose generic constraint formulations that can model a wide range of real-world scheduling constraints. Then, the generic constraints are formulated as SMT and MILP problems and used to compare the respective state-of-the-art solvers, Z3 and Gurobi, on academic and real-world inspired rostering problems. Experimental results show how each solver excels for certain types of problems; the MILP solver generally performs better when the problem is highly constrained or infeasible, while the SMT solver performs better otherwise. On real-world inspired problems containing a more varied set of shifts and personnel, the SMT solver excels. Additionally, it was noted during experimentation that the SMT solver was more sensitive to the way the generic constraints were formulated, requiring careful consideration and experimentation to achieve better performance. We conclude that SMT-based methods present a promising avenue for future research within the domain of personnel scheduling.

Multi-agent Path Finding (MAPF) is the problem of planning collision-free movements of agents so that they get from where they are to where they need to be. Commonly, agents are located on a graph and can traverse edges. This problem has many variations and has been studied for decades. Two such variations are the continuous-time and the lifelong MAPF problems. In the former, edges have non-unit lengths and volumetric agents can traverse them at any real-valued time. In the latter, agents must attend to a continuous stream of incoming tasks. Much work has been devoted to designing solution methods within these two areas. To our knowledge, however, the combined problem of continuous-time lifelong MAPF has yet to be addressed.This work addresses continuous-time lifelong MAPF with volumetric agents by presenting the fast and sub-optimal Continuous-time Prioritized Lifelong Planner (CPLP). CPLP continuously assigns agents to tasks and computes plans using a combination of two path planners; one based on CCBS and the other based on SIPP. Experimental results with up to 800 agents on graphs with up to 12000 vertices demonstrate practical performance, where maximum planning times fall within the available time budget. Additionally, CPLP ensures collision-free movement even when failing to meet this budget. Therefore, the robustness of CPLP highlights its potential for real-world applications.

Increased demand for healthcare services is placing a significant strain on hospitals. Prolonged waiting times for patients are becoming commonplace, while healthcare staff are subjected to unsustainable workloads. Finding ways to increase patient flow through hospital departments is one crucial step toward efficient healthcare services.In this work, a modelling framework is proposed to model patient flow though a healthcare department. Patient progression and resource allocation is simulated, offering insights into expected outcomes, bottlenecks, and other inefficiencies.A discrete-event model of a hospital department is formulated and proposed to be used together with Monte Carlo simulations. Patient treatment is represented by a series of processes, each consisting of smaller tasks. Medical staff members are represented as resources with specific qualifications that decide what tasks they may execute. Resources are allocated dynamically to model department-specific procedures, therefore increasing the flexibility of the proposed framework and opening up modelling possibilities to different healthcare departments.A real-world healthcare department is modelled and simulated using historic data and expert knowledge. In this way, the modelling flexibility of the framework is shown. Comparisons between simulation results and actual outcomes highlight the importance of establishing high-quality quantitative data collection in healthcare departments at an early stage to provide a stable foundation for operational modelling research. With accurate process times and resource usage data, the proposed framework has the potential to serve as an important support function, and ultimately contribute to a more sustainable and efficient healthcare.

Cyber-physical systems are often safety-critical and their correctness is crucial, such as in the case of automated driving. Using formal mathematical methods is one way to guarantee correctness and improve safety. Although these methods have shown their usefulness, care must be taken because modelling errors might result in proving a faulty controller safe, which is potentially catastrophic in practice. This paper deals with two such modelling errors in differential dynamic logic, a formal specification and verification language for hybrid systems, which are mathematical models of cyber-physical systems. The main contributions are to provide conditions under which these two modelling errors cannot cause a faulty controller to be proven safe, and to show how these conditions can be proven with help of the interactive theorem prover KeYmaera X. The problems are illustrated with a real world example of a safety controller for automated driving, and it is shown that the formulated conditions have the intended effect both for a faulty and a correct controller. It is also shown how the formulated conditions aid in finding a loop invariant candidate to prove properties of hybrid systems with feedback loops. Furthermore, the relation between such a loop invariant and the characterisation of the maximal control invariant set is discussed.

Supervisory control theory provides an approach to synthesize supervisors for cyber-physical systems using a model of the uncontrolled plant and its specifications. These supervisors can help guarantee the correctness of the closed-loop controlled system. However, access to plant models is a bottleneck for many industries, as manually developing these models is an error-prone and time-consuming process. An approach to obtaining a supervisor in the absence of plant models would help industrial adoption of supervisory control techniques. This paper presents$SupL^{*}$, an algorithm to learn a maximally permissive controllable supervisor in the absence of plant models. It does so by actively interacting with a simulation of the plant by means of queries. If the obtained supervisor is blocking, existing synthesis techniques are employed to prune the blocking supervisor and obtain the maximally permissive controllable and non-blocking supervisor. Additionally, this paper presents an approach to interface the$SupL^{*}$with a PLC to learn supervisors in a virtual commissioning setting. This approach is demonstrated by learning a supervisor of the well-known Machine Buffer Machine example simulated in Xcelgo Experior and controlled using a PLC.$SupL^{*}$interacts with the PLC and learns a maximally permissive controllable supervisor for the simulated system. Note to Practitioners—Ensuring the correctness of automated systems is crucial. Supervisory control theory proposes techniques to help build control solutions that have certain correctness guarantees. These techniques rely on a model of the system. However, such models are typically unavailable and hard to create. Active learning is a promising technique to learn models by interacting with the system to be learned. This paper aims to integrate active learning and supervisory control such that the manual step of creating models is no longer needed, thus, allowing the use of supervisory control techniques in the absence of models. The proposed approach is implemented in a tool and demonstrated using a case study.

Falsification is a testing method that aims to increase confidence in the correctness of cyber–physical systems by guiding the search for counterexamples with some optimization algorithm. This method generates input signals for a simulation of the system under test and employs quantitative semantics, which serves as objective functions, to minimize the distance needed to falsify a specification. Various implementations based on different optimization strategies and semantics have been proposed and evaluated in the past. Generally, they assume that an input generator is given. However, this is often not the case in practice and different choices can lead to vastly different outcomes. Therefore, this article introduces and evaluates various parameterizations of input generators, including pulse, sinusoidal, and piecewise signals with different interpolation techniques. These input generators are compared based on their performance on benchmark examples, as well as coverage measures in the space-time and frequency domains. Input generators facilitate the exploration of numerous different input signals within a single falsification problem, making them especially valuable for industrial practitioners seeking to incorporate falsification into their daily development work.

Safety critical systems are typically subjected to hazard analysis before commissioning to identify and analyse potentially hazardous system states that may arise during operation. Currently, hazard analysis is mainly based on human reasoning, past experiences, and simple tools such as checklists and spreadsheets. Increasing system complexity makes such approaches decreasingly suitable. Furthermore, testing-based hazard analysis is often not suitable due to high costs or dangers of physical faults. A remedy for this are model-based hazard analysis methods, which either rely on formal models or on simulation models, each with their own benefits and drawbacks. This paper proposes a two-layer approach that combines the benefits of exhaustive analysis using formal methods with detailed analysis using simulation. Unsafe behaviours that lead to unsafe states are first synthesised from a formal model of the system using Supervisory Control Theory. The result is then input to the simulation where detailed analyses using domain-specific risk metrics are performed. Though the presented approach is generally applicable, this paper demonstrates the benefits of the approach on an industrial human-robot collaboration system.

Compositional Optimization(CompOpt) was recently proposed for optimization of discrete-event systems of systems. A modular optimization model allows CompOpt to divide the optimization into separate sub-problems, mitigating the state space explosion problem. This paper presents the Modular Optimization Learner (MOL), a method that interacts with a simulation of a system to automatically learn these modular optimization models. MOL uses amodular learningthat takes as input a hypothesis structure of the system and uses the provided structural information to split the acquired learning into a set of modules, and to prune parts of the search space. Experiments show that modular learning reduces the state space by many orders of magnitude compared to a monolithic learning, which enables learning of much larger systems. Furthermore, an integrated greedy search heuristic allows MOL to remove many sub-optimal paths in the individual modules, speeding up the subsequent optimization.Note to Practitioners—Automation systems are becoming increasingly large and complex and the automation of more and more advanced tasks often requires the coordination of multiple subsystems. Optimization can have a great impact on the efficiency of these systems in terms of cost and operation speed. Finding optimal solutions is, however, a difficult task. As the number of tasks and subsystems of the automation system increases, the search space of the optimization problems tends to grow exponentially.Compositional Optimization(CompOpt) is a method specifically designed for the optimization of large-scale automation systems. A challenge with the application of CompOpt is that it takes as input a specific type of optimization model that divides the system into subsystems; like machines, vehicles, etc. Formulating these models requires a high level of expertise and system knowledge. This paper addresses this challenge with an algorithm that learns these models from a simulation of the system. The simulation can be implemented in any software as long as a suitable interface exists or can be constructed. To divide the learning into subsystems, the algorithm uses an initialplant structure hypothesis(PSH). This can be viewed as a meta-model that includes known structural information, such as the number of subsystems and which actions that affect each subsystem. The more structural information that is added to PSH, the more efficient the learning and subsequent optimization will be. The purpose of this is to reduce the level of expertise and system knowledge needed in the application of optimization, to simplify the transition to Industry 4.0.

The Conflict-Free Electric Vehicle Routing Problem (CF-EVRP) is an extension of the Vehicle Routing Problem (VRP), a combinatorial optimization problem of designing routes for vehicles to visit customers such that a cost function, typically the number of vehicles or the total travelled distance, is minimized. The problem finds many logistics applications, particularly for highly automated logistic systems for material handling. The CF-EVRP involves constraints such as time windows on the delivery to the customers, limited operating range of the vehicles, and limited capacity on the number of vehicles that a road segment can accommodate at the same time. In this paper, the compositional algorithm ComSat for solving the CF-EVRP is presented. The algorithm iterates through the sub-problems until a globally feasible solution is found. The proposed algorithm is implemented using an optimizing SMT-solver and is evaluated against an implementation of a previously presented monolithic model. The soundness and completeness of the algorithm are proven, and it is benchmarked on a set of generated problems and found to be able to solve problems of industrial size.Note to Practitioners—The need to define and solve the CF-EVRP relates to an industrial application where a fleet of autonomous robots navigates in a heterogeneous environment, shared with humans and other vehicles and obstacles. To allow for a low-level trajectory controller to handle dynamic obstacles, like humans and fork-lifts, the CF-EVRP includes capacity constraints on the road segments. This increases the problem complexity, and thus requires to trade off optimality for feasability; this so to get solutions in reasonable time with respect to how long ahead the jobs to schedule are known. The overall problem is to find feasible solutions that satisfy all constraints while avoiding travelling unnecessarily long routes, and at the same time meet the stipulated time-windows to deliver material just-in-time. The compositional algorithm (ComSat) presented in this work is based on the idea to break down the overall scheduling problem into sub-problems that are easier to solve, and then to build a schedule based on the solutions of the sub-problems. ComSat is designed to work well for industrial scenarios where there are good reasons to believe that feasible solutions do exist. This seems a reasonable assumption as in an industrial setting a sufficient number of mobile robots can typically be assumed to be available.

Cyber-physical systems (CPSs) are complex and exhibit both continuous and discrete dynamics, hence it is difficult to guarantee that they satisfy given specifications, i.e., the properties that must be fulfilled by the system. Falsification of temporal logic properties is a testing approach that searches for counterexamples of a given specification that can be used to increase the confidence that a CPS does fulfill its specifications. Falsification can be done using random search methods or optimization methods, both of which have their own benefits and drawbacks. This article introduces two methods that exploit randomness to different degrees: 1) the optimization-free Hybrid-Corner-Random (HCR) and 2) the direct-search method Line-Search Falsification (LSF). HCR combines randomly chosen parameter values with extreme parameter values, which performs surprisingly well on benchmark evaluations. The gradient-free optimization-based LSF optimizes over line segments through a vector of inputs in the$n$-dimensional parameter space. The two methods are compared to the Nelder-Mead and SNOBFIT methods, using a well-known set of benchmark problems and LSF shows better performance than any of the evaluated methods.

Bin packing and bin covering are important optimization problems in many industrial fields, such as packaging, recycling, and food processing. The problem concerns a set of items, each with its own value, that are to be sorted into bins in such a way that the total value of each bin, as measured by the sum of its item values, is not above (for packing) or below (for covering) a given target value. The optimization problem concerns minimizing, for bin packing, or maximizing, for bin covering, the number of bins. This is a combinatorial NP-hard problem, for which true optimal solutions can only be calculated in specific cases, such as when restricted to a small number of items. To get around this problem, many suboptimal approaches exist. This article describes the formulations of the bin packing and covering problems that allow finding the true optimum, for instance, counting hundreds of items using general-purpose MILP-solvers. Also presented are suboptimal solutions that come within less than 10% of the optimum while taking significantly less time to calculate, even ten to 100 times faster, depending on the required accuracy.

Collaborative and intelligent automation systems need intelligent control systems. Some of this intelligence exist on a per-component basis in the form of vision, sensing, motion, and path planning algorithms. To fully take advantage of this intelligence, also the coordination of subsystems need to exhibit intelligence. While there exist middleware solutions that eases communication, development, and reuse of such subsystems, for example the Robot Operating System (ROS), good coordination also requires knowledge about how control is supposed to be performed, as well as expected behavior of the subsystems. This paper introduces lightweight components that wraps ROS2 nodes into composable control components from which an intelligent control system can be built. The ideas are implemented on a use case involving collaborative robots with on-line path planning, intelligent tools, and human operators.

In this paper, limitations of the IOCOS testing relation in regard to testing safety PLC code is examined and a modification of the current IOCOS relation, called safe-IOCOS is proposed. In the IOCOS testing relation, an implementation is IOCOS with respect to a specification, if it emits a subset of the specified outputs and a super-set of the specified inputs after the execution of each trace in the specification. However, for testing safety PLC code, the IOCOS relation is not detailed enough as the subset requirement on the respective inputs and outputs could allow some safety behaviors to go untested. These limitations of the IOCOS relation may thus pose threats to humans. So the notion of safe-IOCOS is defined, which strengthens IOCOS to require equality between the implementation and the specification in relation to the inputs and outputs, respectively. An example shows these shortcomings of IOCOS and how the proposed safe-IOCOS relation is better suited for testing safety PLC code.

Autonomous vehicles apply pertinent planning and control algorithms under different driving conditions. The mode switch between these algorithms should also be autonomous. On top of the nominal planners, a safe fallback routine is needed to stop the vehicle at a safe position if nominal operational conditions are violated, such as for a system failure. This paper describes the design and formal verification of a supervisor to manage all requirements for mode switching between nominal planners, and additional requirements for switching to a safe stop trajectory planner that acts as the fallback routine. The supervisor is designed via a model-based approach and its abstraction is formally verified by model checking. The supervisor is implemented and integrated with the Research Concept Vehicle, an experimental research and demonstration vehicle developed at the KTH Royal Institute of Technology. Simulations and experiments show that the vehicle is able to autonomously drive in a safe manner between two parking lots and can successfully come to a safe stop upon GPS sensor failure.

In this paper, an approach based on the IOCOS testing relation to test safety PLC code using the tool QuickCheck is presented. Testing and validation of the safety PLC code is typically carried out on a physical system using checklists. These checklists are developed by engineers using system specification. However, due to the manual nature of checklist generation and execution, certain test cases can be overlooked and can lead to human accidents. The presented approach allows on-the-fly generation and execution of test cases, which expands the scope of testing by including test cases unconceived during checklist generation. Furthermore, it is demonstrated how errors in the safety PLC code are uncovered based on the IOCOS relation.

We consider the falsification of temporal logic properties as a method to test complex systems, such as autonomous systems. Since these systems are often safety-critical, it is important to assess whether they fulfill given specifications or not. An adaptive cruise controller for an autonomous car is considered where the closed-loop model has unknown parameters and an important problem is to find parameter combinations for which given specification are broken. We assume that the closed-loop system can be simulated with the known given parameters, no other information is available to the testing framework. The specification, such as, the ability to avoid collisions, is expressed using Signal Temporal Logic (STL). In general, systems consist of a large number of parameters, and it is not possible or feasible to explicitly enumerate all combinations of the parameters. Thus, an optimization-based approach is used to guide the search for parameters that might falsify the specification. However, a key challenge is how to select the objective function such that the falsification of the specification, if it can be falsified, can be falsified using as few simulations as possible. For falsification using optimization it is required to have a measure representing the distance to the falsification of the specification. The way the measure is defined results in different objective functions used during optimization. Different measures have been proposed in the literature and in this paper the properties of the Max Semantics (MAX) and the Mean Alternative Robustness Value (MARV) semantics are discussed. After evaluating these two semantics on an adaptive cruise control example, we discuss their strengths and weaknesses to better understand the properties of the two semantics.

The Eleventh Annual IEEE International Conference on Automation Science and Engineering (CASE 2015) was held on August 24–28, at Elite Park Avenue Hotel in Gothenburg, Sweden. IEEE CASE represents the Flagship Automation Conference of the IEEE Robotics and Automation Society and constitutes the primary forum for cross-industry and multidisciplinary research in automation. The conference theme wasAutomation for a Sustainable Future, a global challenge emphasized at the conference by specific workshops and a number of oral sessions. The focus on sustainability involves energy saving, life science, as well as resource efficiency and reusability.

Fault tolerant systems, commonly found in literature, are implemented in various computer applications. Some of these methods have been studied and developed to aid manufacturing systems; however, they have rarely been integrated into the manufacturing process. Broadly, the problem seems to be integration of error handling procedures towards the end of physically building the manufacturing line, lack of a defined workflow, untested program logic and inadequately equipped personnel to name a few. To this end, a survey was conducted within the Swedish automotive industry to get an understanding of current error handling procedures and its shortcomings, and are presented here. Based on this data, and looking at the trends within the manufacturing industry, this paper also identifies research topics aimed towards defining methods to create next generation fault tolerant manufacturing systems.

This paper presents a supervisory control theory based offline approach for calculating restart states in a manufacturing control system. Given these precalculated restart states, an operator can be given instructions for how to correctly resynchronize the control system and the manufacturing resources during the online restart phase, as part of the error recovery process. Restarting from a restart state guarantees that all requirements on the nominal and the restarted productions are fulfilled. The paper includes an empirical comparison showing that the proposed approach enables restart states calculation for systems of sizes that could not be handled using an earlier presented approach.

A generic state-vector transition (SVT) model is suggested, including a flexible synchronous composition involving both shared variables and events. This model is analyzed, focusing on properties that are important for supervisor synthesis. A synthesis procedure is then developed for the SVT model, where supervisor guards are generated that guarantee a controllable, nonblocking and maximally permissive supervisor. Novel conditions are introduced, such that more flexible specifications can be applied than earlier suggested for related models. Since the SVT model includes automata and (colored) Petri nets, optionally extended with variables, guards and actions, as special cases, the suggested synthesis approach unifies supervisor synthesis for the main discrete event model classes. Finally, the SVT model is naturally represented and efficiently computed based on binary decision diagrams, and the resulting supervisor guards are easily implemented in industrial control systems.

This paper presents a preprocess to an existing method for offline calculation of restart states for manufacturing systems modeled by operations. In the existing method, placement transitions are used to model restart in restart states from potential error states, and supervisory control theory is used to calculate which of these transitions are valid. With the proposed preprocess, the precedence and the alternative dependencies between the operations are exploited in order to reduce the number of such placement transitions which are required in the model used by the existing method. With such a reduced model, the valid restart states for larger and more complex systems can be calculated.

In supervisory control theory, a supervisor restricts the plant in order to fulfill given specifications. A problem for larger industrial applications is that the resulting supervisor is not easily implemented and comprehensible for the users. To tackle this problem, an efficient method has recently been introduced to characterize a supervisor by tractable logic conditions, referred to as guards. This approach has been developed for a specific type of automata with variables called extended finite automata (EFAs). An extension of this approach to a more general class of models is presented in this paper. It means that classical supervisory control problems for automata and Petri nets are easily and efficiently solved, but also generalized based on the suggested approach. The synthesis procedure is naturally modeled and efficiently computed based on binary decision diagrams.

This paper presents a method for modeling robot and human resources in the context of assembly systems planning. In assembly systems, several redundant resources can be used to increase system flexibility. However, the “quality” of a sequence planning strongly depends on the “quality” of the system modeling. Furthermore, occurrence of unexpected events or variations in availability of resources may have significant impact on the actual planning. Instead of using simplistic models such as available or unavailable resources, the method presented in this paper proposes a more detailed modeling of resource abilities. Products and resources are considered on the same levels and matched together on a final step. The aim of this modeling is to permit analyses and to increase system flexibility.

A method for restart after an error in a manufacturing system is introduced. The method is able to restart systems even after nonforeseen errors that cannot be planned for, and the online part of the restart method does not require use of more powerful computers than a standard Programmable Logic Controller. It is shown what properties the control function must have to ensure that there is at least one restart state for each controller state. Sufficient conditions to guarantee the possibility to restart a system regardless of where an error occurs are given, along with indications on how the system could otherwise be rebuilt to be restartable.

In order to obtain a unified information flow from early product design to final production, an integrated framework for product, process and automation design is presented. The framework is based on sequences of operations and includes a formal relation between product properties and process operations. This relation includes liaisons (interfaces) and precedence relations, where the precedence relations generate preconditions for the related process operations. From this information a set of sequences of operations (SOPs) is generated. A formal graphical language for hierarchical operations and SOPs is then introduced and defined based on automata extended with variables. Since the operations are self-contained they can be grouped and viewed from different angles, e.g., from a product or a resource perspective. These multiple views increase the interoperability between different engineering disciplines. A case study is performed on a car manufacturing cell, where the suggested modeling framework is shown to give comprehensible SOPs.

Component-based programming frameworks for industrial control logic development promise to shorten development and modification times, and to reduce programming errors. To get these benefits, it is, however, important that the components are specified and verified to work properly. This work introducesReusable Automation Components(RACs), which contain not only the implementation details but also a formal specification defining the correct use and behaviour of the component. This formal specification uses temporal logic to describe time-related properties and has a special structure developed to meet industrial control needs. The RAC can be formally verified, to determine whether the implementation fulfils the specification or not. A RAC prototype development tool has been developed to demonstrate this capability. The main difference between the RAC and other frameworks for formal verification of control logic is the specification modeling. In RAC, not only the implementation but also the specification is based on the structure and languages of conventional control logic, aiming at being easy to comprehend for control logic engineers. Several industrial examples are discussed in this paper, showing the benefits and potential of the framework.

Insufficient indication of errors is a problem in many manufacturing systems. Lack of support for resynchronization of the cell and its control system is another, less obvious problem. A third problem connected to errors in manufacturing cells is lack of support for manual control. In order to resolve an error situation manual control of the cell is often required. The problem is that some of the manual operations may be blocked due to machine protection. When an operator is to execute a blocked operation the only response is that nothing happens. This paper proposes a method where control programs with integrated functions for error detection, resynchronization, and support for manual control are generated out of information that already exists in the development process of a manufacturing system.

Shortened product life-cycles decrease the output rate of manufacturing systems. Offline verification of the control systems promises to increase the output. However, to make offline verification possible some major improvements of the current development process of manufacturing systems are needed. Information handling and development of control programs based on information reuse are the two most important improvement areas. This paper deals with one problem up the many connected to enabling offline verification. A general control program structure, adapted to information reuse and formal mathematical verification methods, is needed. This paper proposes a program structure that makes it possible to generate the PLC-program out of information that already exists in the development process of a manufacturing system. In order to further increase the ability of offline verification the proposed program structure is adapted to import information processed by formal mathematical methods.

Shortened product life-cycles decreases the output rate of manufacturing systems as the introduction of new products into the manufacturing system becomes more frequent. Improvements of the development process of manufacturing systems are needed to increase the output. Information handling and development of control programs based on information reuse are two of the most important improvement areas. These areas, among other things, can be a support for offline verification, which promises to directly increase the output rate due to shortening product introduction times. This paper deals with two problems of the many connected to enabling offline verification. First, a general control program structure, adapted to information reuse, is needed and secondly, the information necessary to generate the control programs needs to be defined. A method is proposed where information from the mechanical design of a cell, from the product, and from manual simulation are reused and automatically converted into control programs that schedule the work in a collision-free, deadlock-free and time-optimized way. The correctness of the generated programs is guaranteed by use of formal methods, simulation and an uncorrupted conversion of specifications into control programs.

Based on some modeling primitives from automata, Petri nets and process algebra, an architecture for a general routing and resource booking problem is presented. The architecture is based on general models for a set of resources, desired routing specifications for a set of objects (products, data packets, vehicles) and a controller that synchronizes the objects utilization of the available resources. High level graphical routing specifications for the objects are also introduced, together with corresponding Petri nets, in order to simplify the specification of desired routes. Two specific operators, event synchronization and arbitrary order including an algebra of events, are then used in the formal Petri net specifications.

This paper presents part of the results from a research project aimed at increasing flexibility and reusability of cell-control software. First to be discussed are the concept of flexibility and the advantages and disadvantages of various types of modular controllers. Then guidelines, generic models that describe the behavior of manufacturing resources, and a message-passing structure are given. The guidelines and the models should be used as the basis to support system developers when implementing modular control software for machining cells. The two main case studies examined to achieve the models are also briefly described.