THE COMP SYSTEM

COMP is a structured specification language and analysis tool that supports the formal development of component-based systems. It is based on the behavioural-abstraction paradigm, which gives prominence to the observable behaviour of systems over their structural representations or the functions that they may perform.

The language is rigorously based upon hidden algebra. Its main programming units, called object modules, consist of hidden-algebra declarations of data or state sorts, data operations, actions, observations, and axioms that bring everything together and define the semantics of programs. Structured specifications are obtained through parallel, synchronized, and indexed compositions of object modules – a defining feature of COMP – which allow the construction of larger and more complex objects, in a hierarchical fashion, from simpler components.


Obtaining COMP

COMP is implemented in Maude 3 and is integrated into the SpeX specification framework. Therefore, in order to run COMP, you need to have both Maude version 3 and SpeX installed on your system.

There are two ways to obtain the source code of COMP:

  • either by downloading the latest distribution as a tar.gz file;
  • or by cloning the entire COMP repository.

On GNU/Linux or macOS machines, the simplest way to install COMP is by running the following scripts from the directory containing the COMP source tree: 


   ./configure
   make
   sudo make install

Documentation

The COMP tutorial is meant as a simple step-by-step introduction to COMP. It covers the installation of the tool and its basic use for the specification and analysis of a benchmark system.

The COMP user guide provides an overview of the capabilities of COMP, including all the specification and verification commands supported by the tool.

The COMP language definition gives an in-depth presentation of the mathematical foundations and of the syntax, semantics, and methodologies of the COMP specification language.

Examples

A technical report documenting the formal specification and verification of a medium-sized system involving ATMs, multiple users, bank account, and various interactions between them is available here.

Seven other smaller examples are discussed in the list below. The full source code of all COMP examples (including the case study) is available here.

Alternating bit protocol (ABP)

Gives a specification of the alternating bit protocol, a network protocol that keeps sending lost or corrupted messages using a FIFO communication channel until they are properly delivered. The protocol guarantees that messages are delivered in the same order in which they have been sent.

Learn more

This is the behavioural-object hierarchy used in the language-definition document. It covers compositions with a finite number of components (parallel or synchronized) as well as indexed compositions.

Learn more

Gives a specification of counter that alternates between two operating modes (increasing or decreasing) depending on the position of a switch (on or off). It's a simple example that illustrates the synchronized composition of two objects: the counter and the switch.

Learn more

Gives a specification of the access protocol QLock, a variant of Edsger Dijkstra's concept of binary semaphore that solves concurrency problems in systems with multiple execution threads. It covers synchronized and indexed compositions, and is used in the COMP tutorial.

Learn more

Gives a specification of a telephone system where users can call various numbers and the duration of the calls is logged. It's a simple example that illustrates indexed compositions and the analysis of a composed object obtained in this manner.

Learn more

This is a classic example of managing interactions between two objects: a server and a cashier, both parts of a vending machine. It emphasizes the use of various data types in defining objects and synchronized compositions.

Learn more

Gives a specification of wrist watch with two physical pushers used for setting the time by adjusting the minute and/or hour indicators. It covers synchronized compositions and object renamings, and is used in the COMP user guide.

Learn more

Publications

The seminal paper on behavioural specification for hierarchical object composition, which constitutes the mathematical foundation of the COMP specification language, is available here.

A talk on the underlying libraries that enabled the development of the COMP interpreter was given at the 26th International Workshop on Algebraic Development Techniques (WADT 2022). The slides of the presentation are available here.

License

The COMP source code is licensed under the GNU General Public License v2.0 or later.

Contact

The maintainers of the COMP system can be contacted by email.

Acknowledgements

This work was supported by a grant of the Romanian Ministry of Education and Research, CCCDI – UEFISCDI, project number PN-III-P2-2.1-PED-2019-0955, within PNCDI III.