No description available.

Process modelling is a design approach where a system or procedure is decomposed in a number of abstract, independent, but connected processes, and then recomposed into a well-defined workflow specification. Research in formal verification, for its part, and theorem proving in particular, is focused on the rigorous verification of system properties using logical proof. This thesis introduces a systematic methodology for process modelling and composition based on formal verification. Our aim is to augment the numerous benefits of a workflow based specification, such as modularity, separation of concerns, interoperability between heterogeneous (including human-based) components, and optimisation, with the high level of trust provided by formally verified properties, such as type correctness, systematic resource accounting (including exception handling), and deadlock-freedom. More specifically, we focus on bridging the gap between the deeply theoretical proofs-as-processes paradigm and the highly pragmatic tasks of process specification and composition. To accomplish this, we embed the proofs-as-processes paradigm within the modern proof assistant HOL Light. This allows the formal, mechanical translation of Classical Linear Logic (CLL) proofs to p-calculus processes. Our methodology then relies on the specification of abstract processes in CLL terms and their composition using CLL inference. A fully diagrammatic interface is used to guide our developed set of high level, semi-automated reasoning tools, and to perform intuitive composition actions including sequential, parallel, and conditional composition. The end result is a p-calculus specification of the constructed workflow, with guarantees of correctness for the aforementioned properties. We can then apply a visual, step-by-step simulation of this workflow or perform an automated workflow deployment as executable code in the programming language Scala. We apply our methodology to a use-case of a holiday booking web agent and to the modelling of real-world collaboration patterns in healthcare, thus demonstrating the capabilities of our framework and its potential use in a variety of scenarios.

In global energy and industrial market, petroleum refining industry accounts for a major share. Through proper planning and the use of adequate mathematical models for the different processing units, many profit improving opportunities can be realized. The increasing crude oil price has also made refining of crude oil blends to be a common practice. This thesis aims to provide useful insight for planning of the integrated refinery subsystems. The main subsystems referred to are (1) The crude oil unloading subsystem (2) The production and product blending subsystem and (3) The product distribution subsystem. Aspen HYSYS® was first used to develop a rigorous model for crude distillation unit (CDU) and vacuum distillation unit (VDU). The rigorous model was validated with pilot plant data from literature. The information obtained from the rigorous model is further used to develop a model for planning of the CDU and VDU. This was combined with models (obtained from empirical correlations) for fluid catalytic cracker (FCC) and hydrotreater (HDT) units to form a mathematical programming planning model used for refinery production and product blending subsystem planning. Since two different types of crude were considered, the optimum volumetric mixing ratio, the sulphur content at that mixing ratio and the CDU flow rate were determined. The yields fraction obtained from the rigorous model were then used to generate regression model using least square method. The sulphur composition of the crude oil was used as independent variable in the regression model. The generated regression models were then used to replace the regular fixed yield approach in a refinery planning model and the results compared. From the results obtained, the proposed method provided an alternative and convenient means for estimating yields from CDU and VDU than the regular fixed yield approach. The proposed aggregate model for the production and products blending subsystem was integrated with the modified scheduling model for the crude unloading subsystem developed by Lee et al. (1996) and products distribution model developed by Alabi and Castro (2009) for refinery planning. It was found that the regression model could be integrated in a refinery planning model and that the CDU flow rate was maximised as compared to the non- integrated system.

In global energy and industrial market, petroleum refining industry accounts for a major share. Through proper planning and the use of adequate mathematical models for the different processing units, many profit improving opportunities can be realized. The increasing crude oil price has also made refining of crude oil blends to be a common practice. This thesis aims to provide useful insight for planning of the integrated refinery subsystems. The main subsystems referred to are (1) The crude oil unloading subsystem (2) The production and product blending subsystem and (3) The product distribution subsystem. Aspen HYSYS® was first used to develop a rigorous model for crude distillation unit (CDU) and vacuum distillation unit (VDU). The rigorous model was validated with pilot plant data from literature. The information obtained from the rigorous model is further used to develop a model for planning of the CDU and VDU. This was combined with models (obtained from empirical correlations) for fluid catalytic cracker (FCC) and hydrotreater (HDT) units to form a mathematical programming planning model used for refinery production and product blending subsystem planning. Since two different types of crude were considered, the optimum volumetric mixing ratio, the sulphur content at that mixing ratio and the CDU flow rate were determined. The yields fraction obtained from the rigorous model were then used to generate regression model using least square method. The sulphur composition of the crude oil was used as independent variable in the regression model. The generated regression models were then used to replace the regular fixed yield approach in a refinery planning model and the results compared. From the results obtained, the proposed method provided an alternative and convenient means for estimating yields from CDU and VDU than the regular fixed yield approach. The proposed aggregate model for the production and products blending subsystem was integrated with the modified scheduling model for the crude unloading subsystem developed by Lee et al. (1996) and products distribution model developed by Alabi and Castro (2009) for refinery planning. It was found that the regression model could be integrated in a refinery planning model and that the CDU flow rate was maximised as compared to the non- integrated system.

The goal of the thesis is to evaluate if developed phase chemical process models for cement clinker and lime production processes are reliable to use as predictive tools in understanding the changes when introducing sustainability measures. The thesis describes the development of process simulation models in the application of sustainability measures as well as the evaluation of these models. The motivation for developing these types of models arises from the need to predict the chemical and the process changes in the production process, the impact on the product quality and the emissions from the flue gas. The main chemical reactions involving the major elements (calcium, silicon, aluminium and iron) are relatively well known. As for the minor elements, such as sodium and potassium metals, sulphur, chlorine, phosphorus and other trace elements, their influence on the main reactions and the formation of clinker minerals is not entirely known. When the concentrations of minor and trace elements increase due to the use of alternative materials and fuels, a model that can accurately predict their chemistry is invaluable. For example, the shift towards using less carbon intensive fuels and more biomass fuels often leads to an increased phosphorus concentration in the products. One way to commit to sustainable development methods in cement clinker and lime production is to use new combustion technologies, which increase the ability to capture carbon dioxide. Introducing oxy-fuel combustion achieves this, but at the same time, the overall process changes in many other ways. Some of these changes are evaluated by the models in this work. In this thesis, a combination of the software programs Aspen Plus™ and ChemApp™ constitutes the simulation model. Thermodynamic data from FACT are evaluated and adjusted to suit the chemistry of cement clinker and lime. The resulting model has been verified for one lime and two cement industrial processes. Simulated scenarios of co-combustion involving different fuels and different oxy-fuel combustion cases in both cement clinker and lime rotary kiln production are described as well as the influence of greater amounts of phosphorus on the cement clinker quality.

The planning and scheduling of appropriate resources is essential in engineering design for delivering quality products on time, within cost and at acceptable risk. There is an inherent complexity in deciding what resources should perform which tasks taking into account their effectiveness towards completing the task, whilst adjusting to their availabilities. The right resources must be applied to the right tasks in the correct order. In this context, process modelling and simulation could aid in resource management decision making. However, most approaches define resources as elements needed to perform the activities without defining their characteristics, or use a single classification such as human designers. Other resources such as computational and testing resources, amongst others have been overlooked during process planning stages. In order to achieve this, literature and empirical investigations were conducted. Firstly, literature investigations focused on what elements have been considered design resources by current modelling approaches. Secondly, empirical studies characterised key design resources, which included designers, computational, testing and prototyping resources. The findings advocated for an approach that allows allocation flexibility to balance different resource instances within the process. In addition, capabilities to diagnose the impact of attaining specific performance to search for a preferred resource allocation were also required. Therefore, the thesis presents a new method to model different resource types with their attributes and studies the impact of using different instances of those resources by simulating the model and analysing the results. The method, which extends a task network model, Applied Signposting Model (ASM), with Bayesian Networks (BN), allows testing the influence of using different resources combinations on process performance. The model uses BN within each task to model different instances of resources that carries out the design activities (computational, designers and testing) along with its configurable attributes (time, risk, learning curve etc.), and tasks requirements. The model was embedded in an approach and was evaluated by applying it to two aerospace case studies. The results identified insights to improve process performance such as the best performing resource combinations, resource utilisation, resource sensitive activities, the impact of different variables, and the probability of reaching set performance targets by the different resource instances.

Over the past three decades, modelling packages for chemical processes have become more advanced and widely used. For example, equation-oriented dynamic simulators, such as gPROMS are useful for simulating plantwide processes as well as unit operations, and are widely used by process engineers. Whereas, other types of simulator (e.g. Simulink) are often used by control engineers to solve complex control problems. However, both these types of simulator rely on the user being proficient in modelling and familiar with their syntax beforehand. A useful development would be the integration of some knowledge into the formation of the process models and automatic syntax code generation. This would lead to the design engineers having a library of knowledge to check on first, much as an expert engineer uses their past experiences to help guide them through a design. If this could be incorporated into a modelling interface this would greatly help the design engineer, especially when tackling problems in areas that they have little, or no experience. The thesis addresses this problem and describes the design of an intelligent modelling interface that incorporates a knowledge base using some form of a priori case library and recall facility. The interface also incorporates an automatic input file generation stage. At present, the user can: specify a single unit operation problem to search for, retrieve similar cases from the database, specify their solution in the database based on past cases and experience, and then automatically generate an input file for either gPROMS or Simulink. These features are demonstrated through four case studies.

Thesis (MScEng (Industrial Engineering))--University of Stellenbosch, 2010. / ENGLISH ABSTRACT: Concurrent and distributed business processes are becoming the norm in many organisations. Current modelling techniques do not address the problems faced by concurrent business processes sufficiently. We showhowmodel checking is applied to business processes to prove behavioural properties to address the aforementioned shortcomings. A method of abstraction is required to construct business process models that can be model checked. In this thesis we show the suitability of the Logical Thinking Process as an abstraction tool. We call the combination of the Logical Thinking Process and model checking the Complexity Alleviation Method (CAM). We apply CAM to two well-known supply chain and manufacturing problems, and insightful results are obtained. This leads us to the conclusion that CAM allows for the quicker modelling of business processes, as well as providing problem-specific and proven solutions in amanner not possible with simulation or other techniques. / AFRIKAANSE OPSOMMING: Gelyklopende en verspreide besigheidsprosesse word ’n alledaagse verskynsel in menigte instansies. Huidige modelleringstegnieke is nie in staat om die probleme geassosieer met gelyklopende besigheidsprosesse aan te spreek nie. Ons wys hoe model model verifikasie (“model checking”) toegepas word op besigheidsprosesse om gedragseienskappe te bewys en sodoende die voorgenoemde tekortkominge aan te spreek. ’nMetode van abstraksie word benodig ombesigheidsprosesmodelle, wat verifieerbaar is, te konstrueer. In hierdie verhandeling word die geskiktheid van die Logiese Denkproses (“the Logical Thinking Process”) as abstraksie gereedskap aangetoon. Ons noem die kombinasie van die Logiese Denkproses en model verifikasie Kompleksiteitsverligtingsmetodologie (CAM). Ons pas CAM op twee welbekende aanbodketting- en vervaardigingsprobleme toe en insiggewende resultate is verkry. Dit lei ons tot die gevolgtrekking dat CAM vinniger konstruering van modelle te weeg bring, sowel as probleem spesifieke en bewysbare oplossings verskaf wat nie moontlik ismet simulasie of ander tegnieke nie.

Yes / The process of generating FMEA following document-centric approach is tedious and susceptible to human error. This paper presents preliminary methodology for robotic manufacturing process modelling in MBSE environment with a scope of automating multiple steps of the modelling process using ontology. This is followed by the reasoning towards automatic generation of process FMEA from the MBSE model. The proposed methodology allows to establish robust and self-synchronising links between process-relevant information, reduce the likelihood of human error, and scale down time expenses.

This bachelor thesis deals with the subject of business process modelling in an outsourced environment. The communication process between two parties that are on either side of the globe can be problematic and affect the quality of the system requirements. The background of this study is that there is a lack of communication between these parties, which will eventuate in poor results.   The purpose of this study is to find out whether it is possible to make use of business process modelling in an outsourced environment in order to increase the quality of system requirements by bringing the two parties closer together with help of a common language. A qualitative approach was used to interview relevant informants at Länsförsäkringar AB and its business units Länsförsäkringar Liv and Länsförsäkringar Bank.   We have identified that it is not necessarily the system requirements that have a poor quality but how these system conveyed to the external supplier. Based on our data collection, we realized the great benefits of business process modelling as a means of communication in the system development, which can be a huge advantage in an outsourced environment. According to our study, it is certain that a business process modelling with mapped processes and flow charts can support communication as a common language because of the creation of processes and images instead of text.