Today almost every complex technical system used in industry, science, commerce and communication is more or less interfaced with software and software systems. This dictates that most information exchange is closely related to software and computer systems. The consequence of this wide distribution of software is a high dependency on its functioning and quality. Because of this dependency and distribution, making information systems safe, reliable, as well as secure and protecting information against all kinds of attack is an essential research topic, particularly in computer science.

Scientific foundations have been developed for programming and building computer systems. These foundations cover a broad spectrum of issues and work with formal models and description techniques in order to support a deep and precise understanding and managing of a system's properties and interplay. In addition, software engineering has many additional applications, ranging from telecommunications to embedded systems. For example software engineering has now become essential in automotive and aircraft industry, and has been intergral in furthering computer networks distributed over wide-area networks. A vast proportion of information exchange is influenced by computer systems and information security is important for reliable and secure software and computer systems.

Information security covers the protection of information against unauthorized disclosure, transfer, modification, and destruction, whether accidentally or intentionally. Attacks against computer systems can cause considerable economic and physical damage. Quality of life in general and of individual citizens, and the effectiveness of the economy critically depends on our ability to build software in a transparent and efficient way. Furthermore, we must be able to enhance the software development process systematically in order to ensure safety, security and reliability. This, in turn, requires very high software reliability, i. e., an extremely high confidence in the ability of the software to perform flawlessly. The foundations of software technology provide models that enable us to capture application domains and their requirements, but also to understand the structure and working of software systems, software architectures and programs. New developments must pay due diligence to the importance of security-related aspects, and align current methods and techniques to information security, integrity, and system reliability. However, based on the specific needs in applications of software technology, models and formal methods must serve the needs and the quality of advanced software engineering methods, especially taking into account security aspects in Information Technology.

As a consequence of the wide distribution of software and software infrastructure, information security depends on the quality and excellent understanding of its functioning. Only when this functionality is guaranteed as safe, customers, and information are protected against adversarial attacks. Thus, to make communication and computation secure against catastrophic failure and malicious interference, it is essential to build secure software systems and methods for their development. Such development is difficult, mainly because of the conflict between development costs and verifiable correctness.

In the summer of 2006, a group of internationally renowned researchers in computer science met and lectured on the topics described above. The articles in this book describe the state-of-the-art ideas on how to meet these challenges in software engineering.

Rajeev Alur describes the foundations of model checking of programs with finite data and stack-based control flow. Manfred Broy introduces an abstract theory for systems, components, composition, architectures, interfaces, and compatibility. In his article he applies this theory to object orientation and elaborates on the application of that theory covering notions for a formal model of objects, classes, components, and architectures as well as those of interfaces of classes and components and their specification. Ernie Cohen explains how to use ordinary program invariants to prove properties of cryptographic protocols.

Networked computer systems face a range of threats from hostile parties on the network leading to violations of design goals such as confidentiality, privacy, authentication, access control, and availability. The purpose of Andrew Gordon's article is to introduce an approach to this problem based on process calculi. Transactions are the essential components of electronic business systems, and their safety and security are of increasing concern. Tony Hoare presents a theoretical model of compensable transactions, showing how long running transactions may be correctly composed out of shorter ones. Orna Kupferman presents on “Applications of Automata-Theory in Formal Verification”. In this automata-theoretic approach to verification, she reduces questions about programs and their specifications to questions about automata.

In a distributed system with no central management such as the Internet, security requires a knowledge about who can be trusted for each step in establishing it, and why. Butler W. Lampson explains the “speaks for” relation between principals describing how authority is delegated. Axel van Lamsweerde contributes model-based requirements engineering. Models for agents, operations, obstacles to goals, and security threats are introduced and a model building with the KAOS method is presented. Wolfgang Paul outlines a correctness proof for a distributed real time system – for the first time in a single place – from the gate level to the computational model of a CASE tool.

Amir Pnueli describes an approach for the synthesis of (hardware and software) designs from LTL specifications. This approach is based on modelling the synthesis problem which is similar to the problem of finding a winning strategy in a two-person game. K. Venkatesh Prasad introduces the notion of a “mobile networked embedded system”, in which a mobile entity is composed of internally and externally networked software components. He discusses the challenges related to designing a mobile networked embedded system with regards to security, privacy, usability, and reliability. Finally, Wolfram Schulte explains the “Spec# Approach”, which provides method contracts in the form of pre- and post-conditions as well as object invariants. He describes the design of Spec#'s state-of-the-art program verifier for object-oriented programs.

The contributions in this volume have emerged from lectures of the 27th International Summer School on Software System Reliability and Security, held at Marktoberdorf from August 1 to August 13, 2006. More than 100 participants from 28 countries attended, including students, lecturers and staff. The Summer School provided two weeks of learning, discussion and development of new ideas, and was a fruitful event, at both the professional and social level.

We would like to thank all lecturers, staff, and hosts in Marktoberdorf. In particular special thanks goes to our secretaries Dr. Katharina Spies, Silke Müller, and Sonja Werner for their great and gentle support.

The Marktoberdorf Summer School was arranged as an Advanced Study Institute of the NATO Security Through Science Programme with support from the town and county of Marktoberdorf and the Deutscher Akademischer Austausch Dienst (DAAD). We thank all authorities involved.

THE EDITORS