Egon Börger

Endlich liegt der ,,Klassiker" der Theoretischen Informatik, der Studenten und Forschern ein unentbehrliches Standardwerk ist, in neuer Auflage vor.

Algorithmen, Sprachen und Kalküle unter besonderer Berücksichtigung ihrer Komplexität

Berechenbarkeit Komplexität Logik

Christoph Beierle

Correctness Proof for the WAM with Types

Michael Butler

Jonathan P. Bowen

Paul Boca

The ABZ 2008 conference was held in London during September 16–18, 2008. The conference aimed at contributing to the cross-fertilization of three rigorous methods that share a common conceptual foundation and are widely used in both academia and industry for the design and analysis of hardware and so- waresystems,namely,abstractstate machines,B, andZ. It followedonfromthe Dagstuhl seminar on Rigorous Methods for Software Construction and Ana- sis, which was organized in May 2006 by Jean-Raymond Abrial (ETH Zur ¨ ich, Switzerland) and Uwe Gl¨ asser (Simon Fraser University – Burnaby, Canada), and brought together researchers from the ASM and the B community (see: http://www. dagstuhl. de/06191). The conference simultaneously incorporated the 15th International ASM Workshop, the 17th International Conference of Z Users and the 8th Inter- tional Conference on the B Method, which were present with separate Program Committees to select the papers published in separate tracks (see Chapters 2–4 of these proceedings). The conference covered a wide range of researchspanning from theoretical and methodological foundations to tool support and practical applications. It was split into three main parts: – Aone-daycommonprogramoffourinvitedlectures,seeChap. 1ofthesep- ceedings,and the presentationof three papers selected among the submitted contributions – Two days of contributed research papers and short presentations of work in progress, of industrial experience reports and of tool demonstrations, as documented in Chap.

First International Conference, ABZ 2008, London, UK, September 16-18, 2008. Proceedings

Abstract State Machines, B and Z

Joachim Schmid

Robert F. Stärk

The origin of this book goes back to the Dagstuhl seminar on Logic for System Engineering, organized during the first week of March 1997 by S. Jiihnichen, J. Loeckx, and M. Wirsing. During that seminar, after Egon Borger's talk on How to Use Abstract State Machines in Software Engineering, Wolfram Schulte, at the time a research assistant at the University of Ulm, Germany, questioned whether ASMs provide anything special as a scientifically well founded and rigorous yet simple and industrially viable framework for high level design and analysis of complex systems, and for natural refinements of models to executable code. Wolfram Schulte argued, referring to his work with K. Achatz on A Formal Object-Oriented Method Inspired by Fusion and Object-Z [1], that with current techniques of functional programming and of axiomatic specification, one can achieve the same result. An intensive and long debate arose from this discussion. At the end of the week, it led Egon Borger to propose a collaboration on a real-life specification project of Wolfram Schulte's choice, as a comparative field test of purely functional declarative methods and of their enhancement within an integrated abstract state-based operational (ASM) approach. After some hesitation, in May 1997 Wolfram Schulte accepted the offer and chose as the theme a high-level specification of Java and of the Java Virtual Machine.

Definition, Verification, Validation

Java and the Java Virtual Machine

Werner Schmidt

Albert Fleischmann

Christian Stary

Stefan Obermeier

Activities performed in organizations are coordinated via communication between the people involved. The sentences used to communicate are naturally structured by subject, verb, and object. The subject describes the actor, the verb the action and the object what is affected by the action. Subject-oriented Business Process Management (S-BPM) as presented in this book is based on this simple structure which enables process-oriented thinking and process modeling. S-BPM puts the subject of a process at the center of attention and thus deals with business processes and their organizational environment from a new perspective, meeting organizational requirements in a much better way than traditional approaches. Subjects represent agents of an action in a process, which can be either technical or human (e.g. a thread in an IT system or a clerk). A process structures the actions of each subject and coordinates the required communication among the subjects. S-BPM provides a coherent procedural framework to model and analyze business processes: its focus is the cooperation of all stakeholders involved in the strategic, tactical, and operational issues, sharing their knowledge in a networked structure. The authors illustrate how each modeling activity through the whole development lifecycle can be supported through the use of appropriate software tools. The presentation style focuses on professionals in industry, and on students specializing in process management or organizational modeling. Each chapter begins with a summary of key findings and is full of examples, hints, and possible pitfalls. An interpreter model, a toolbox, and a glossary summarizing the main terms complete the book. The web site www.i2pm.net provides additional software tools and further material.

Subject-Oriented Business Process Management

Hans Kleine Büning

This volume contains the revised versions of 28 papers presented at the third workshop on Computer Science Logic held in Kaiserslautern, FRG, October 2-6, 1989. These proceedings cover a wide range of topics both from theoretical and applied areas of computer science. More specifically, the papers deal with problems arising at the border of logic and computer science, e.g. in complexity, data base theory, logic programming, artificial intelligece, and temporal logic. The volume should be of interest to all logicians and computer scientists working in the above field.

3rd Workshop on Computer Science Logic. Kaiserslautern, FRG, October 2-6, 1989. Proceedings

CSL '89

Michael M. Richter

This volume contains the papers which were presented to the workshop "Computer-Science Logic" held in Karlsruhe on October 12-16, 1987. Traditionally Logic, or more specifically, Mathematical Logic splits into several subareas: Set Theory, Proof Theory, Recursion Theory, and Model Theory. In addition there is what sometimes is called Philosophical Logic which deals with topics like nonclassical logics and which for historical reasons has been developed mainly at philosphical departments rather than at mathematics institutions. Today Computer Science challenges Logic in a new way. The theoretical analysis of problems in Computer Science for intrinsic reasons has pointed back to Logic. A broad class of questions became visible which is of a basically logical nature. These questions are often related to some of the traditional disciplines of Logic but normally without being covered adequately by any of them. The novel and unifying aspect of this new branch of Logic is the algorithmic point of view which is based on experiences people had with computers. The aim of the "Computer-Science Logic" workshop and of this volume is to represent the richness of research activities in this field in the German-speaking countries and to point to their underlying general logical principles.

1st Workshop on Computer Science Logic, Karlsruhe, FRG, October 12-16, 1987. Proceedings

CSL '87

This state-of-the-art survey gives a systematic presentation of recent advances in the design and validation of computer architectures. The book covers a comprehensive range of architecture design and validation methods, from computer aided high-level design of VLSI circuits and systems to layout and testable design, including the modeling and synthesis of behavior and dataflow, cell-based logic optimization, machine assisted verification, and virtual machine design.

Architecture Design and Validation Methods

In Memory of Dieter Rötting. 24.8.1937 - 4.6.1984. On the Occasion of the 50th Anniversary of His Birth

Computation Theory and Logic

Yuri Gurevich

Karl Meinke

This volume presents the proceedings of the Fourth International Workshop on Analogical and Inductive Inference (AII '94) and the Fifth International Workshop on Algorithmic Learning Theory (ALT '94), held jointly at Reinhardsbrunn Castle, Germany in October 1994. (In future the AII and ALT workshops will be amalgamated and held under the single title of Algorithmic Learning Theory.) The book contains revised versions of 45 papers on all current aspects of computational learning theory; in particular, algorithmic learning, machine learning, analogical inference, inductive logic, case-based reasoning, and formal language learning are addressed.

7th Workshop, CSL '93, Swansea, United Kingdom, September 13 - 17, 1993. Selected Papers

Computer Science Logic

Robert Stärk

A Method for High-Level System Design and Analysis

Abstract State Machines

This volume contains the papers which were presented at the second workshop "Computer Science Logic" held in Duisburg, FRG, October 3-7, 1988. These proceedings cover a wide range of topics both from theoretical and applied areas of computer science. More specifically, the papers deal with problems arising at the border of logic and computer science: e.g. in complexity, data base theory, logic programming, artificial intelligence, and concurrency. The volume should be of interest to all logicians and computer scientists working in the above fields.

2nd Workshop on Computer Science Logic, Duisburg, FRG, October 3-7, 1988. Proceedings

CSL'88

This book constitutes the refereed proceedings of the First International Conference of Abstract State Machines, B and Z, ABZ 2008, held in London, UK, in September 2008. The conference simultaneously incorporated the 15th International ASM Workshop, the 17th International Conference of Z Users and the 8th International Conference on the B Method. The 44 revised full papers presented together with 4 invited contributions were carefully reviewed and selected from numerous submissions. The conference fosters the cross-fertilization of three rigorous methods for the design and analysis of hardware and software systems - both in academia and industry - namely Abstract State Machines, B, and Z. Covering a wide range of research spanning from theoretical and methodological foundations to tool support and practical applications, the contributions are organized in topical sections on abstract state machines, B papers, Z papers, ABZ short papers, and the papers of the Verified Software Repository Network (VSR-net) workshop.

Alexander Raschke

This book uses a variety of applications to illustrate a modeling method that helps practitioners to manage complex software-intensive systems. The proposed method relies on the combination of its abstraction concept and its operational character, with behavioral models in the precise and simple form of Abstract State Machines (ASMs). The book introduces both the modeling method (Part I) and the available tool support (Part II): In Part I the authors detail (using numerous examples) how to construct, explain, debug, explore, extend and reuse accurate system design models, starting from scratch. Only an elementary knowledge of common mathematical (including set-theoretic) notation and some basic experience with computational processes (systems, programs, algorithms) is assumed. Part II then shows how the modeling method can be supported by implementing tools that make design models executable and debuggable. To illustrate how to build, debug and maintain systems and to explain their construction in a checkable manner, a general, problem-oriented refinement method is adopted to construct system models from components. The method starts with abstract models and refines them step by step, incrementally adding further details that eventually lead to code. Intended for practitioners who build software intensive systems, and students specializing in software engineering, it can be used both for self-study and for teaching, and it can serve as a reference book. Exercises are included to help readers check their understanding of the explained concepts. For many models defined in the book, refinements to executable versions can be downloaded for experimental validation from the book’s website at http://modelingbook.informatik.uni-ulm.de

Egon Börger

About

Books

Join the club