Healthcare Service

In this use case centred around healthcare, we exemplify how developers can compose locally the libraries generated by independent choreographies.

Suppose that a “healthcare service” in a hospital needs to gather sensitive data about vital signs (we call them vitals) from some IoT devices (e.g., smartwatches, heart monitors), and then upload them to the cloud for storage. This is a typical scenario that requires integration of libraries for participating in choreographies at the local level. We shall carry out the following two steps.

  1. Define a new choreography class, called VitalsStreaming, that prescribes how data should be streamed from an IoT Device monitoring the vitals of a patient to a data Gatherer; this choreography will enforce that the Gatherer processes only data that is (a) correctly cryptographically signed by the device and (b) pseudonymised.

  2. Implement the healthcare service a local Java class, called HealthCareService, that com- bines the Java library compiled from VitalsStreaming to gather data from the IoT devices with the Java library compiled from our previous DistAuth example to authenticate with the cloud storage service through a third-party service (this could be, e.g., a national authentication system) and upload the data.

Vitals choreographies

public enum StreamState@R { ON, OFF }

public VitalsStreamingHelper@A {
  private static Vitals@A pseudonymise( Vitals@A vitals ) { /*...*/ }
  private static Boolean@A checkSignature( Signature@A signature ) { /*...*/ }

public class VitalsStreaming@( Device, Gatherer ) {
  private SymChannel@( Device, Gatherer )< Object > ch; 
  private Sensor@Device sensor;

  public VitalsStreaming( 
    SymChannel@( Device, Gatherer )< Object > ch, 
    Sensor@Device sensor 
  ) { = ch;
    this.sensor = sensor; 
  public void gather( Consumer@Gatherer< Vitals > consumer ) {
    if ( sensor.isOn() ) {
      ch.< StreamState >select( StreamState@Device.ON );
      VitalsMsg@Gatherer msg = 
      >> ch::< Vitals >com; 
      if ( checkSignature( msg.signature() ) ){
        >> VitalsStreamingHelper::pseudonymise 
        >> consumer::accept;
    } else {
      ch.< StreamState >select( StreamState@Device.OFF ); 

Try it yourself: see the source code on .

In class VitalsStreaming composes a channel between the Device and the Gatherer and a Sensor object located at the Device (for obtaining the local vital readings).

Method pseudonymises personal data in Vitals at the Gatherer. Likewise, method checkSignature is used by the Gatherer uses to check that a message signature is valid. (We omit the bodies of these two static methods, which are standard local methods.)

The interesting part of this class is method gather. The Device checks whether its sensor is on and informs the Gatherer of the result with appropriate selections for knowlegde of choice. If the sensor is on, then Device sends its next available reading to Gatherer. Gatherer now checks that the message is signed correctly; if so, it pseudonymises the content of the message and then hands it off to a local consumer function. Notice that Gatherer does not need to inform Device of its local choice, since it does not affect the code that Device needs to run. We then recursively invoke gather to process the next reading.

Local code of the healthcare service

To conclude the use case, we define the local implementation of the healthcare service. The healthcare service acts as the Gatherer in the VitalsStreaming choreography (to gather the data) and as the Client in the DistAuth choreography (to authenticate with the cloud storage). So we compose the compiled Java classes VitalsStreaming_Gatherer and DistAuth_Client, respectively. The code of this local implementation is given below.

import DistAuth_Client; // From the DistAuth choreography
import VitalsStreaming_Gatherer; // From the VitalsStreaming choreography public class 

public class HealthCareService {
  public static void main() {
    TLSChannel_A toIP = HealthIdentityProvider.connect();
    TLSChannel_A toStorage = HealthDataStorage.connect();
    AuthResult_A authResult = new DistAuth_Client( toIP )
      .authenticate( getCredentials() );
    authResult.left().ifPresent( token -> {
      .map( Device::connect )
      .map( VitalsStreaming_Gatherer::new )
      .forEach( vs -> vs.gather( data -> new StorageMesg( token, data ) ) ) 
  private static Credentials getCredentials() { /* ... */ } 

The interesting part is the main method of the HealthCareService, which interweaves local computation using the standard Java library and the libraries generated by our compiler. In the method, we use auxiliary methods to connect to the identity provider for authentication (which implements IP in DistAuth) and the data storage service (which implements Service in DistAuth)—we assume that these services are provided by third parties, e.g., the national health system and some cloud provider. After the connection, we run our distributed authentication protocol as the Client, checking check if we succesfully received an authentication token by inspecting the optional result. If so we: obtain a parallel stream of Device objects from a local registry of devices; connect to each device in parallel, which maps devices to channels; and use each channel to create a respective instance of VitalsStreaming_Gatherer (the code compiled by Choral to implement Gatherer in VitalsStreaming). Finally, we launch the gather method to engage in the VitalsStreaming choreography with each device, passing as a consumer function a lambda expression that sends the received data to the cloud storage service (including the authentication token). Notice that we do not need to worry about pseudonymisation nor signature checking in the local code, since all these details are dealt with by the code compiled from VitalsStreaming.