DaLí - Dynamic Logics for cyber-physical systems: towards contract based design

2nd DaLí workshop, submissions deadline - June 14, 2019

1st DaLí workshop

abstract

Contract-based 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 ad-hoc tweaking 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, 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 Floyd-Hoare 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, continuous, with A. Platzer differential logic, and, more recently, of a quantum nature, with A. Baltag and S.Smets.
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 build DLs on-demand, 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 model-theoretical characterisations of broad classes of DLs, that can be further combined. A generic design-by-contract 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.