Skip to content
You are not logged in |Login  
     
Limit search to available items
Record:   Prev Next
Resources
More Information
Bestseller
BestsellerE-book

Title Behavioural types : from theory to tools / editors, Simon Gay (University of Glasgow, UK), António Ravara (Universidade Nova de Lisboa, Portugal).

Publication Info. Gistrup, Denmark : River Publishers, [2017]
[Ann Arbor, Michigan] : ProQuest Ebook Central.
©2017

Item Status

Description 1 online resource (xxxiv, 375 pages) : illustrations (some colour).
text file PDF
Series River Publishers series in automation, control and robotics
River Publishers series in automation, control and robotics.
Bibliography Includes bibliographical references and index.
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.
Local Note eBooks on EBSCOhost EBSCO eBook Subscription Academic Collection - North America
Subject Programming languages (Electronic computers)
Programming languages (Electronic computers)
Type theory.
Type theory.
Genre/Form Electronic books.
Added Author Gay, Simon, 1969- editor.
Ravara, António, editor.
Other Form: Print version: Behavioural types : from theory to tools. Gistrup, Denmark : River Publishers, ©2017 9788793519824
ISBN 8793519818
9788793519824 (hardback)
8793519826
9788793519817 (electronic book)