![]() |
![]() |
Editors: Jorge A. Pérez and Nobuko Yoshida
This Special Issue of LMCS collects full versions of four selected papers presented at the 39th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2019), which was held in Kongens Lyngby, Denmark, on June 17–21, 2019. FORTE 2019 was one of the three conferences of DisCoTec 2019, the 14th International Federated Conference on Distributed Computing Techniques.
FORTE is a forum for fundamental research on theory, models, tools, and applications for distributed systems. It covers models and formal specification, testing and verification methods for distributed computing.
In the 2019 edition of FORTE, 15 full paper submissions were accepted for presentation. Four of those were selected for this Special Issue, based on the referee reports we received for their conference versions and their presentations at the conference. Authors were asked to revise and complement the version presented at FORTE with omitted proofs and other new material. The extended version of each paper has undergone the usual reviewing process of LMCS, in accordance with its high standards.
The selected papers witness the high quality of the scientific program of FORTE 2019. They address process algebra, information flow, refinement checking, and timed automata.
We would like to thank the authors for their efforts in producing the extended versions contained in this Special Issue. We are very grateful to the expert reviewers for their careful reading. We would also like to thank the program committee of FORTE 2019, for their expert evaluation of the papers presented at the conference. Finally, we wish to thank the Editor-in-Chief and Executive Editors for accepting to publish this Special Issue and for their support during its preparation.
May 2021
Jorge A. Pérez and Nobuko Yoshida
Program Chairs FORTE 2019
Guest Editors of the Special Issue
Psi-calculi is a parametric framework for process calculi similar to popular pi-calculus extensions such as the explicit fusion calculus, the applied pi-calculus and the spi calculus. Mechanised proofs of standard algebraic and congruence properties of bisimilarity apply to all calculi within the framework. A limitation of psi-calculi is that communication channels must be symmetric and transitive. In this paper, we give a new operational semantics to psi-calculi that allows us to lift these restrictions and simplify some of the proofs. The key technical innovation is to annotate transitions with a provenance -- a description of the scope and channel they originate from. We give mechanised proofs that our extension is conservative, and that the standard algebraic and congruence properties of strong and weak bisimilarity are maintained. We show correspondence with a reduction semantics and barbed bisimulation. We show how a pi-calculus with preorders that was previously beyond the scope of psi-calculi can be captured, and how to encode mixed choice under very strong quality criteria.
The notion of refinement plays an important role in software engineering. It is the basis of a stepwise development methodology in which the correctness of a system can be established by proving, or computing, that a system refines its specification. Wang et al. describe algorithms based on antichains for efficiently deciding trace refinement, stable failures refinement and failures-divergences refinement. We identify several issues pertaining to the soundness and performance in these algorithms and propose new, correct, antichain-based algorithms. Using a number of experiments we show that our algorithms outperform the original ones in terms of running time and memory usage. Furthermore, we show that additional run time improvements can be obtained by applying divergence-preserving branching bisimulation minimisation.
Constant-time programming is a countermeasure to prevent cache based attacks where programs should not perform memory accesses that depend on secrets. In some cases this policy can be safely relaxed if one can prove that the program does not leak more information than the public outputs of the computation. We propose a novel approach for verifying constant-time programming based on a new information flow property, called output-sensitive noninterference. Noninterference states that a public observer cannot learn anything about the private data. Since real systems need to intentionally declassify some information, this property is too strong in practice. In order to take into account public outputs we proceed as follows: instead of using complex explicit declassification policies, we partition variables in three sets: input, output and leakage variables. Then, we propose a typing system to statically check that leakage variables do not leak more information about the secret inputs than the public normal output. The novelty of our approach is that we track the dependence of leakage variables with respect not only to the initial values of input variables (as in classical approaches for noninterference), but taking also into account the final values of output variables. We adapted this approach to LLVM IR and we developed a prototype to verify LLVM implementations.
We introduce a new class of Parametric Timed Automata (PTAs) where we allow clocks to be compared to parameters in guards, as in classic PTAs, but also to be updated to parameters. We focus here on the EF-emptiness problem: "is the set of parameter valuations for which some given location is reachable in the instantiated timed automaton empty?". This problem is well-known to be undecidable for PTAs, and so it is for our extension. Nonetheless, if we update all clocks each time we compare a clock with a parameter and each time we update a clock to a parameter, we obtain a syntactic subclass for which we can decide the EF-emptiness problem and even perform the exact synthesis of the set of rational valuations such that a given location is reachable. To the best of our knowledge, this is the first non-trivial subclass of PTAs, actually even extended with parametric updates, for which this is possible.