1,721,111 research outputs found
Object-oriented approach for dynamic system modelling and simulation
No full textSoftware engineering always cares to provide solutions for building applications as close as possible to what they should be, according to the requirements and the final users needs. Systems behavior simulation is a very common application to virtually reproduce and often predict the real-world behavior. Simulation is one of the most operational research tool in a large variety of engineering and scientific domains: Transport, telecommunication, medicine, chemical processes, physics, etc. The complexity of such application is relative to the increasing complexity of the systems. In this context, it is relevant to bring together different tools and formalisms such as markovian chain, Petri nets, etc., to improve the existent approaches and so to answer the simulations performances needs. The principle objective of this thesis is to bring together techniques from software engineering and safety engineering in order to improve the state of the art of modeling and simulation of dynamic systems in the industrial context. In addressing this objective, this work initially involves defining the essential limitations of the used formalisms, methods and tools regarding from one hand the software engineering modeling and simulation techniques and from the other hand the existent risk analysis methodologies. This work is conducted with respect to the problem of danger identification, considering the context of the complex systems behavior and their interaction with the human operator. In software engineering, it is well known that Petri/high-level nets have attractive characteristics to be used in systems simulation and behavior prediction such as the natural graphical representation, and their well-defined semantic. They are well-suited for the description of complex situations with concurrency (interleaving and true concurrency depending on the underlying semantics), conflict and confusion. However, the absence of structuring capabilities has been one of the main criticisms raised against Petri nets/high-level nets. Thus, there have been many attempts to introduce structuring principles in nets of this kind [BCM88] [Kie89] [JR91]. The attractive characteristics of Petri/high-level nets have prompted researchers to enrich these formalisms with object-oriented features. CO-OPN (Concurrent Object-Oriented Petri Net) approach, brings together the power of both Petri/high-level nets and object-orientation techniques, it has been devised so as to offer an adequate framework for the specification and design of large scale concurrent system [BG91]. CO-OPN, as a powerful modeling tool, has been used in a limited way to simulate systems. This work aims to provide a CO-OPN extension to allow a more realistic systems' simulation. Actually, its simulator semantic uses to be a suitable approach for modeling near closed systems and software components, because they need to loose coupling with external world. But, when we model more realistic problems like industrial processes, where human interaction is a relevant event, this approach is not sufficient to catch all system activity attributes. Moreover, the CO-OPN interpretation process does not allow interaction with the object internal states. This work provides a new solution to overcome CO-OPN simulation limitations and a set of prototypes to assist dynamic systems simulations. Furthermore, this work has been conducted in a Risk Analysis (RA) context, a domain where computer-based simulations research are of utmost interest. Actually, classical approaches used to address complex workplace hazard in a limited way, using checklists or sequence models. Moreover, the use of single oriented methods, such as AEA (man-oriented), FMEA (machine oriented) or HAZOP (process oriented), is not satisfactory to overcome the increasing sophistication of industrial processes. The automation of a part of the analysis process as well as the multiple-oriented approach allowed by dynamic modeling may indeed enhance significantly the analysis completeness and reduce the time analyzing time. This work, based on Object Oriented Petri net formalism (CO-OPN), propose an alternative multi-oriented approach where existent methods limitations have been criticized to develop a dynamic model, MORM (Man-machine Occupational Risk Modeling). A real industrial system (metal wire making process) has been specified to implement the different approach steps (system identification, model application, system simulation, system analysis)
Generation of object-oriented programs from CO-OPN specifications
No full textThe execution of formal specifications is important for verification, validation and animation purposes. This thesis describes transformation of CO-OPN specifications in executable code. The original goal of this transformation was validation by prototyping, but animation and, partially, verification also became interesting goals during the development. The work was already done to study the transformation of CO-OPN specifications to Prolog programs [18], to ADA programs [37] and even to Java programs [57]. Nevertheless the only implemented technique was the transformation to Prolog. Starting with those results, we designed and implemented the automatic transformation of CO-OPN specifications to Java programs. The main contributions of this work are: Definition and implementation of CO-OPN state and execution models. Study and implementation of various methods to integrate generated code with external systems. Implementation of an extensible code generator. This thesis first gives a brief introduction to CO-OPN language, then describes main principles that govern the transformation of CO-OPN to executable code. This explanation is logically divided in three parts, corresponding to main CO-OPN entities: generation of Abstract Data Types, Classes and Contexts. Then the architecture of code generation engine is presented. Finally, integration of generated code is illustrated by comprehensive examples.LG
Flexible subtyping relations for component-oriented formalisms and their verification
No full textIn this thesis we address the problem of safe substitutability in mobile component-oriented formalisms. We try to give a solution for different definitions of "safe" through a new notion of subtyping based on flexibility and observation. The aim is to have a definition which is applicable to a large numbers of existing formalisms, and which itself may be seen as an abstraction of many existing definitions of subtyping. In a similar way, we also try to see the verification of such relations in a way that may be applicable to many formalisms, and which may be seen as "containing" many existing techniques. Our hope is that our work may link these subtype definitions or verification techniques to formalisms they were not originally designed for. The contribution of this thesis can be divided in several points. First of all, the full formal definition of a "descriptive" component-oriented formalism based on concurrency, non determinism, complex composition and mobility. Also, the definition of a general flexible notion of subtyping, as well as a more particular example. Verification techniques for these subtyping relations are also grouped under the concept of component transformation, which is shown to include many other works. Finally, to illustrate the main concepts of our work, we provide a case study with a model of a "mobile" drinks dispenser.LG
Going Beyond Counting First Authors in Author Co-citation Analysis
Get PDFThe present study examines one of the fundamental aspects of author co-citation analysis (ACA) - the way co-citation
counts are defined. Co-citation counting provides the data on which all subsequent statistical analyses and mappings
are based, and we compare ACA results based on two different types of co-citation counting - the traditional type that
only counts the first one among a cited work's authors on the one hand and a non-traditional type that takes into
account the first 5 authors of a cited work on the other hand. Results indicate that the picture produced through this non-traditional author co-citation counting contains more coherent author groups and is therefore considerably clearer. However, this picture represents fewer specialties in the research field being studied than that produced through the traditional first-author co-citation counting when the same number of top-ranked authors is selected and analyzed. Reasons for these effects are discussed
High-level Petri net model checking : the symbolic way
No full textAlthough model checking is heavily used in the hardware domain, its use is not mainstream in software engineering yet. Modeling of software system is tedious using low-level formalisms such as Place/Transition Petri Nets. Moreover, usual verification techniques (e.g., state space analysis) are often intractable because of the infamous State Space Explosion. While modeling can be eased by using high-level formalisms such as High- level Petri Nets that make models more concise and more readable, State Space Explosion is still an important challenge. Many authors have tackled this issue on High-level Petri Nets, mostly by either modularizing the system or by reducing the states to consider (e.g., partial orders, symmetries). Most of those approaches encode the state space explicitly, i.e., the required amount of memory is linear to the number of states, which is rapidly intractable due to State Space Explosion. Symbolic Model Checking partially overcomes this problem by encoding the state space in a condensed way using Decision Diagrams and has been success- fully applied to Place/Transition Petri Nets. Albeit very effective, to be applied to High-level Petri Nets, these techniques require to “unfold” the High-level Petri Nets to an equivalent Petri nets. This is sometimes impractical because it might be difficult, if not infeasible, to figure out the data types boundaries. To partially overcome these problems, we propose to apply Symbolic Model Checking at the High-level Petri Net level directly. To that end, we propose the S Decision Diagrams a kind of Decision Diagrams especially created to han- dle large sets of terms representing the instances of the data types. Besides, we introduce the notion of Partial Net Unfolding that avoids having to unfold all data types prior model checking. Moreover, we describe Algebraic Clustering that adapts the concept of clustering to High-level Petri Nets and therefore that allows to apply advanced techniques such as saturation. These contributions pave the way to the application of Symbolic Model Checking to modular extensions of the High-level Petri Net. Finally, as a proof of concept, we implemented all the proposed techniques in a model checker called the Algebraic Petri Nets Analyzer
Revisiting memory assignment semantics in imperative programming languages
No full textThis thesis studies the semantics of imperative programming languages. In particular, it explores the relationship between the syntax and semantics of memory assignment. The contributions are threefold. First, I developed a theoretical programming language, called the assignment calculus, to uniformly express the assignment semantics of imperative programming languages. Second, I formalized common memory errors (e.g. access to uninitialized memory and memory leaks) in the context of this language, and provided dynamic and static approaches to prevent them. Third, I developed a general purpose programming language called Anzen, based on the theoretical foundation of the assignment calculus
SATEL — A test intention language for object-oriented specifications of reactive systems
No full textCette thèse traite de la problématique de la génération de jeux de tests à partir d'une spécification logicielle. En particulier nous nous intéresserons au langage de spécification CO-OPN(Concurrent Object-Oriented Petri Nets) [1, 2], basé sur les réseaux algébriques étendus grâce à des méchanismes objets et de distribution. Pour traiter ce problème nous avons dû revoir le langage CO-OPN. En effet la sémantique du langage ayant été définie par itérations successives, celle-ci s'est avérée inadaptée à la génération de jeux de tests. Nous proposons à travers notre travail une nouvelle version de CO-OPN où la syntaxe et la sémantique ont été complètement revues et qui intègrent les travaux précédents où des descriptions précises et formelles ont été employés..
- …
