Behavioural types : from theory to tools /

Behavioural type systems in programming languages support the specification and verification of properties of programs beyond the traditional use of type systems to describe data processing. A major example of such a property is correctness of communication in concurrent and distributed systems, mot...

Full description

Bibliographic Details
Corporate Author:	Taylor & Francis
Other Authors:	Gay, Simon, 1969- (Editor), Ravara, António (Editor)
Format:	eBook
Language:	English
Published:	Gistrup, Denmark : River Publishers, [2017]
Series:	River Publishers series in automation, control and robotics.
Subjects:	Programming languages (Electronic computers) Type theory. Théorie des types. COMPUTERS / Programming / Software Development SCIENCE / Energy Type theory Electronic books.
Online Access:	Connect to the full text of this electronic book

Table of Contents:

Front Cover
Half Title Page
RIVER PUBLISHERS SERIES IN AUTOMATION, CONTROLAND ROBOTICS
Title Page
Behavioural Types: fromTheory to Tools
Copyright Page
Contents
Preface
Acknowledgments
List of Contributors
List of Figures
List of Tables
List of Abbreviations
Chapter 1
Contract-Oriented Design of Distributed Applications: A Tutorial
1.1 Introduction
1.1.1 From Service-Oriented to Contract-Oriented Computing
1.1.2 Honesty Attacks
1.1.3 Diogenes
1.2 Specifying Contract-Oriented Services in CO2
1.2.1 Contracts
1.2.2 Processes
1.2.3 An Execution Context
1.2.4 Adding Recursion
1.3 Honesty
1.3.1 A Simple Dishonest Store
1.3.2 A More Complex Dishonest Store
1.3.3 Handling Failures
1.3.4 An Honest Store, Finally
1.3.5 A Recursive Honest Store
1.4 Refining CO2 Specifications in Java Programs
1.4.1 Compilation of CO2 Specifications into Java Skeletons
1.4.2 Checking Honesty of Refined Java Programs
1.5 Conclusions
1.5.1 Related Work
References
Chapter 2
Contract-Oriented Programming with Timed Session Types
2.1 Introduction
2.2 Timed Session Types
2.2.1 Specifying Contracts
2.2.2 Compliance
2.2.3 Run-Time Monitoring of Contracts
2.3 Contract-Oriented Programming
2.3.1 A Simple Store
2.3.2 A Simple Buyer
2.3.3 A Dishonest Store
2.3.4 An Honest Store
2.3.5 A Recursive Honest Store
2.4 Conclusions
2.4.1 Related Work
References
Chapter 3
A Runtime Monitoring Tool for Actor-Based Systems
3.1 Introduction
3.2 Background
3.2.1 Runtime Monitoring Criteria
3.2.2 A Branching-Time Logic for Specifying Correctness Properties
3.2.3 Monitoring ?HML
3.3 A Tool for Monitoring Erlang Applications
3.3.1 Concurrency-Oriented Development Using Erlang
3.3.2 Reasoning about Data.
3.3.2.1 Properties with specific PIDs
3.3.2.2 Further reasoning about data
3.3.3 Monitor Compilation
3.4 detectEr in Practice
3.4.1 Creating the Target System
3.4.1.1 Setting up the Erlang project
3.4.1.2 Running and testing the server
3.4.2 Instrumenting the Test System
3.4.2.1 Property specification
3.4.2.2 Monitor synthesis and instrumentation
3.4.2.3 Running the monitored system
3.4.2.4 Running the correct server
3.5 Conclusion
3.5.1 Related and Future Work
References
Chapter 4
How to Verify Your Python Conversations
4.1 Framework Overview
4.2 Scribble-Based Runtime Verification
4.2.1 Verification Steps
4.2.2 Monitoring Requirements
4.3 Conversation Programming in Python
4.4 Monitor Implementation
4.5 Monitoring Interruptible Systems
4.5.1 Use Case: Resource Access Control (RAC)
4.5.2 Interruptible Multiparty Session Types
4.5.3 Programming and Verification of Interruptible Systems
4.5.4 Monitoring Interrupts
4.6 Formal Foundations of MPST-Based Runtime Verification
4.7 Concluding Remarks
References
Chapter 5
The DCR Workbench: Declarative Choreographies for Collaborative Processes
5.1 Introduction
5.1.1 History of the DCR Workbench
5.1.2 The DCR Workbench
5.2 Running Example
5.3 Dynamic Condition-Response Graphs
5.3.1 Event States
5.3.2 Relations
5.3.3 Executing Events
5.3.4 Formal Development
5.4 Modelling with the Workbench
5.4.1 Inputting a Model: The Parser Panel
5.4.2 Visualisation and Simulation: The Visualiser and Activity Log Panels
5.5 Refinement
5.6 Time
5.7 Subprocesses
5.8 Data
5.9 Other Panels
5.10 Conclusion
References
Chapter 6
A Tool for Choreography-Based Analysis of Message-Passing Software
6.1 Introduction
6.2 Overview of the Theory
6.3 Architecture.
6.4 Modelling of an ATM Service
6.4.1 ATM Service
Version 1
6.4.2 ATM Service
Version 2
6.4.3 ATM Service
Version 3 (fixed)
6.5 Conclusions and Related Work
References
Chapter 7
Programming Adaptive Microservice Applications: An AIOCJ Tutorial*
7.1 Introduction
7.2 AIOCJ Outline
7.2.1 AIOCJ Architecture and Workflow
7.3 Choreographic Programming
7.4 Integration with Legacy Software
7.5 Adaptation
7.6 Deployment and Adaptation Procedure
7.7 Conclusion
References
Chapter 8
JaDA
the Java Deadlock Analyzer
8.1 Introduction
8.2 Example
8.3 Overview of JaDA's Theory
8.3.1 The Abstract Behavior of the Network Class
8.3.2 Behavioral Type Inference
8.3.3 Analysis of Behavioral Types
8.4 The JaDA Tool
8.4.1 Prerequisites
8.4.2 The Architecture
8.4.3 The Current JVML Coverage
8.4.4 Tool Configuration
8.4.5 Deliverables
8.5 Current Limitations
8.6 Related Tools and Assessment
8.7 Conclusions
References
Chapter 9
Type-Based Analysis of Linear Communications
9.1 Language
9.2 Type System
9.3 Extended Examples
9.3.1 Fibonacci Stream Network
9.3.2 Full-Duplex and Half-Duplex Communications
9.3.3 Load Balancing
9.3.4 Sorting Networks
9.3.5 Ill-typed, Lock-free Process Networks
9.4 Related Work
References
Chapter 10
Session Types with Linearity in Haskell
10.1 Introduction
10.2 Pre-Session Types in Haskell
10.2.1 Tracking Send and Receive Actions
10.2.2 Partial Safety via a Type-Level Function for Duality
10.2.3 Limitations
10.3 Approaches in the Literature
10.3.1 Note on Recursion and Duality
10.3.2 Single Channel
Neubauer and Thiemann [9]
10.3.3 Multi-Channel Linearity
Pucella and Tov [13]
10.3.4 An Alternate Approach
Sackman and Eisenbach [15]
10.3.5 Multi-Channels with Inference.
Imai et al. [5]
10.3.6 Session Types via Effect Types
Orchard and Yoshida [11]
10.3.7 GV in Haskell
Lindley and Morris [8]
10.4 Future Direction and Open Problems
References
Chapter 11
An OCaml Implementation of Binary Sessions
11.1 An API for Sessions
11.2 A Few Simple Examples
11.3 API Implementation
11.4 Extended Example: The Bookshop
11.5 Related Work
References
Chapter 12
Lightweight Functional Session Types
12.1 Introduction
12.2 A First Look
12.3 The Core Language
12.3.1 Syntax
12.3.2 Typing and Kinding Judgments
12.4 Extensions
12.4.1 Recursion
12.4.2 Access Points
12.5 Links with Session Types
12.5.1 Design Choices
12.5.2 Type Reconstruction
12.6 Conclusion and Future Work
References
Chapter 13
Distributed Programming Using Java APIs Generated from Session Types
13.1 Background: Distributed Programming in Java
13.1.1 TCP Sockets
13.1.2 Java RMI
13.2 Scribble Endpoint API Generation: Toolchain Overview
13.2.1 Global Protocol Specification
13.2.2 Endpoint API Generation
13.2.3 Hybrid Session Verification
13.2.4 Additional Math Service Endpoint Examples
13.3 Real-World Case Study: HTTP (GET)
13.3.1 HTTP in Scribble: First Version
13.3.2 HTTP in Scribble: Revised
13.4 Further Endpoint API Generation Features
References
Chapter 14
Mungo and StMungo: Tools for Typechecking Protocols in Java
14.1 Introduction
14.2 Mungo: Typestate Checking for Java
14.2.1 Example: Iterator
14.3 StMungo: Typestates from Communication Protocols
14.3.1 Example: Travel Agency
14.4 POP3: Typechecking an Internet Protocol Client
14.4.1 Challenges of Using Mungo and StMungo in the Real World
14.5 Related Work
References
Chapter 15
Protocol-Driven MPI Program Generation
15.1 Introduction.
15.2 Pabble: Parameterised Scribble
15.3 MPI Backbone
15.3.1 MPI Backbone Generation from Ring Protocol
15.4 Computation Kernels
15.4.1 Writing a Kernel
15.4.1.1 Initialisation
15.4.1.2 Passing data between backbone and kernel through queues
15.4.1.3 Predicates
15.5 The Pabble Language
15.5.1 Global Protocols Syntax
15.5.1.1 Restriction on constants
15.5.2 Local Protocols
15.6 MPI Backbone Generation
15.6.1 Interaction
15.6.2 Parallel Interaction
15.6.3 Internal Interaction
15.6.4 Control-flow: Iteration and For-loop
15.6.5 Control-flow: Choice
15.6.6 Collective Operations: Scatter, Gather and All-to-all
15.6.7 Process Scaling
15.7 Merging MPI Backbone and Kernels
15.7.1 Annotation-Guided Merging Process
15.7.2 Kernel Function
15.7.3 Datatypes
15.7.4 Conditionals
15.8 Related Work
15.9 Conclusion
References
Chapter 16
Deductive Verification of MPI Protocols
16.1 Introduction
16.2 The Finite Differences Algorithm and Common Coding Faults
16.3 The Protocol Language
16.4 Overview of the Verification Procedure
16.5 The Marking Process
16.6 Related Work
16.7 Conclusion
References
Index
About the Editors
Back Cover.