Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Formal Analysis of the Contract Automata Runtime Environment with Uppaal: Modelling, Verification and Testing

Davide Basile

TL;DR

The paper addresses the challenge of ensuring dependable behaviour for CARE, a runtime environment for contract automata, by formalising its low-level interactions as a network of stochastic timed automata and verifying them with Uppaal. It combines exhaustive and statistical model checking with model-based testing to validate both the abstract model and its concrete CARE implementation, including a traceable link to source code. Key contributions include a bottom-up, open-source formal model that can be connected to the code via traceability, demonstration of deadlock- and error-free operation under realistic parameter settings, and generation of concrete tests (JUnit) from abstract Uppaal traces. The work demonstrates how formal methods can guide dependable development of distributed middleware, with artefacts and test suites publicly available and adaptable to evolving CARE configurations and implementations.

Abstract

Recently, a distributed middleware application called contract automata runtime environment (CARE) has been introduced to realise service applications specified using a dialect of finite-state automata. In this paper, we detail the formal modelling, verification and testing of CARE. We provide a formalisation as a network of stochastic timed automata. The model is verified against the desired properties with the tool Uppaal, utilising exhaustive and statistical model checking techniques. Abstract tests are generated from the Uppaal models that are concretised for testing CARE. This research emphasises the advantages of employing formal modelling, verification and testing processes to enhance the dependability of an open-source distributed application. We discuss the methodology used for modelling the application and generating concrete tests from the abstract model, addressing the issues that have been identified and fixed.

Formal Analysis of the Contract Automata Runtime Environment with Uppaal: Modelling, Verification and Testing

TL;DR

The paper addresses the challenge of ensuring dependable behaviour for CARE, a runtime environment for contract automata, by formalising its low-level interactions as a network of stochastic timed automata and verifying them with Uppaal. It combines exhaustive and statistical model checking with model-based testing to validate both the abstract model and its concrete CARE implementation, including a traceable link to source code. Key contributions include a bottom-up, open-source formal model that can be connected to the code via traceability, demonstration of deadlock- and error-free operation under realistic parameter settings, and generation of concrete tests (JUnit) from abstract Uppaal traces. The work demonstrates how formal methods can guide dependable development of distributed middleware, with artefacts and test suites publicly available and adaptable to evolving CARE configurations and implementations.

Abstract

Recently, a distributed middleware application called contract automata runtime environment (CARE) has been introduced to realise service applications specified using a dialect of finite-state automata. In this paper, we detail the formal modelling, verification and testing of CARE. We provide a formalisation as a network of stochastic timed automata. The model is verified against the desired properties with the tool Uppaal, utilising exhaustive and statistical model checking techniques. Abstract tests are generated from the Uppaal models that are concretised for testing CARE. This research emphasises the advantages of employing formal modelling, verification and testing processes to enhance the dependability of an open-source distributed application. We discuss the methodology used for modelling the application and generating concrete tests from the abstract model, addressing the issues that have been identified and fixed.
Paper Structure (34 sections, 13 figures, 2 tables)

This paper contains 34 sections, 13 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Related work
  3. Background
  4. Contract Automata
  5. Uppaal
  6. CARE
  7. Services
  8. Orchestrator
  9. Choices and Actions
  10. Methodology
  11. Modelling TCP/IP sockets communication
  12. Abstractions
  13. Traceability
  14. Remark
  15. Formal model
  16. ...and 19 more sections

Figures (13)

  • Figure 1: An example of contract automaton
  • Figure 2: The class diagram for the orchestrated services; the methods of the derived classes are visible in their super-class/interface as abstract methods (in italic)
  • Figure 3: The class diagram for the orchestrator; the methods of the derived classes are visible in their super-class/interface as abstract methods (in italic)
  • Figure 4: The sequence diagrams depicting the interactions implementing a centralised match action (on the left) and a distributed match action (on the right)
  • Figure 5: The Uppaal code used to model the TCP/IP socket communications
  • ...and 8 more figures

Theorems & Definitions (1)

  • Example 3.1