LEADER 00000cam a2200625Mi 4500
001 on1040038567
003 OCoLC
005 20200417040046.6
006 m o d
007 cr |||||||||||
008 180427s2017 dk a ob 001 0 eng d
020 8793519818
020 9788793519824|q(hardback)
020 8793519826
020 9788793519817|q(electronic book)
035 (OCoLC)1040038567
037 5050188|bProquest Ebook Central
040 QCL|beng|erda|epn|cQCL|dOCLCO|dOCLCF|dAU@|dYDX|dOCLCQ|dLVT
|dUKAHL|dN$T
049 RIDW
050 4 QA76.7|b.B44 2017
082 04 005.13|223
090 QA76.7|b.B44 2017
245 00 Behavioural types :|bfrom theory to tools /|ceditors,
Simon Gay (University of Glasgow, UK), António Ravara
(Universidade Nova de Lisboa, Portugal).
264 1 Gistrup, Denmark :|bRiver Publishers,|c[2017]
264 2 [Ann Arbor, Michigan] :|bProQuest Ebook Central.
264 4 |c©2017
300 1 online resource (xxxiv, 375 pages) :|billustrations
(some colour).
336 text|btxt|2rdacontent
337 computer|bc|2rdamedia
338 online resource|bcr|2rdacarrier
347 text file|bPDF|2rda
490 1 River Publishers series in automation, control and
robotics
504 Includes bibliographical references and index.
505 0 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.
505 8 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.
505 8 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.
505 8 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.
505 8 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.
590 eBooks on EBSCOhost|bEBSCO eBook Subscription Academic
Collection - North America
650 0 Programming languages (Electronic computers)|0https://
id.loc.gov/authorities/subjects/sh85107313
650 0 Type theory.|0https://id.loc.gov/authorities/subjects/
sh85139126
650 7 Programming languages (Electronic computers)|2fast|0https:
//id.worldcat.org/fast/1078704
650 7 Type theory.|2fast|0https://id.worldcat.org/fast/1159972
655 4 Electronic books.
700 1 Gay, Simon,|d1969-|0https://id.loc.gov/authorities/names/
n93053229|eeditor.
700 1 Ravara, António,|0https://id.loc.gov/authorities/names/
nb2016011978|eeditor.
776 08 |iPrint version:|tBehavioural types : from theory to
tools.|dGistrup, Denmark : River Publishers, ©2017
|z9788793519824
830 0 River Publishers series in automation, control and
robotics.|0https://id.loc.gov/authorities/names/
no2016146605
856 40 |uhttps://rider.idm.oclc.org/login?url=http://
search.ebscohost.com/login.aspx?direct=true&scope=site&
db=nlebk&AN=1800576|zOnline eBook via EBSCO. Access
restricted to current Rider University students, faculty,
and staff.
856 42 |3Instructions for reading/downloading the EBSCO version
of this eBook|uhttp://guides.rider.edu/ebooks/ebsco
901 MARCIVE 20231220
948 |d20200422|cEBSCO|tebscoebooksacademic 3-13-4-17 3106
|lridw
994 92|bRID
