Muutke küpsiste eelistusi

E-raamat: Behavioural Types: From Theory to Tools

Edited by (University of Glasgow, UK), Edited by (Universidade Nova de Lisboa, Portugal)
Teised raamatud teemal:
  • Formaat - PDF+DRM
  • Hind: 42,11 €*
  • * hind on lõplik, st. muud allahindlused enam ei rakendu
  • Lisa ostukorvi
  • Lisa soovinimekirja
  • See e-raamat on mõeldud ainult isiklikuks kasutamiseks. E-raamatuid ei saa tagastada.
Behavioural Types: From Theory to ToolsSuurem pilt
Teised raamatud teemal:

DRM piirangud

  • Kopeerimine (copy/paste):

    ei ole lubatud

  • Printimine:

    ei ole lubatud

  • Kasutamine:

    Digitaalõiguste kaitse (DRM)
    Kirjastus on väljastanud selle e-raamatu krüpteeritud kujul, mis tähendab, et selle lugemiseks peate installeerima spetsiaalse tarkvara. Samuti peate looma endale  Adobe ID Rohkem infot siin. E-raamatut saab lugeda 1 kasutaja ning alla laadida kuni 6'de seadmesse (kõik autoriseeritud sama Adobe ID-ga).

    Vajalik tarkvara
    Mobiilsetes seadmetes (telefon või tahvelarvuti) lugemiseks peate installeerima selle tasuta rakenduse: PocketBook Reader (iOS / Android)

    PC või Mac seadmes lugemiseks peate installima Adobe Digital Editionsi (Seeon tasuta rakendus spetsiaalselt e-raamatute lugemiseks. Seda ei tohi segamini ajada Adober Reader'iga, mis tõenäoliselt on juba teie arvutisse installeeritud )

    Seda e-raamatut ei saa lugeda Amazon Kindle's. 

Behavioral type systems in programming languages support the specification and verification of programs’ properties 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 behavioral type systems, this text is a valuable reference for researchers in the field as well as an introduction to the subject for graduate students and software developers.
Preface xv
Acknowledgments xix
List of Contributors xxi
List of Figures xxv
List of Tables xxxi
List of Abbreviations xxxiii
1 Contract-Oriented Design of Distributed Applications: A Tutorial 1(26)
Nicola Atzei
Massimo Bartoletti
Maurizio Murgia
Emilio Tuosto
Roberto Zunino
1.1 Introduction
2(2)
1.1.1 From Service-Oriented to Contract-Oriented Computing
2(1)
1.1.2 Honesty Attacks
3(1)
1.1.3 Diogenes
4(1)
1.2 Specifying Contract-Oriented Services in CO2
4(4)
1.2.1 Contracts
5(1)
1.2.2 Processes
5(1)
1.2.3 An Execution Context
6(1)
1.2.4 Adding Recursion
7(1)
1.3 Honesty
8(6)
1.3.1 A Simple Dishonest Store
8(2)
1.3.2 A More Complex Dishonest Store
10(1)
1.3.3 Handling Failures
11(2)
1.3.4 An Honest Store, Finally
13(1)
1.3.5 A Recursive Honest Store
13(1)
1.4 Refining CO2 Specifications in Java Programs
14(5)
1.4.1 Compilation of CO2 Specifications into Java Skeletons
15(2)
1.4.2 Checking Honesty of Refined Java Programs
17(2)
1.5 Conclusions
19(3)
1.5.1 Related Work
20(2)
References
22(5)
2 Contract-Oriented Programming with Timed Session Types 27(22)
Nicola Atzei
Massimo Bartoletti
Tiziana Cimoli
Stefano Lande
Maurizio Murgia
Alessandro Sebastian Podda
Livio Pompianu
2.1 Introduction
27(2)
2.2 Timed Session Types
29(7)
2.2.1 Specifying Contracts
29(2)
2.2.2 Compliance
31(4)
2.2.3 Run-Time Monitoring of Contracts
35(1)
2.3 Contract-Oriented Programming
36(7)
2.3.1 A Simple Store
37(1)
2.3.2 A Simple Buyer
37(1)
2.3.3 A Dishonest Store
38(2)
2.3.4 An Honest Store
40(1)
2.3.5 A Recursive Honest Store
41(2)
2.4 Conclusions
43(3)
2.4.1 Related Work
44(2)
References
46(3)
3 A Runtime Monitoring Tool for Actor-Based Systems 49(28)
Duncan Paul Attard
Ian Cassar
Adrian Francalanza
Luca Aceto
Anna Ingolfsdottir
3.1 Introduction
49(2)
3.2 Background
51(6)
3.2.1 Runtime Monitoring Criteria
52(1)
3.2.2 A Branching-Time Logic for Specifying Correctness Properties
52(3)
3.2.3 Monitoring muHML
55(2)
3.3 A Tool for Monitoring Erlang Applications
57(6)
3.3.1 Concurrency-Oriented Development Using Erlang
57(1)
3.3.2 Reasoning about Data
58(4)
3.3.2.1 Properties with specific PIDs
61(1)
3.3.2.2 Further reasoning about data
61(1)
3.3.3 Monitor Compilation
62(1)
3.4 detectEr in Practice
63(10)
3.4.1 Creating the Target System
64(4)
3.4.1.1 Setting up the Erlang project
64(2)
3.4.1.2 Running and testing the server
66(2)
3.4.2 Instrumenting the Test System
68(5)
3.4.2.1 Property specification
68(1)
3.4.2.2 Monitor synthesis and instrumentation
69(1)
3.4.2.3 Running the monitored system
70(1)
3.4.2.4 Running the correct server
71(2)
3.5 Conclusion
73(1)
3.5.1 Related and Future Work
73(1)
References
74(3)
4 How to Verify Your Python Conversations 77(22)
Rumyana Neykova
Nobuko Yoshida
4.1 Framework Overview
78(1)
4.2 Scribble-Based Runtime Verification
79(3)
4.2.1 Verification Steps
79(2)
4.2.2 Monitoring Requirements
81(1)
4.3 Conversation Programming in Python
82(3)
4.4 Monitor Implementation
85(2)
4.5 Monitoring Interruptible Systems
87(7)
4.5.1 Use Case: Resource Access Control (RAC)
88(2)
4.5.2 Interruptible Multiparty Session Types
90(1)
4.5.3 Programming and Verification of Interruptible Systems
91(3)
4.5.4 Monitoring Interrupts
94(1)
4.6 Formal Foundations of MPST-Based Runtime Verification
94(2)
4.7 Concluding Remarks
96(1)
References
97(2)
5 The DCR Workbench: Declarative Choreographies for Collaborative Processes 99(26)
Soren Debois
Thomas T. Hildebrandt
5.1 Introduction
99(3)
5.1.1 History of the DCR Workbench
100(1)
5.1.2 The DCR Workbench
101(1)
5.2 Running Example
102(1)
5.3 Dynamic Condition-Response Graphs
102(5)
5.3.1 Event States
102(1)
5.3.2 Relations
103(1)
5.3.3 Executing Events
104(1)
5.3.4 Formal Development
105(2)
5.4 Modelling with the Workbench
107(4)
5.4.1 Inputting a Model: The Parser Panel
107(3)
5.4.2 Visualisation and Simulation: The Visualiser and Activity Log Panels
110(1)
5.5 Refinement
111(4)
5.6 Time
115(2)
5.7 Subprocesses
117(2)
5.8 Data
119(1)
5.9 Other Panels
120(1)
5.10 Conclusion
120(1)
References
121(4)
6 A Tool for Choreography-Based Analysis of Message-Passing Software 125(22)
Julien Lange
Emilio Tuosto
Nobuko Yoshida
6.1 Introduction
126(1)
6.2 Overview of the Theory
127(5)
6.3 Architecture
132(3)
6.4 Modelling of an ATM Service
135(6)
6.4.1 ATM Service - Version 1
136(1)
6.4.2 ATM Service - Version 2
137(4)
6.4.3 ATM Service - Version 3 (fixed)
141(1)
6.5 Conclusions and Related Work
141(3)
References
144(3)
7 Programming Adaptive Microservice Applications: an AIOCJ Tutorial 147(22)
Saverio Giallorenzo
Ivan Lanese
Jacopo Mauro
Maurizio Gabbrielli
7.1 Introduction
147(3)
7.2 AIOCJ Outline
150(3)
7.2.1 AIOCJ Architecture and Workflow
151(2)
7.3 Choreographic Programming
153(2)
7.4 Integration with Legacy Software
155(3)
7.5 Adaptation
158(4)
7.6 Deployment and Adaptation Procedure
162(3)
7.7 Conclusion
165(1)
References
166(3)
8 JaDA - the Java Deadlock Analyzer 169(24)
Abel Garcia
Cosimo Laneve
8.1 Introduction
169(2)
8.2 Example
171(2)
8.3 Overview of JaDA's Theory
173(8)
8.3.1 The Abstract Behavior of the Network Class
173(2)
8.3.2 Behavioral Type Inference
175(2)
8.3.3 Analysis of Behavioral Types
177(4)
8.4 The JaDA Tool
181(6)
8.4.1 Prerequisites
181(1)
8.4.2 The Architecture
181(3)
8.4.3 The Current JVML Coverage
184(2)
8.4.4 Tool Configuration
186(1)
8.4.5 Deliverables
187(1)
8.5 Current Limitations
187(2)
8.6 Related Tools and Assessment
189(1)
8.7 Conclusions
190(1)
References
191(2)
9 Type-Based Analysis of Linear Communications 193(26)
Luca Padovani
9.1 Language
193(4)
9.2 Type System
197(8)
9.3 Extended Examples
205(9)
9.3.1 Fibonacci Stream Network
205(2)
9.3.2 Full-Duplex and Half-Duplex Communications
207(2)
9.3.3 Load Balancing
209(1)
9.3.4 Sorting Networks
210(2)
9.3.5 Ill-typed, Lock-free Process Networks
212(2)
9.4 Related Work
214(1)
References
215(4)
10 Session Types with Linearity in Haskell 219(24)
Dominic Orchard
Nobuko Yoshida
10.1 Introduction
219(3)
10.2 Pre-Session Types in Haskell
222(4)
10.2.1 Tracking Send and Receive Actions
223(1)
10.2.2 Partial Safety via a Type-Level Function for Duality
224(1)
10.2.3 Limitations
225(1)
10.3 Approaches in the Literature
226(13)
10.3.1 Note on Recursion and Duality
227(1)
10.3.2 Single Channel
227(2)
10.3.3 Multi-Channel Linearity
229(4)
10.3.4 An Alternate Approach
233(2)
10.3.5 Multi-Channels with Inference
235(1)
10.3.6 Session Types via Effect Types
236(2)
10.3.7 GV in Haskell
238(1)
10.4 Future Direction and Open Problems
239(1)
References
240(3)
11 An OCaml Implementation of Binary Sessions 243(22)
Hernan Melgratti
Luca Padovani
11.1 An API for Sessions
244(1)
11.2 A Few Simple Examples
245(3)
11.3 API Implementation
248(7)
11.4 Extended Example: The Bookshop
255(5)
11.5 Related Work
260(1)
References
261(4)
12 Lightweight Functional Session Types 265(22)
Sam Lindley
J. Garrett Morris
12.1 Introduction
265(1)
12.2 A First Look
266(4)
12.3 The Core Language
270(8)
12.3.1 Syntax
270(4)
12.3.2 Typing and Kinding Judgments
274(4)
12.4 Extensions
278(3)
12.4.1 Recursion
278(1)
12.4.2 Access Points
279(2)
12.5 Links with Session Types
281(3)
12.5.1 Design Choices
282(1)
12.5.2 Type Reconstruction
283(1)
12.6 Conclusion and Future Work
284(1)
References
284(3)
13 Distributed Programming Using Java APIs Generated from Session Types 287(22)
Raymond Hu
13.1 Background: Distributed Programming in Java
287(3)
13.1.1 TCP Sockets
288(2)
13.1.2 Java RMI
290(1)
13.2 Scribble Endpoint API Generation: Toolchain Overview
290(11)
13.2.1 Global Protocol Specification
291(3)
13.2.2 Endpoint API Generation
294(3)
13.2.3 Hybrid Session Verification
297(2)
13.2.4 Additional Math Service Endpoint Examples
299(2)
13.3 Real-World Case Study: HTTP (GET)
301(4)
13.3.1 H 1-1'P in Scribble: First Version
302(1)
13.3.2 HTTP in Scribble: Revised
303(2)
13.4 Further Endpoint API Generation Features
305(2)
References
307(2)
14 Mungo and StMungo: Tools for Typechecking Protocols in Java 309(20)
Ornela Dardha
Simon J. Gay
Dimitrios Kouzapas
Roly Perera
A. Laura Voinea
Florian Weber
14.1 Introduction
309(2)
14.2 Mungo: Typestate Checking for Java
311(4)
14.2.1 Example: Iterator
312(3)
14.3 StMungo: Typestates from Communication Protocols
315(5)
14.3.1 Example: Travel Agency
316(4)
14.4 POP3: Typechecking an Internet Protocol Client
320(6)
14.4.1 Challenges of Using Mungo and StMungo in the Real World
324(2)
14.5 Related Work
326(1)
References
327(2)
15 Protocol-Driven MPI Program Generation 329(24)
Nicholas Ng
Nobuko Yoshida
15.1 Introduction
329(2)
15.2 Pabble: Parameterised Scribble
331(2)
15.3 MPI Backbone
333(1)
15.3.1 MPI Backbone Generation from Ring Protocol
334(1)
15.4 Computation Kernels
334(4)
15.4.1 Writing a Kernel
335(3)
15.4.1.1 Initialisation
336(1)
15.4.1.2 Passing data between backbone and kernel through queues
336(1)
15.4.1.3 Predicates
337(1)
15.5 The Pabble Language
338(4)
15.5.1 Global Protocols Syntax
338(3)
15.5.1.1 Restriction on constants
340(1)
15.5.2 Local Protocols
341(1)
15.6 MPI Backbone Generation
342(6)
15.6.1 Interaction
342(2)
15.6.2 Parallel Interaction
344(1)
15.6.3 Internal Interaction
344(1)
15.6.4 Control-flow: Iteration and For-loop
345(1)
15.6.5 Control-flow: Choice
345(1)
15.6.6 Collective Operations: Scatter, Gather and All-to-all
346(2)
15.6.7 Process Scaling
348(1)
15.7 Merging MPI Backbone and Kernels
348(2)
15.7.1 Annotation-Guided Merging Process
348(1)
15.7.2 Kernel Function
349(1)
15.7.3 Datatypes
349(1)
15.7.4 Conditionals
350(1)
15.8 Related Work
350(1)
15.9 Conclusion
350(1)
References
351(2)
16 Deductive Verification of MPI Protocols 353(20)
Vasco T. Vasconcelos
Francisco Martins
Eduardo R.B. Marques
Nobuko Yoshida
Nicholas Ng
16.1 Introduction
353(2)
16.2 The Finite Differences Algorithm and Common Coding Faults
355(3)
16.3 The Protocol Language
358(4)
16.4 Overview of the Verification Procedure
362(2)
16.5 The Marking Process
364(4)
16.6 Related Work
368(1)
16.7 Conclusion
369(1)
References
370(3)
Index 373(2)
About the Editors 375
Simon Gay, António Ravara
Lisainfo e-raamatute kohta Lisainfo e-raamatute kohta
Püsilink: https://www.kriso.ee/db/97810007992552e.html