RiSE - Rigorous Systems Engineering

Over the past decades, the complexity and size as well as the ubiquity and criticality of computer systems have increased dramatically. They are now at a level where human engineers and programmers require assistance by computer-aided methods and tools that are based on a rigorous mathematical foundation. We have seen much recent progress in such techniques and tools: model checkers and static analyzers are now used routinely in the design of hardware and certain restricted kinds of software. Nevertheless, the exploding presence of concurrent computation - from multi-core processors to cloud computing - has rendered many established methods obsolete and is the single most important challenge facing systems engineering today. The traditional use of model checking and related techniques has been a posteriori, i.e., a program or model is analyzed after completion. This procedure is costly and decouples the quality assessment from the engineering process. It is the goal of our project to move beyond classical model checking and a posteriori verification. We use the term "Rigorous Systems Engineering" (RiSE) to describe an approach in which mathematical techniques such as model checking provide a solid foundation for the design process from day one. Within RiSE, we plan to focus on topics that are motivated by the new generation of highly concurrent and embedded systems: We will look at software transactions and data center programming to address multi-core and software-as-a-service issues; at virtualization and distributed message passing concepts to address real-time issues; and at the integration of model checking with complementary, execution based techniques, such as software testing, in order to build tools that can cope with large-scale software systems. The project has three main research thrusts: First, we will develop new language-based, architectural, and verification paradigms for highly concurrent and real-time software. Second, we will develop novel game-theoretic algorithms for analyzing and synthesizing individual system components within a larger context. Third, we will develop and improve decision procedures that lie at the very heart of every automatic method and tool for system design and analysis. RiSE consists of five internationally recognized researchers from the model checking community and four renowned researchers from the neighboring fields of software systems, distributed computing, and computational logic. This set-up will encourage the integration of different viewpoints and complementary approaches towards the common objective of RiSE.