This paper describes Djed, a stablecoin protocol that behaves like an autonomous central bank that buys and sells its currency (the stablecoin) for a price in a range that is pegged to a target price. It is crypto-backed in the sense that the bank keeps a volatile cryptocurrency in its reserve. The reserve is used to buy stablecoins from users that want to sell them. And revenue from sales of stablecoins to users is stored in the reserve. Besides stablecoins, the protocol also trades reservecoins in order to capitalize itself and maintain a reserve ratio significantly greater than one. To the best of our knowledge, this is the first implemented stablecoin protocol where stability claims are precisely and mathematically stated and proven. Furthermore, the claims and their proofs are formally verified using two different techniques: bounded model checking, to exhaustively search for counterexamples to the claims or to establish invariant satisfaction; and interactive theorem proving, to build rigorous formal proofs using a proof assistant with automated theorem proving features.

We report on our industrial experience in using formal methods for the analysis of safety-critical systems developed in a model-based design framework. We first highlight the formal proof workflow devised for the verification and validation of embedded systems developed in Matlab/Simulink. In particular, we show that there is a need to: determine the compatibility of the model to be analysed with the proof engine, establish whether the model facilitates proof convergence or when optimisation is required, and avoid over-specification when specifying the hypotheses constraining the inputs of the model during analysis. We also stress on the importance of having a certain harness over the proof activity and present a set of tools we developed to achieve this purpose. Finally, we give a list of best practices, methods and any necessary tools aiming at guaranteeing the validity of the verification results obtained.

We propose an automatic transformation of Focal specifications to UML class diagrams. The main motivation for this work lies within the framework of the EDEMOI project, which aims to integrate and apply several requirements engineering and formal methods techniques to analyze regulations in the domain of airport security. The idea is to provide a graphical documentation of formal models for developers, and in the long-term, for certification authorities. The transformation is formally described and an implementation has been designed. We also provide a concrete example coming from the EDEMOI project.

We present the validation of regulations intended to ensure airport security in the framework of civil aviation. In particular, we describe the proofs of correctness/completeness for two standards, one at the international level and the other at the European level, and we show how the properties of the European level refines those of the international level. These models are expressed using the Focal environment, an object-oriented specification and proof system, and the proofs described by means of a declarative-like language are processed by the automated theorem prover Zenon. We show how Zenon appears quite appropriate when dealing with abstract specifications like our case study, but also how it should be controlled to present readable proofs.