Contract Automata Runtime Environment (CARE)

CARE is a library for implementing applications specified via contract automata.

CARE provides a runtime environment to coordinate the CARE services that are implementing the contracts of the synthesised orchestration.

Thus, CARE is the missing piece between specifications through contract automata and their implementations, so making explicit the low-level interactions realising the prescribed actions.

Scientific Publications

Basile, D., ter Beek, M.H. (2023). A Runtime Environment for Contract Automata. In: Chechik, M., Katoen, JP., Leucker, M. (eds) Formal Methods. FM 2023. Lecture Notes in Computer Science, vol 14000. Springer, Cham. https://doi.org/10.1007/978-3-031-27481-7_31

Basile, D., 2024, June. Modelling, Verifying and Testing the Contract Automata Runtime Environment with Uppaal. In International Conference on Coordination Models and Languages (pp. 93-110). Cham: Springer Nature Switzerland. https://doi.org/10.1007/978-3-031-62697-5_6

Install

The Contract Automata Runtime Environment is released as a GitHub Package, simply add this dependency to the pom.xml of your Maven project.

<dependency>
  <groupId>io.github.contractautomataproject</groupId>
  <artifactId>care</artifactId>
  <version>1.0.0</version>
</dependency>

Usage

Check https://github.com/ContractAutomataProject/CARE_Examples for examples of usage of CARE.

Class Diagram

This is the main class diagram of CARE.

Two main elements of CARE are the abstract classes RunnableOrchestratedContract and RunnableOrchestration. This last one is a special service that reads the synthesised orchestration and orchestrates the RunnableOrchestratedContract to realise the overall application. Each RunnableOrchestratedContract is a wrapper responsible for pairing the specification of a service (the contract) with its implementation. This wrapper is listening for invocation commands from the orchestrator, and replies by invoking the corresponding method. In case the invocation is not allowed by the contract, or in case an interaction terminates prior to the fulfilment of the contract, a ContractViolationException is raised registering the remote host violating the contract. This guarantees the adherence of the implementation to the specification and allows for accountability.

Both RunnableOrchestratedContract and RunnableOrchestration abstract from the way in which a choice is made, in the presence of branches or termination. This is abstracted by the method choice.
Currently two implementations are DictatorialChoice (the orchestrator chooses alone) and MajoritarianChoice (services vote and the majority wins). The other aspect to concretize is the implementation of an action of a contract. This is abstracted by the interfaces OrchestratedAction and OrchestratorAction, to which, respectively, RunnableOrchestratedContract and RunnableOrchestration depends upon. Currently, two implementations for the actions are CentralAction (the orchestrator acts as a proxy) and DistributedAction (the services involved in the action interacts with each other and the orchestrator). When initialised, RunnableOrchestration checks that all the involved RunnableOrchestratedContract have a compatible configuration (in terms of choice and action implementations).

A class TypedCALabel extending the class CALabel of CATLib is used to add the type of the parameter and the returned value to each action. Thus for a match between a request and an offer it is also required that their types are compatible (i.e. returned values are supertypes of the parameters of the complementary actions).

Formal Model Verification

CARE has been formally modelled as a network of stochastic timed automata and verified using the tool Uppaal. The formal model provides a detailed documentation of the behaviour of the software with traceability information relating the model to the source code. For more information check the README file located under the folder src/spec/uppaal.