Almost all technical systems are more or less interfaced with software systems, thus attacks against computer systems can cause considerable economic and physical damage. Due to the wide distribution of software systems the understanding of safety, security, and reliability (shortly termed with “dependability”) as well as the improvement of the general quality of complex software systems (cyber security) and its development process show a challenging and crucial issue in computer science research.

To cover the broad range of engineering dependable software systems, we assembled in our NATO Advanced Study Institute Summer School Marktoberdorf 2012 a group of internationally leading researchers and experts. They taught their profound knowledge and experience in Software Engineering going from REQUIREMENTS through the entire PROCESS, using methods to verify the software system with MODEL CHECKING, methods to detect faults with TESTING as well as techniques to formally prove systems' behavior by VERIFICATION. The course was designed as an in-depth presentation and excellent teaching of state-of-the-art scientific techniques and methods covering research and industrial practice as well as scientific foundations.

ED BRINKSMA lectured on Model-based Testing. His course provided an overview of model-based testing and its application. He gave an introduction to testing in general, and model-based testing in particular. He showed how both theory and tools can be extended to deal with real-time behavior in specifications, implementations and tests.

The topic of MANFRED BROY's lecture was From Requirements to Functional and Architectural Views. Understanding requirements as logical statements about systems, he used the complete machinery of predicate logic to define relationships between requirements in terms of traces and healthiness conditions for sets of requirements. A comprehensive specification of a system was given in a structured manner in terms of adequate formal system models. The model included a data model, a context model, and a structured interface model.

MICHAEL BUTLER's lecture on Abstraction, Refinement and Decomposition for Systems Engineering addressed the key role played by formal modeling and verification in systems engineering. In order to manage system complexity, abstraction, refinement and decomposition of formal models are key methods for structuring the formal modeling effort since they support separation of concerns and layered reasoning. Michael used the Event-B formal modeling language and the associated Rodin toolset for Event-B. The key features of Event-B are the use of set theory as a modeling notation, refinement to represent systems at different abstraction levels and mathematical proof to verify the consistency between refinement levels.

The title of ERNIE COHEN's lecture was How to Verify Your Software. Deductively verified software has long been viewed as a niche activity, practical only for proof-checking experts and too expensive for all but the most critical software. This is no longer the case; thanks to improvements in reasoning technology and programming methodology, it is now often cheaper to verify software than to test it. The course described VCC (a verifier for concurrent C code) and how it can be used to write verified software.

Families of Dependable Systems: A Model Checking Approach was the topic of STEFANIA GNESI. A number of models, logics and associated tools for the qualitative analysis of variability aspects and their use to deal with adaptability and evolvability of systems have recently been proposed. Stefania introduced the action-based branching-time temporal logic MHML that allows expressing constraints over the products of a family as well as constraints over their behavior in a single logical framework. Based on model-checking techniques for MHML, a modeling and verification framework was presented that can automatically generate all the familyt's valid products, visualize the family/products behavior and efficiently model check properties expressed in MHML over products and families alike.

In his series of lectures Verifying Execution Traces KLAUS HAVELUND focused on checking program executions against formal specifications. A variety of formalisms and algorithms have been proposed for this purpose, specifically over the last decade. These included state machines, temporal logics, regular expressions, grammar systems and rule-based systems. A major research challenge was how to conveniently specify and efficiently monitor properties of traces containing data parameterized events. Klaus presented a set of different data-centric formalisms as well as their associated monitoring algorithms, illustrating the state of the art in RV.

JOOST-PIETER KATOEN held a lecture on Performance Analysis by Model Checking. Continuous-time Markov chains (CTMCs) are omnipresent. First and foremost, they are the heart of classical performance analysis. They provide a natural semantics of queuing networks, stochastic Petri nets, stochastic process algebras, and systems biology. Joost-Pieter's lectures focused on the analysis of CTMCs using model checking. The foundations for reachability, timed reachability, as well as timed automata objectives were considered. Practical examples showed its applicability. Abstraction techniques were introduced enabling the verification of huge Markov chains.

Lectures on Handling Obstacles in Goal-Oriented Requirements Engineering were held by AXEL VAN LAMSWEERDE. The course presented a systematic approach for integrating risk analysis in model-based requirements engineering. Obstacles were introduced as a natural abstraction for risk analysis. An obstacle to a goal is a precondition for the non-satisfaction of this goal. The course detailed and illustrated a variety of techniques supporting the identify-assess-resolve cycles of obstacle analysis. For obstacle identification, a formal regression calculus was used to derive obstacles, or combine model checking and inductive learning to generate a domain-complete set of obstacles. For obstacle assessment, Axel enriched the models with a probabilistic layer allowing us to estimate the likelihood of fine-grained obstacles and propagate these through the obstacle and goal models in order to determine the severity and likelihood of obstacle consequences. For obstacle resolution, alternative countermeasures by use of systematic model transformations that encode risk-reduction tactics were explored, and most appropriate ones selected based on the likelihood of obstacles and the severity of their consequences.

KIM LARSEN lectured on Model-based Verification and Validation of Embedded Systems. Model-driven development has been proposed as a way to deal with the increasing complexity of real-time and embedded systems, while reducing the time and cost to market. During his lectures he offered a thorough account of the formalism of timed automata as well as several recent extensions including priced timed automata, (priced) timed games and most recently stochastic timed automata. Kim also emphasized the substantial research effort in the design of algorithms and data structures for efficient analysis as to be found in the verification tool UPPAAL and its various branches. Indication of industrial applications was also given.

The topic of RICHARD PAIGE was Model-Driven Engineering and Model Transformation: for Fun and Profit. Model-Driven Engineering (MDE) is an engineering discipline that uses descriptions of phenomena of interest as first-class engineering artifacts. At the heart of MDE is model transformation, the process of transforming models across and between languages. The fundamental concepts of MDE, including how its style and form of description, differ from that of more mathematical approaches was introduced. Mechanisms for verifying and validating such transformations, ranging from automated testing to concrete task-specific forms of analysis such as failure analysis were considered.

Symbolic Execution and Software Testing was the title of CORINA PĂSĂREANU's lecture. Symbolic execution is a systematic program analysis technique that has become increasingly popular in recent years, due to algorithmic advances and availability of computational power and constraint solving technology. Corina reviewed different flavors of symbolic execution, ranging from generalized symbolic execution to dynamic symbolic execution or concolic testing. The application of symbolic execution to software testing was discussed.

DORON PELED held a lecture on Software Reliability Methods: Model Checking. During the last three decades, the automatic verification of systems called “model checking” has gained a lot of success as an alternative to manual methods of system testing. In this series of lectures Doron showed some basic techniques to formally specify properties of systems and automatically verify them. The lecture concentrated on Linear Temporal Logic and Buchi Automata specification, and on explicit state model checking, as is done in the SPIN model checking system. Branching time specification/verification was briefly mentioned. Finally, the principles of automatically constructing correct-by-design systems directly from their specification were shown.

As shown in this series of a NATO Advanced Study Institute, such presentations as well as working and learning together are essential for future scientific results in computer science and consequently the development of large-scale reliable and secure software systems. The Summer School provided two weeks of learning, discussion and development of new ideas, and was be a productive and beneficial event, at both the professional and social level.

We thank all lecturers, the staff, and hosts in Marktoberdorf. Special thanks goes to Dr. Katharina Spies and Silke Müller for their great support.

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

THE EDITORS