Manfred Broy Libri

Testing is the primary hardware and software verification technique used by industry today. Usually, it is ad hoc, error prone, and very expensive. In recent years, however, many attempts have been made to develop more sophisticated formal testing methods. This coherent book provides an in-depth assessment of this emerging field, focusing on formal testing of reactive systems. This book is based on a seminar held in Dagstuhl Castle, Germany, in January 2004. It presents 19 carefully reviewed and revised lectures given at the seminar in a well-balanced way ensuring competent complementary coverage of all relevant aspects. An appendix provides a glossary for model-based testing and basics on finite state machines and on labelled transition systems. The lectures are presented in topical sections on testing of finite state machines, testing of labelled transition systems, model-based test case generation, tools and case studies, standardized test notation and execution architectures, and beyond testing.

A lucid statement of the philosophy of modular programming can be found in a 1970 textbook on the design of system programs by Gouthier and Pont [1, l Cfl0. 23], which we quote below: A well-defined segmentation of the project effort ensures system modularity. Each task fonos a separate, distinct program module. At implementation time each module and its inputs and outputs are well-defined, there is no confusion in the intended interface with other system modules. At checkout time the in tegrity of the module is tested independently; there are few sche duling problems in synchronizing the completion of several tasks before checkout can begin. Finally, the system is maintained in modular fashion; system errors and deficiencies can be traced to specific system modules, thus limiting the scope of detailed error searching. Usually nothing is said about the criteria to be used in dividing the system into modules. This paper will discuss that issue and, by means of examples, suggest some criteria which can be used in decomposing a system into modules. A Brief Status Report The major advancement in the area of modular programming has been the development of coding techniques and assemblers which (1) allow one modu1e to be written with little knowledge of the code in another module, and (2) alJow modules to be reas sembled and replaced without reassembly of the whole system.

Software development for the automotive domain has become the enabling te- nologyforalmostallsafety-criticalandcomfortfunctionso? eredtothecustomer. Ninety percentofallinnovations inautomotive systems aredirectly or indirectly enabled by embedded software. The numbers of serious accidents have declined in recent years, despite constantly increasing tra? c; this is correlated with the introduction of advanced, software-enabled functionality for driver assistance, such as electronic stability control. Software contributes signi? cantly to the - tomotive value chain. By 2010 it is estimated that software will make up 40% of the value creation of automotive electrics/electronics. However, with the large number of software-enabled functions, their int- actions, and the corresponding networking and operating infrastructure, come signi? cant complexities both during the automotive systems engineering p- cess and at runtime. A central challenge for automotive systems development is the scattering of functionality across multiple subsystems, such as electronic control units (ECUs) and the associated networks. As an example, consider the central locking systems (CLS), whose functionality is spread out over up to 19 di? erent ECUs in some luxury cars. Of course, this includes advanced functi- ality, such as seat positioning and radio tuning according to driver presets upon entry, as well as unlocking in case of a detected impact or accident. However, thisexampledemonstratesthatmodernautomotivesystemsbridgecomfort-and safety-critical functionality. This induces particular demands on safety and - curity, and, in general, software and systems quality. The resulting challenges and opportunities were discussed, in depth, at the second Automotive Software Workshop San Diego (ASWSD)2006, on whose results we report here.

This text discusses the philosophy of modular programming, emphasizing well-defined project segmentation for system modularity. It highlights the clarity of module interfaces, independent testing, and ease of maintenance. The paper aims to explore criteria for dividing systems into modules and notes advancements in coding techniques that facilitate module independence and reassembly.

Software development for the automotive domain is currently subject to a silent revolution. On the one hand, software has become the enabling technology for almost all safety-critical and comfort functions o? ered to the customer. A total of 90 % of all innovations in automotive systems are directly or indirectly - abled by software. Today’s luxury cars contain up to 80 electronic control units (ECUs) and 5 di? erent, inter-connectednetworkplatforms, overwhich some700 software-enabled functions are distributed. On the other hand, the complexity induced by this largenumber of functions, their interactions, and their supporting infrastructure has started to becomethe limiting factor for automotive software development. Adequate management of this complexity is particularly important; the following list highlights three of the corresponding challenges: First, the dependencies between safety-critical and comfort functions are rapidly increasing; a simple example is the interplay of airbag controland power seat control in the case of an accident. Careful analysis and design of these dependencies are necessary to yield correct software solutions. Second, advances in wired and wireless networking infrastructures enable - terconnection between cars and backend service providers (e. g., to call for help in cases of emergency), between cars and devices brought into the car by drivers and passengers (such as cell phones, PDAs, and laptops), and even among cars. This dramatically shifts the focus from the development of individual software solutionsresidingondedicatedECUstotheirdistributionandinteractionwithin and beyond car boundaries.

This book constitutes the thoroughly refereed postconference proceedings of the 5th International Andrei Ershov Memorial Conference, PSI 2003, held in Akademgorodok, Novosibirsk, Russia in July 2003. The 55 revised full papers presented were carefully reviewed and selected from 110 submissions during two rounds of evaluation and improvement. The papers are organized in topical sections on programming, software engineering, software education, program synthesis and transformation, graphical interfaces, partial evaluation and supercompilation, verification, logic and types, concurrent and distributed systems, reactive systems, program specification, verification and model checking, constraint programming, documentation and testing, databases, and natural language processing

A mathematical and logical foundation for the specification and development of interactive systems based on a model that describes systems in terms of their input/output behavior. Based on this model, the authors build a basic method, called FOCUS, that enables interactive systems to be described by characterizing their histories of message interaction. The book progresses from an introduction and guided tour of FOCUS through streams, specifications and their properties, and behavioral, interface, and conditional refinements.

InhaltsverzeichnisFoundations of Software Engineering.Domains as a Prerequisite for Requirements and Software Domain Perspectives and Facets, Requirements Aspects and Software Views.Software and System Modeling Based on a Unified Formal Semantics.Postmodern Software Design with NYAM: Not Yet Another Method.Methodology.A Discipline for Handling Feature Interaction.Merging Changes to Software Specifications.Combining and Distributing Hierarchical Systems.Software Engineering Issues for Network Computing.A Two-Layered Approach to Support Systematic Software Development.Evaluation and Case Studies.A Framework for Evaluating System and Software Requirements Specification Approaches.Formal Methods and Industrial-Strength Computer Networks.Tool Support and Prototyping.Integration Tools Supporting Development Processes.Formal Models and Prototyping.Abstraction and Modular Verification of Infinite-State Reactive Systems.NSA’s MISSI Reference Architecture – Moving from Prose to Precise Specifications.Requirements Engineering Repositories: Formal Support for Informal Teamwork Methods.

Modern information processing systems show such complex properties as distribution, parallelism, interaction, time dependency, and nondeterminism. For critical applications, mathematical methods are needed to model the systems and to support their development and validation. Impressive progress in mathematical methods for programming software systems makes it possible to think about unifying the different approaches. This book gives a comprehensive overview of existing methods and presents some of the most recent results in applying them. The main topics are: advanced programming techniques, foundations of systems engineering, mathematical support methods, and application of the methods. The approaches presented are illustrated by examples and related to other approaches.

The RPC-memory specification problem was proposed by Broy and Lamport as a case study in the formal design of distributed and concurrent systems. As a realistic example typical for operating systems and hardware design, the RPC-memory problem was used as the basis for comparing various approaches to formal specification, refinement, and verification. Preliminary solutions were discussed during a workshop at Schloss Dagstuhl, Germany, in September 1994. Then an extensive discussion took place between the referees and authors. Finally 15 thoroughly revised papers were accepted for inclusion in this volume in full detail together with the problem statement and a synopsis.