Provably Correct Systems / edited by Mike Hinchey, Jonathan P. Bowen, Ernst-Rüdiger Olderog.

Format:

Book

Contributor:

Hinchey, Mike, editor.

Bowen, Jonathan P., editor.

Olderog, E.-R., editor.

SpringerLink (Online service)

Series:

Computer Science (Springer-11645)

NASA monographs in systems and software engineering 1860-0131

NASA Monographs in Systems and Software Engineering, 1860-0131

Language:

English

Subjects (All):

Logic, Symbolic and mathematical.

Computer logic.

Computers.

Computer programming.

Mathematical Logic and Formal Languages.

Logics and Meanings of Programs.

Models and Principles.

Programming Techniques.

Local Subjects:

Mathematical Logic and Formal Languages.

Logics and Meanings of Programs.

Models and Principles.

Programming Techniques.

Physical Description:

1 online resource (XV, 328 pages) : 84 illustrations, 48 illustrations in color.

Edition:

First edition 2017.

Contained In:

Springer eBooks

Place of Publication:

Cham : Springer International Publishing : Imprint: Springer, 2017.

System Details:

text file PDF

Summary:

As computers increasingly control the systems and services we depend upon within our daily lives like transport, communications, and the media, ensuring these systems function correctly is of utmost importance. This book consists of twelve chapters and one historical account that were presented at a workshop in London in 2015, marking the 25th anniversary of the European ESPRIT Basic Research project 'ProCoS' (Provably Correct Systems). The ProCoS I and II projects pioneered and accelerated the automation of verification techniques, resulting in a wide range of applications within many trades and sectors such as aerospace, electronics, communications, and retail. The following topics are covered: An historical account of the ProCoS project Hybrid Systems Correctness of Concurrent Algorithms Interfaces and Linking Automatic Verification Run-time Assertions Checking Formal and Semi-Formal Methods <web-supported scientific="" communities Provably Correct Systems provides researchers, designers and engineers with a complete overview of the ProCoS initiative, past and present, and explores current developments and perspectives within the field.

Contents:

Foreword

Preface

Part I: Historic Account

ProCoS: How It All Began - As Seen from Denmark

Part II: Hybrid Systems

Constraint-Solving Techniques for the Analysis of Probabilistic Hybrid Systems

MARS: A Tool chain for Modelling, Analysis and Verification of Hybrid Systems

Part III: Correctness of Concurrent Algorithms

A Proof Method for Linearizability on TSO Architectures

Part IV: Interfaces and Linking

Linking Discrete and Continuous Models, Applied to Traffic Manoeuvres

Towards Interface-Driven Design of Evolving Component-Based Architectures

Part V: Automatic Verification

Computing Verified Machine Address Bounds during Symbolic Exploration of Code

Engineering a Formal, Executable x86 ISA Simulator for Software Verification

Advances in Connection-Based Automated Theorem Proving

Part VI: Run-Time Assertion Checking

Run-Time Deadlock Detection

In-Circuit Assertions and Exceptions for Reconfigurable Hardware Design

Part VII: Formal and Semi-Formal Methods

From ProCoS to Space and Mental Models - a Survey of Combing Formal and Semi-Formal Methods

Part VIII: Web-Supported Communities in Science

Provably Correct Systems: Community, Connections and Citations.

Other Format:

Printed edition:

ISBN:

978-3-319-48628-4

9783319486284

Access Restriction:

Restricted for use by site license.