Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben

2010 | Buch

Vicinity Respecting Homomorphisms for Abstracting System Requirements Kapitel lesen Erstes Kapitel lesen

Transactions on Petri Nets and Other Models of Concurrency IV

herausgegeben von: Kurt Jensen, Susanna Donatelli, Maciej Koutny

Verlag: Springer Berlin Heidelberg

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten
insite
SUCHEN

Über dieses Buch

These Transactions publish archival papers in the broad area of Petri nets and other models of concurrency, ranging from theoretical work to tool support and industrial applications. ToPNoC issues are published as LNCS volumes, and hence are widely distributed and indexed. This Journal has its own Editorial Board which selects papers based on a rigorous two-stage refereeing process. ToPNoC contains: Revised versions of a selection of the best papers from workshops and tutorials at the annual Petri net conferences; Special sections/issues within particular subareas (similar to those published in the Advances in Petri Nets series); Other papers invited for publication in ToPNoC; Papers submitted directly to ToPNoC by their authors. The fourth volume of ToPNoC contains revised and extended versions of a selection of the best papers from the workshops held at the 30th International Conference on Application and Theory of Petri Nets and Other Models of Concurrency and from the 10th Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools. The nine papers provide good coverage of a diverse range of topics including workflow systems, model checking, agent-based software systems, the state explosion problem, structure theory for Petri nets, and modal logics. ‘The volume presents a good mixture of theory, tools, and practical applications related to concurrency and gives a useful snapshot of current research.

Inhaltsverzeichnis

Frontmatter
Vicinity Respecting Homomorphisms for Abstracting System Requirements
Abstract
This paper is concerned with structuring system requirements on an abstract conceptual level. Channel/Agency Petri nets are taken as a formal model. They allow to represent functional aspects as well as data aspects of the requirements in a graphical way. Vicinity respecting homomorphisms are presented as a means to refine and abstract these nets. They preserve paths, i.e., dependencies between computational elements and they preserve important structural properties of nets, such as S- and T-components, siphons and traps and the free choice property. These properties have important interpretations for marked Petri nets and can therefore be used for the analysis of system models at more concrete levels.
Jörg Desel, Agathe Merceron
Search-Order Independent State Caching
Abstract
State caching is a memory reduction technique used by model checkers to alleviate the state explosion problem. It has traditionally been coupled with a depth-first search to ensure termination. We propose and experimentally evaluate an extension of the state caching method for general state exploring algorithms that are independent of the search order (i.e., search algorithms that partition the state space into closed (visited) states, open (to visit) states and unmet states).
Sami Evangelista, Lars Michael Kristensen
Bounded Parametric Model Checking for Elementary Net Systems
Abstract
Bounded Model Checking (BMC) is an efficient verification method for reactive systems. BMC has been applied so far to verification of properties expressed in (timed) modal logics, but never to their parametric extensions. In this paper we show, for the first time that BMC can be extended to PRTECTL – a parametric extension of the existential version of CTL. To this aim we define a bounded semantics and a translation from PRTECTL to SAT. The implementation of the algorithm for Elementary Net Systems is presented, together with some experimental results.
Michał Knapik, Maciej Szreter, Wojciech Penczek
SAT-Based (Parametric) Reachability for a Class of Distributed Time Petri Nets
Abstract
Formal methods - among them the model checking techniques - play an important role in the design and production of both systems and software. In this paper we deal with an adaptation of the bounded model checking methods for timed systems, developed for timed automata, to the case of time Petri nets. We consider distributed time Petri nets and parametric reachability checking, but the approach can be easily adapted to verification of other kinds of properties for which the bounded model checking methods exist. A theoretical description is supported by some experimental results, generated using an extension of the model checker verICS.
Wojciech Penczek, Agata Pòłrola, Andrzej Zbrzezny
Parametric Model Checking with VerICS
Abstract
The paper presents the verification system verICS, extended with the three new modules aimed at parametric verification of Elementary Net Systems, Distributed Time Petri Nets, and a subset of UML. All the modules exploit Bounded Model Checking for verifying parametric reachability and the properties specified in the logic PRTECTL – the parametric extension of the existential fragment of CTL.
Michał Knapik, Artur Niewiadomski, Wojciech Penczek, Agata Półrola, Maciej Szreter, Andrzej Zbrzezny
Schedule-Aware Workflow Management Systems
Abstract
Contemporary workflow management systems offer work-items to users through specific work-lists. Users select the work-items they will perform without having a specific schedule in mind. However, in many environments work needs to be scheduled and performed at particular times. For example, in hospitals many work-items are linked to appointments, e.g., a doctor cannot perform surgery without reserving an operating theater and making sure that the patient is present. One of the problems when applying workflow technology in such domains is the lack of calendar-based scheduling support. In this paper, we present an approach that supports the seamless integration of unscheduled (flow) and scheduled (schedule) tasks. Using CPN Tools we have developed a specification and simulation model for schedule-aware workflow management systems. Based on this a system has been realized that uses YAWL, Microsoft Exchange Server 2007, Outlook, and a dedicated scheduling service. The approach is illustrated using a real-life case study at the AMC hospital in the Netherlands. In addition, we elaborate on the experiences obtained when developing and implementing a system of this scale using formal techniques.
Ronny S. Mans, Nick C. Russell, Wil M. P. van der Aalst, Arnold J. Moleman, Piet J. M. Bakker
On-the-Fly Auditing of Business Processes
Abstract
Information systems supporting business processes are usually very complex. If we have to ensure that certain business rules are enforced in a business process, it is often easier to design a separate system, called a monitor, that collects the events of the business processes and verifies whether the rules are satisfied or not. This requires a business rule language (BRL) that allows to verify business rules over finite histories. We introduce such a BRL and show that it can express many common types of business rules. We introduce two interesting properties of BRL formulas: the future stability and the past stability. The monitor should be able to verify the business rules over the complete history, which is increasing over time. Therefore we consider abstractions of the history. Actually we generate from a set of business rules a labeled transition system (with countable state space) that can be executed by the monitor if each relevant event of the business process triggers a step in the labeled transition system. As long as the monitor is able to execute a step, the business rules are not violated. We show that for a sublanguage of BRL, we can transform the labeled transition system into a colored Petri net such that verification becomes independent of the history length.
Kees van Hee, Jan Hidders, Geert-Jan Houben, Jan Paredaens, Philippe Thiran
Modeling Organizational Units as Modular Components of Systems of Systems
Abstract
Modern software systems are frequently characterized as systems of systems. Agent-orientation as a software engineering paradigm exhibits a high degree of qualification for addressing many of the accompanying challenges. However, when it comes to a hierarchical/recursive system decomposition, classical agent orientation reaches its limits. We propose the concept of an organizational unit that both embeds actors and is itself embedded as a collective actor in surrounding organizational units. Building upon previous publications that feature an abstract model of organizational units, we supply it with a precise operational semantics in this paper.
Matthias Wester-Ebbinghaus, Daniel Moldt, Michael Köhler-Bußmeier
A Multi-Agent Organizational Framework for Coevolutionary Optimization
Abstract
This paper introduces DAFO, a Distributed Agent Framework for Optimization that helps in designing and applying Coevolutionary Genetic Algorithms (CGAs). CGAs have already proven to be efficient in solving hard optimization problems, however they have not been considered in the existing agent-based metaheuristics frameworks that currently provide limited organization models. As a solution, DAFO includes a complete organization and reorganization model, Multi-Agent System for EVolutionary Optimization (MAS4EVO), that permits to formalize CGAs structure, interactions and adaptation. Examples of existing and original CGAs modeled using MAS4EVO are provided and an experimental proof of their efficiency is given on an emergent topology control problem in mobile hybrid ad hoc networks called the injection network problem.
Grégoire Danoy, Pascal Bouvry, Olivier Boissier
Backmatter
Metadaten
Titel
Transactions on Petri Nets and Other Models of Concurrency IV
herausgegeben von
Kurt Jensen
Susanna Donatelli
Maciej Koutny
Copyright-Jahr
2010
Verlag
Springer Berlin Heidelberg
Electronic ISBN
978-3-642-18222-8
Print ISBN
978-3-642-18221-1
DOI
https://doi.org/10.1007/978-3-642-18222-8

Premium Partner

    Bildnachweise