From specifications to concrete processes

This project aims at studying a dynamic logic with binders, and (automatic) translations from specifications in (some fragment) of this logic into a concrete process algebra.

The quest for logics and formal methods for the rigorous development of reactive software, i.e. systems which interact with their environment along the whole computation, and not only in its starting and termination points [1], is an active topic of research in Computer Science. Typical approaches start from the construction of a concrete model (e.g. in the form of a transition system [8], or a process algebra expression [5, 2]) upon which the relevant properties are later formulated in a suitable (modal) logic and typically verified by some form of model-checking. Resorting to old software engineering jargon, most of these approaches proceed by inventing & verifying.

We intend, however, to contribute to the field following an alternative correct by construction perspective; loose specification has an important role to play, because they support the gradual addition of requirements and implementation decisions such that verification of the correctness of a complex system can be done piecewise in smaller steps. This entails the adoption of a logic, orthogonal to the entire development process, suitable to express requirements on various levels of abstraction, from property specifications, concerning e.g. safety and liveness requirements, to constructive specifications representing concrete processes. In this view, Dynamic Logic with Binders D↓ was recently introduced in [6], combining in the same formalism binders of hybrid logic [3] with regular modalities of dynamic logics [4].

Goal

Actually, D↓-logic is suited to directly express process structures and, thus, the implementation of abstract requirements. The binder operator is crucial for this. The ability to give names to visited states, together with the modal features to express transitions, makes possible a precise description of the whole dynamics of a process in a single sentence. Binders allow to express recursive patterns, namely loop transitions (from the current to some visited state). In fact we have no way to make this kind of specification in the absence of a feature to refer to specific states in a model, as in standard modal logic. For example, sentence

↓ x0. ⟨a⟩x0 ∧ ⟨b⟩ ↓ x1.(⟨a⟩x0 ∧ ⟨b⟩x1)

specifies a process with two states accepting actions a and b respectively. This can be easily translated into a process definition in a given process algebra, for instance into the declaration

{x0 = a.x0 + b.x1, x1 = b.x1 + a.x0}

in CCS [7].

The aim of this work is to make a systematic study of these translations and the implementation of an automatic translator from specifications in (a fragment) of D↓ into terms of a concrete process algebra.

Relevant literature

1. L. Aceto, A. Ingólfsdóttir, K. G. Larsen, and J. Srba. Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, 2007.
2. J. C. M. Baeten, T. Basten, and M. A. Reniers. Process Algebra: Equational theories of communicating processes. Cambridge University Press, 2010.
3. T. Braüner. Hybrid Logic and its Proof-Theory. App. Logic Series. Springer, 2010.
4. D. Harel, D. Kozen, and J. Tiuryn. Dynamic Logic. MIT Press, 2000.
5. C. A. R. Hoare. Communicating Sequential Processes. Series in Computer Science. Prentice-Hall International, 1985.
6. A. Madeira, L. Barbosa, R. Hennicker, and M. Martins. Dynamic logic with binders and its applications to the developmet of reactive systems (extended with proofs). Technical Report available from http://alfa.di.uminho.pt/~madeira/main_files/extreport.pdf, 2016.
7. R. Milner. Communication and concurrency. PHI Series in computer science. Prentice Hall, 1989.
8. G. Winskel and M. Nielsen. Models for concurrency. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science (Vol. 4), pages 1–148. Oxford University Press, Oxford, UK, 1995.