Dynamic logics for cyberphysical systems: towards contract based design
Start Date: 
July, 2016
End Date: 
June, 2019

Contractbased design, a development paradigm orthogonal to a vast number of software development methods, provides a rigorous basis for compositional analysis, verification and refinement. Actually, its potential goes far beyond the obvious support to maintenance and documentation of complex systems. It also paves the way to their modularization in sets of components mutually constrained by contractual obligations, therefore setting the ground for property elicitation, validation, inference and synthesis.

It is now consensual that system design can no longer rely on adhoctweaking techniques. A rigorous discipline is crucial to boost productivity and enforce correctness. Our starting point is that such a discipline could build on the contract paradigm, although a generic, unified view of contracts is still missing. This is particularly evident in the emerging domain of Cyber Physical Systems (CPS) where the difficulty of rigorously model the interactions among heterogeneous components, and the physical and cyber sides remains a serious obstacle to their efficient realization.

A recent survey published in J. Sifakis Festschrift [NV14], recalls that “while in traditional embedded system design the physical system is regarded as given, the emphasis of CPS design is instead on managing dynamics, time, and concurrency by orchestrating networked, distribute computational resources together with the physical systems.” Dealing appropriately with their design requires languages amenable to mathematical analysis and verification, so that assessing system correctness is no longer left to simulation and prototyping.

This project aims at contributing to the definition of a generic methodology for design, modelling and verification of CPS, resorting to contracts to build reliable abstractions of (discrete, continuous, mixed) components and enable hierarchical and compositional development . Such contracts will reflect the interaction of control software with physical environments, expose/constraint behaviour and functionality (which in CPS arises from interweaved loci of sensing, actuation, connectivity, computation, storage and energy), in a way that ensures (or at least, measures) predictability of behaviour and controlled use of resources. Actually, issues like unpredictability of external interactions and component availability, uncertainty in the information gathered, real time decisions on continuous behaviours, etc, entails the need for new variants of contracts and corresponding, underlying logics.

At the center of such a methodology is a dynamic logic (DL). As logics of programs, DLs offer a classical framework to reason about contracts in precise way. Over time, building on the pioneer intuitions of FloydHoare logic, they grew to an entire family of logics and became increasingly popular for assertional reasoning. Simultaneously, their object (i.e. the very notion of a program) evolved in unexpected ways. This leads to DLs tailored to specific programming paradigms and extended to new computing domains, either probabilistic, following the original work of D. Kozen [Koz85], continuous, with A. Platzer differential logic, and, more recently, of a quantum nature, with A. Baltag and S.Smets [BS12].

The contribution of DALÍ builds on the hypothesis that variants of DL can be generated through a systematic process, so that their models and proof theory (and, consequently, the corresponding tool support) can be characterised in a generic, parametric way, according to the specific requirements to be formalised. Differently from other approaches in the literature, ours is not to develop yet another DL (for CPS) but investigate a generic method to built DLs ondemand, i.e., parametric on the specific constraints of each application domain. Typical parameters will be a base logic for contracts’ specification (e.g. propositional, first order, probabilistic, etc.), and a specific algebraic structure to model the space of programs, as well as the corresponding domains of behaviours (e.g. Kleene algebras of probabilistic programs, continuous dynamics, energy consuming functions, etc.).

Such a method will guide the development of parametric calculi and modeltheoretical characterisations of broad classes of DLs, that can be further combined. A generic designbycontract development methodology will emerge from this setting. Suitable tool support will require the incorporation of new, dynamic structures suitable to deal with more complex nonlinear differential equations.

On the applications side, DALÍ will focus on the CPS domain from a double perspective. Firstly, it will introduce models and verification strategies for controllers used in industrial automation, fitting the international standard IEC 611313, largely adopted in industry. Contractbased verification of such controllers, explicitly integrating the corresponding (models of) physical components will provide a main testbed for the ideas and tools to be developed within the project. Secondly, a real casestudy on the “voltage regulator function” in industrial energy systems will be conduct. The case study is provided by EFACEC, a main Portuguese player in industrial automation.