|
|
|
|
| LEADER |
00000cam a2200000Mi 4500 |
| 001 |
in00004768233 |
| 006 |
m o d |
| 007 |
cr ||||||||||| |
| 008 |
180427s2017 dk a ob 001 0 eng d |
| 005 |
20240130225617.5 |
| 035 |
|
|
|a (OCoLC)on1040038567
|
| 040 |
|
|
|a QCL
|b eng
|e rda
|e pn
|c QCL
|d OCLCO
|d OCLCF
|d AU@
|d YDX
|d OCLCQ
|d LVT
|d UKAHL
|d N$T
|d K6U
|d OCLCO
|d TYFRS
|d OCLCQ
|d OCLCO
|d OCLCL
|
| 019 |
|
|
|a 1391468653
|
| 020 |
|
|
|a 8793519818
|
| 020 |
|
|
|a 9788793519824
|q (hardback)
|
| 020 |
|
|
|a 8793519826
|
| 020 |
|
|
|a 9788793519817
|q (electronic bk.)
|
| 020 |
|
|
|a 9781003337331
|q (electronic bk.)
|
| 020 |
|
|
|a 1003337333
|q (electronic bk.)
|
| 020 |
|
|
|a 9781000799392
|q (electronic bk. : EPUB)
|
| 020 |
|
|
|a 1000799395
|q (electronic bk. : EPUB)
|
| 020 |
|
|
|a 9781000799255
|q (electronic bk. : PDF)
|
| 020 |
|
|
|a 1000799255
|q (electronic bk. : PDF)
|
| 024 |
7 |
|
|a 10.1201/9781003337331
|2 doi
|
| 035 |
|
|
|a (OCoLC)1040038567
|z (OCoLC)1391468653
|
| 037 |
|
|
|a 5050188
|b Proquest Ebook Central
|
| 037 |
|
|
|a 9781003337331
|b Taylor & Francis
|
| 050 |
|
4 |
|a QA76.7
|b .B44 2017
|
| 072 |
|
7 |
|a COM
|x 051230
|2 bisacsh
|
| 072 |
|
7 |
|a SCI
|x 024000
|2 bisacsh
|
| 072 |
|
7 |
|a UMX
|2 bicssc
|
| 082 |
0 |
4 |
|a 005.13
|2 23
|
| 049 |
|
|
|a TXAM
|
| 245 |
0 |
0 |
|a Behavioural types :
|b from theory to tools /
|c editors, Simon Gay (University of Glasgow, UK), António Ravara (Universidade Nova de Lisboa, Portugal).
|
| 264 |
|
1 |
|a Gistrup, Denmark :
|b River Publishers,
|c [2017]
|
| 264 |
|
2 |
|a [Ann Arbor, Michigan] :
|b ProQuest Ebook Central.
|
| 264 |
|
4 |
|c ©2017
|
| 300 |
|
|
|a 1 online resource (xxxiv, 375 pages) :
|b illustrations (some colour).
|
| 336 |
|
|
|a text
|b txt
|2 rdacontent
|
| 337 |
|
|
|a computer
|b c
|2 rdamedia
|
| 338 |
|
|
|a online resource
|b cr
|2 rdacarrier
|
| 490 |
1 |
|
|a River Publishers series in automation, control and robotics
|
| 504 |
|
|
|a Includes bibliographical references and index.
|
| 505 |
0 |
|
|a 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 |
|
|a 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 |
|
|a 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 |
|
|a 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 |
|
|a 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.
|
| 520 |
|
|
|a 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, motivated by the importance of structured communication in modern software. Behavioural Types: from Theory to Tools presents programming languages and software tools produced by members of COST Action IC1201: Behavioural Types for Reliable Large-Scale Software Systems, a European research network that was funded from October 2012 to October 2016. As a survey of the most recent developments in the application of behavioural type systems, it is a valuable reference for researchers in the field, as well as an introduction to the area for graduate students and software developers.
|
| 545 |
0 |
|
|a Simon Gay, António Ravara
|
| 650 |
|
0 |
|a Programming languages (Electronic computers)
|
| 650 |
|
0 |
|a Type theory.
|
| 650 |
|
6 |
|a Théorie des types.
|
| 650 |
|
7 |
|a COMPUTERS / Programming / Software Development
|2 bisacsh
|
| 650 |
|
7 |
|a SCIENCE / Energy
|2 bisacsh
|
| 650 |
|
7 |
|a Programming languages (Electronic computers)
|2 fast
|
| 650 |
|
7 |
|a Type theory
|2 fast
|
| 655 |
|
7 |
|a Electronic books.
|2 local
|
| 700 |
1 |
|
|a Gay, Simon,
|d 1969-
|e editor.
|1 https://id.oclc.org/worldcat/entity/E39PCjKcxdjQ4rcP6VrK7RMCDC
|
| 700 |
1 |
|
|a Ravara, António,
|e editor.
|
| 710 |
2 |
|
|a Taylor & Francis.
|
| 776 |
0 |
8 |
|i Print version:
|t Behavioural types : from theory to tools.
|d Gistrup, Denmark : River Publishers, ©2017
|z 9788793519824
|
| 830 |
|
0 |
|a River Publishers series in automation, control and robotics.
|
| 856 |
4 |
0 |
|u https://www.taylorfrancis.com/books/9781003337331
|z Connect to the full text of this electronic book
|t 0
|
| 955 |
|
|
|a Taylor & Francis Open Access ebooks
|
| 994 |
|
|
|a 92
|b TXA
|
| 999 |
f |
f |
|s f89010e3-71b1-454a-aa7b-ea0fb4dc2ab1
|i fe04a493-d35e-4519-b275-38bd24a96c79
|t 0
|
| 952 |
f |
f |
|a Texas A&M University
|b College Station
|c Electronic Resources
|d Available Online
|t 0
|e QA76.7 .B44 2017
|h Library of Congress classification
|
| 998 |
f |
f |
|a QA76.7 .B44 2017
|t 0
|l Available Online
|