Correct System Design

1. Front Matter

   Pages I-XIV

   PDF

2. Methodology

   1. Theories of programming: Top-Down and Bottom­up and Neeting in the Middle

      • C. A. R. Hoare

      Pages 3-28

3. A Triptych Software Development Paradigm: Domain, Requirements and Software Towards a Nodel Development of a Decision Support System for Sustainable Development

   1. A Triptych Software Development Paradigm: Domain, Requirements and Software Towards a Nodel Development of a Decision Support System for Sustainable Development

      • Dines Bjørner

      Pages 29-60

4. Real-Time Constraints Through the ProCoS Layers

   1. Real-Time Constraints Through the ProCoS Layers

      • Anders P. Ravn, Hans Rischel

      Pages 61-78

5. Monotonicity in Calculational Proofs

   1. Monotonicity in Calculational Proofs

      • David Gries

      Pages 79-85

6. Programming

   1. The Alma Project, or How First-Order Logic Can Help us in Imperative Programming

      • Krzysztof R. Apt, Andrea Schaerf

      Pages 89-113

   2. Type and Effect Systems

      • Flemming Nielson, Hanne Riis Nielson

      Pages 114-136

7. Automation

   1. Proving Theorems About Java-Like Byte Code

      • J Strother Moore

      Pages 139-162

   2. Multiple State and Single State Tableaux for Combining Local and Global Nodel Checking

      • Armin Biere, Yunshan Zhu, Edmund M. Clarke

      Pages 163-179

   3. On the Existence of Network Invariants for Verifying Parameterized Systems

      • Parosh Aziz Abdulla, Bengt Jonsson

      Pages 180-197

8. Compilation

   1. Verification of Compilers

      • Gerhard Goos, Wolf Znnmerrnaun

      Pages 201-230

   2. Translation Validation: From SIGNAL to C

      • A. Pnueli, O. Shtrichman, M. Siegel

      Pages 231-255

   3. Compilation and Synthesis for Real-Time Embedded Controllers

      • Martin Fränzle1, Markus Müller-Olm

      Pages 256-287

   4. Optimization Under the Perspective of Soundness, Completeness, and Reusability

      • Jens Knoop, Oliver Rüthing

      Pages 288-315

9. Application

   1. Verification of Automotive Control Units

      • Tom Bienmüllor, Jürgon Bohn, Henning Brinkmann, Udo Brockmeyer, Werner Damm, Hardi Hungar et al.

      Pages 319-319

   2. Correct Real-Time Software for Programmable Logic Controllers

      • Ernst-Rüdiger Olderog

      Pages 342-362

   3. Formal Methods for the International Space Station ISS

      • Jan Peleska, Bettina Buth

      Pages 363-389

   4. METAFrame in Practice: Design of Intelligent Network Services

      • Bernhard Steffen, Tiziana Margaria

      Pages 390-415

10. Back Matter

    Pages 417-417

    PDF

Computers are gaining more and more control over systems that we use or rely on in our daily lives, privately as well as professionally. In safety-critical applications, as well as in others, it is of paramount importance that systems controled by a computer or computing systems themselves reliably behave in accordance with the specification and requirements, in other words: here correctness of the system, of its software and hardware is crucial. In order to cope with this callenge, software engineers and computer scientists need to understand the foundations of programming, how different formal theories are linked together, how compilers correctly translate high-level programs into machine code, and why transformations performed are justifiable. This book presents 17 mutually reviewed invited papers organized in sections on methodology, programming, automation, compilation, and application.

• Compiler
• System
• automation
• decision support system
• formal method
• logic
• optimization
• programming
• proving
• real-time
• verification

• Fachbereich Informatik, Universität Oldenburg, Oldenburg, Germany

  Ernst-Rüdiger Olderog

• Fachbereich Informatik, Universität Dortmund, Dortmund, Germany

  Bernhard Steffen

Policies and ethics