H is a tool for formal specification and verification of reconfigurable systems. These are software systems that behave differently in different modes of operation (often called configurations) and commute between them along their lifetime.
H supports a dedicated generic logic-based specification language for reconfigurable systems. The genericity of the language is given by the fact that the formalism used for specifying the local behavior of the system, for each configuration, can be freely chosen by the user as the most appropriate for the given requirements. Proof support for the specification language is obtained via a generic methodology of proof-by-translation, when a conjecture is first translated to first-order logic then verified there using automated first-order provers.
The system is available in two distributions:
Warning for slow connections: each of the two binary files is about 95 Mb large.
To install the H system, first install Hets:
$ sudo apt-get install software-properties-common
$ sudo apt-add-repository ppa:hets/hets
$ sudo apt-get update
$ sudo apt-get install hets-desktop-all
The source code of the project is freely available on a Git development branch of Hets. You can get it with
$ git clone https://github.com/spechub/Hets.git
$ cd Hets
$ git checkout rigid_casl
The next step is to setup the compilation of the Hets sources, following the instructions at Build Hets using Stack, then to compile the H source code with
$ make
The H user guide provides an introduction to using the H system.
The H language definition gives a complete formal overview on the syntax and the semantics of the H specification language.
This video shows how to further extend an existing definition of hybridized logic in H, how to analyze a specification in the newly generated hybridized logic and how to check whether a conjecture is true or not for it.
A library of examples is available.
Larger case studies are the specification of a steam boiler control system and a design of a bike-sharing-system.
The seminal paper of the H language by R. Diaconescu. It surveys to a greater extent its concept and its mathematical foundations, and only briefly its current implementation and some case studies.
A paper on the Hets-based implementation of H by M. Codescu.
A larger case study by I. Țuțu, C.E. Chiriță, A. Lopes, and J.L. Fiadeiro on the use of H for the design and analysis of a bike-sharing system.
Copyright © 2018-2020, Razvan Diaconescu, IMAR
The Hets source code is licensed under the GPLv2 or higher.