A flexible workcell controller has been developed using a three level control hierarchy (workcell, workstation, equipment). The cell controller is automatically generated from a model input by the user. The model consists of three sets of graphs. One set of graphs describes the process plans of the parts produced by the manufacturing system, one set describes movements into, out of and within workstations, and the third set describes movements of parts/transporters between workstations. The controller uses an event driven Petri net to maintain state information and to communicate with lower level controllers. The control logic is contained in an artificial neural network. The Petri net state information is used as the input to the neural net and messages that are Petri net events are output from the neural net. A genetic algorithm was used to search over alternative operation choices to find a "good" solution. The system was fully implemented and several test cases are described.

Background: The development of the IT-industry, where new technologies and new services continually arise, has led to new players with different specializations. The increased degree of specialization means that these players need to cooperate with each other in different types of projects. Problem definition: What factors are important in a project to achieve the objectives as quickly as possible? More players should lead to cooperation difficulties, how can you coordinate in the best possible way? Today, it is desirable for all parties in the project to shorten down the lead time. Purpose: The main purpose is to explore the different factors that affects the project's lead time concerning broadband installation. The part purpose, is to analyze and assess the conditions for cooperation between different players in the project for broadband installation and to provide a recommendation. Method: In order to answer the problem definition, the paper is structured around a qualitative approach with interviews to obtain data. Mostly, the used data comes from primary sources with an extension of secondary sources. Theories: Theories that are used in the paper are: Communication Process, Communication Plan, Project Planning & Project Plan, Efficiency through collaboration, Communication in a network. Empiric: Empirical data consists of primary data collected through interviews. Analysis: The analysis is based on the variables from the theoretical frame of reference; Communications, Planning, Interaction & Information. From these variables, empirical data are analyzed in relation to the theory. Conclusion: In the conclusion, the authors discuss about the projects process which is described in the paper. The authors have concluded that; communication, planning and collaboration plays a major role in order to shorten down the lead times for the project. Cooperation beyond enterprise boundaries becomes necessary.

The creation of large-scale simulation models is a difficult and time-consuming task. Yet simulation is one of the techniques most frequently used by practitioners in Operations Research and Industrial Engineering, as it is less limited by modeling assumptions than many analytical methods. The effective generation of simulation models is an important challenge. Due to the rapid increase in computing power, it is possible to simulate significantly larger systems than in the past. However, the verification and validation of these large-scale simulations is typically a very challenging task. This thesis introduces a simulation framework that can generate a large variety of manufacturing simulation models. These models have to be described with a simulation data specification. This specification is then used to generate a simulation model which is described as a Petri net. This approach reduces the effort of model verification. The proposed Petri net data structure has extensions for time and token priorities. Since it builds on existing theory for classical Petri nets, it is possible to make certain assertions about the behavior of the generated simulation model. The elements of the proposed framework and the simulation execution mechanism are described in detail. Measures of complexity for simulation models that are built with the framework are also developed. The applicability of the framework to real-world systems is demonstrated by means of a semiconductor manufacturing system simulation model.

A net is a special configuration of lines and points in the projective plane. There are certain restrictions on the number of its lines and points. We proved that there cannot be any (4,4) nets in CP^2. In order to show this, we use tropical algebraic geometry. We tropicalize the hypothetical net and show that there cannot be such a configuration in CP^2.

Thesis (Ph. D.)--University of Missouri-Columbia, 2000. / Typescript. Vita. Includes bibliographical references (leaves 200-206). Also available on the Internet.

Thesis (Ph. D.)--University of Missouri-Columbia, 2000. / Typescript. Vita. Includes bibliographical references (leaves 200-206). Also available on the Internet.

Se ha determinado, en una arquitectura multi-Core SMP, el lugar donde incorporar el PP o el HPP sin alterar el ISA del resto de los core. Se ha obtenido una familia de procesadores que ejecutan los algoritmos de Petri para dar solución a sistemas reactivos y concurrentes, con una sólida verificación formal que permite la programación directa de los procesadores. Para esto, se ha construido el hardware de un PP y un HPP, con un IP-Core en una FPGA, integrado a un sistema multi-Core SMP, que ejecuta distintos tipo de RdP. Esta familia de procesadores es configurable en distintos aspectos: - Tamaño del procesador (cantidad de plazas y transiciones). - Procesadores con tiempo y procesadores temporales. - Arquitectura heterogénea, que permite distribuir los recursos empleados para instanciar el procesador según se requiera, y obtener un ahorro sustancial. - La posibilidad de configurar el procesador en pos de obtener los requerimientos y minimizar los recursos. Muy valorado en la construcción de sistemas embebidos. En los sistemas con alta necesidad de concurrencia y sincronización, donde se ha evaluado este procesador, las prestaciones han mostrado una importante mejora en el desempeño. El procesador tiene la capacidad de resolver simultáneamente, por conjuntos múltiples disparos, lo que disminuye los tiempos de consulta y decisión, además los programas ejecutados cumplen con los formalismos de las RdP extendidas y sincronizadas, y los resultados de su ejecución son determinísticos. Los tiempos de respuesta para determinar una sincronización son de dos ciclos por consulta (entre la solicitud de un disparo y la respuesta).

We present a formal description of `Face Fundamental Transversals' on the faces of the Complexes of polyhedra (meaning threedimensional polytopes). A Complex of a polyhedron is the collection of the vertex points of the polyhedron, line segment edges and polygonal faces of the polyhedron. We will prove that for the faces of any 3-dimensional complex of a polyhedron under face adjacency relations, that a `Face Fundamental Transversal' exists, and it is a union of the connected orbits of faces that are intersected exactly once. While exploring the problem of finding a face fundamental transversal, we have found a partial result for edges that are incident to faces in a face fundamental transversal. Therefore we will present this partial result, as The Edge Transversal Proposition 1. We will also discuss a few conjectures that arose out this proposition. In order to reach our approaches we will first discuss some history of polyhedra, group theory, and incorporate a little crystallography, as this will appeal to various audiences.

In this thesis we present a study of the generation of abstract program models from programs in real-world programming languages that are employed in the formal verification of software. The thesis is divided into three parts, which cover distinct types of software systems, programming languages, verification scenarios, program models and properties.The first part presents an algorithm for the extraction of control flow graphs from sequential Java bytecode programs. The graphs are tailored for a compositional technique for the verification of temporal control flow safety properties. We prove that the extracted models soundly over-approximate the program behaviour w.r.t. sequences of method invocations and exceptions. Therefore, the properties that are established with the compositional technique over the control flow graphs also hold for the programs. We implement the algorithm as ConFlEx, and evaluate the tool on a number of test cases.The second part presents a technique to generate program models from incomplete software systems, i.e., programs where the implementation of at least one of the components is not available. We first define a framework to represent incomplete Java bytecode programs, and extend the algorithm presented in the first part to handle missing code. Then, we introduce refinement rules, i.e., conditions for instantiating the missing code, and prove that the rules preserve properties established over control flow graphs extracted from incomplete programs. We have extended ConFlEx to support the new definitions, and re-evaluate the tool, now over test cases of incomplete programs.The third part addresses the verification of multithreaded programs. We present a technique to prove the following property of synchronization with condition variables: "If every thread synchronizing under the same condition variables eventually enters its synchronization block, then every thread will eventually exit the synchronization". To support the verification, we first propose SyncTask, a simple intermediate language for specifying synchronized parallel computations. Then, we propose an annotation language for Java programs to assist the automatic extraction of SyncTask programs, and show that, for correctly annotated programs, the above-mentioned property holds if and only if the corresponding SyncTask program terminates. We reduce the termination problem into a reachability problem on Coloured Petri Nets. We define an algorithm to extract nets from SyncTask programs, and show that a program terminates if and only if its corresponding net always reaches a particular set of dead configurations. The extraction of SyncTask programs and their translation into Petri nets is implemented as the STaVe tool. We evaluate the technique by feeding annotated Java programs to STaVe, then verifying the extracted nets with a standard Coloured Petri Net analysis tool / Den här avhandlingen studerar automatisk konstruktion av abstrakta modeller för formell verifikation av program skrivna i verkliga programmeringsspråk. Avhandlingen består av tre delar som involverar olika typer av program, programmeringsspråk, verifikationsscenarier, programmodeller och egenskaper.Del ett presenterar en algoritm för generation av flödesgrafer från sekventiella program i Java bytekod. Graferna är skräddarsydda för en kompositionell teknik för verifikationen av temporala kontrollflödens säkerhetsegenskaper. Vi visar att de extraherade modellerna sunt överapproximerar programbeteenden med avseende på sekvenser av metodanrop och -undantag. Således gäller egenskaperna som kan fastställas genom kompositionstekniken över kontrollflöden även för programmen. Vi implementerar dessutom algoritmen i form av verktyget ConFlEx och utvärderar verktyget på ett antal testfall.Del två presenterar en teknik för att generera modeller av ofullständiga program. Det vill säga, program där implementationen av åtminstone en komponent inte är tillgänglig. Vi definierar ett ramverk för att representera ofullständiga Java bytekodsprogram och utökar algoritmen från del ett till att hantera ofullständig kod.  Därefter presenterar vi raffineringsregler - villkor för att instansiera den saknade koden - och bevisar att reglerna bevarar relevanta egenskaper av kontrollflödesgrafer. Vi har dessutom utökat ConFlEx till att stödja de nya definitionerna och har omvärderat verktyget på testfall av ofullständiga program.Del tre angriper verifikation av multitrådade program. Vi presenterar en teknik för att bevisa följande egenskap för synkronisering med vilkorsvariabler: "Om varje trådsynkronisering under samma villkor så småningom stiger in i sitt synkroniseringsblock så kommer varje tråd också till slut lämna synkroniseringen". För att stödja verifikationen så introducerar vi först SyncTask - ett enkelt mellanliggande språk för att specificera synkronisering av parallella beräkningar. Därefter presenterar vi ett annoteringsspråk för Java som tillåter automatisk extrahering av SyncTask-program och visar att egenskapen gäller om och endast om motsvarande SyncTask-program terminerar. Vi reducerar termineringsproblemet till ett nåbarhetsproblem på färgade Petrinät samt definierar en algoritm som skapar Petrinät från SyncTask-program där programmet terminerar om och endast om nätet alltid når en särskild mängd av döda konfigurationer. Extraktionen av SyncTask-program och deras motsvarande Petrinät är implementerade i form av verktyget STaVe.  Slutligen utvärderar vi verktyget genom att mata annoterade. / <p>QC 20151101</p>

Lithium ion batteries have become one of the most popular types of battery in consumer electronics as well as aerospace and automotive applications. The efficient use of Li-ion batteries in automotive applications requires well designed battery management systems. Low order Li-ion battery models that are fast and accurate are key to well- designed BMS. The control oriented low order physics based model developed previously cannot predict the temperature and predicts inaccurate voltage dynamics. This thesis focuses on two things: (1) the development of a thermal component to the isothermal model and (2) the development of a hybrid neural net and physics based battery model that corrects the output of the physics based model. A simple first law based thermal component to predict the temperature model is implemented. The thermal model offers a reasonable approximation of the temperature dynamics of the battery discharge over a wide operating range, for both a well-ventilated battery as well as an insulated battery. The model gives an accurate prediction of temperature at higher SOC, but the accuracy drops sharply at lower SOCs. This possibly is due to a local heat generation term that dominates heat generation at lower SOCs. A neural net based modeling approach is used to compensate for the lack of knowledge of material parameters of the battery cell in the existing physics based model. This model implements a neural net that corrects the voltage output of the model and adds a temperature prediction sub-network. Given the knowledge of the physics of the battery, sparse neural nets are used. Multiple types of standalone neural nets as well as hybrid neural net and physics based battery models are developed and tested to determine the appropriate configuration for optimal performance. The prediction of the neural nets in ventilated, insulated and stressed conditions was compared to the actual outputs of the batteries. The modeling approach presented here is able to accurately predict voltage output of the battery for multiple current profiles. The temperature prediction of the neural nets in the case of the ventilated batteries was harder to predict since the environment of the battery was not controlled. The temperature predictions in the insulated cases were quite accurate. The neural nets are trained, tested and validated using test data from a 4.4Ah Boston Power lithium ion battery cell. / text