V²CPS 2016

Abstract:
It is required of many cyber-physical systems that their run-time behavior be predictable prior to deployment. Due to cost and related considerations, there is an increasing trend towards implementing such systems using general-purpose (commercial off-the-shelf, or COTS) components; since COTS components are typically designed to ensure functional correctness, it is difficult to validate non-functional properties for systems built using such components. We will explore the challenges that arise in ensuring timing predictability for safety-critical systems that are implemented upon COTS platforms and that interact with uncertain environments, and discuss how the discipline of real-time scheduling is beginning to respond to these challenges by devising new models and methods for the design, analysis, and implementation of such safety-critical systems.

Abstract:
I discuss a new and formal, measurement-driven and model-based automated verification and synthesis technique, to be applied on quantitative properties over systems with partly unknown dynamics. I focus on physical systems (with spatially continuous variables, possibly noisy), driven by external inputs and accessed under noisy measurements, and suggest that the approach can be as well generalised over CPS. I formulate this new setup as a data-driven Bayesian model inference problem, formally embedded within a quantitative, model-based verification procedure.
While emphasising the generality of the approach over a number of diverse model classes, this talk zooms in on systems represented via stochastic hybrid models (SHS), which are probabilistic models with heterogeneous dynamics (continuous/discrete, i.e. hybrid, as well as nonlinear) - as such, SHS are quite a natural framework for CPS. With focus on model-based verification procedures, I provide the characterisation of general temporal specifications based on Bellman’s dynamic programming. The computation of such properties and the synthesis of related control architectures optimising properties of interest, is attained via the development of abstraction techniques based on quantitative approximations. This abstraction approach employs methods and concepts from the formal verification area, such as that of (approximate probabilistic) bisimulation, over models and problems known in the field of systems and control. Theory is complemented by algorithms, all packaged in a software tool (FAUST²) that is freely available to users.

Abstract:
We present an approach for synthesizing switched controllers for continuous-time plants, so that the resulting closed-loop system satisfies specifications expressed in temporal logic. Our approach uses a combination of control certificates such as control Lyapunov functions and control barriers. Such a certificate provides a controller switching strategy and associated property proof in one shot. However, the difficulty of our approach lies in synthesizing such certificates automatically from the given plant description and property specification. We present solutions to this synthesis problem by combining SMT solvers commonly used in program verification/synthesis applications with techniques for relaxing polynomial optimization problems commonly used in control literature. We illustrate our approach on a series of challenging benchmark problem instances.
Joint work with Hadi Ravanbakhsh, Amin Ben Sassi and Yuen-Lam Voronin.

Abstract:
In general, system testing and verification should be conducted with respect to formal specifications. However, the development of formal specifications is a challenging and error prone task, even for experts. In this work, we first present a framework for the elicitation and debugging of formal specifications. The elicitation of formal specifications is handled through a graphical user interface. The debugging algorithm checks inconsistent and wrong specifications. Namely, it detects validity, redundancy and vacuity issues in formal specifications developed in a fragment of Metric Interval Temporal Logic (MITL). The algorithm informs system engineers on any issues in their specifications. Thus, specification errors in the elicitation process can be corrected before any test and verification process is initiated. Second, we develop a framework that analyzes reactive requirements during the testing process and reports on the test cases which satisfy the requirements but do not reflect the intentions of the requirement engineers. Finally, we present experimental results on specifications that typically appear in Cyber-Physical Systems (CPS) applications.
The application of our specification debugging, and signal vacuity detection algorithms on user derived requirements shows that the aforementioned issues are common. Therefore, the framework can help the developers to correct their specifications and avoid wasted effort on checking incorrect requirements as well as finding more subtle errors during testing.

Abstract:
At the heart of an automobile is its powertrain, and the operation of powertrain components such as the engine is controlled by embedded software on electronic control units (ECUs). The paradigm of model-based development (MBD) has become the de facto standard for designing such control software. MBD designs of control software range from feature-level models to application-level and even entire system-level models. On the other hand, models of the plant (e.g. the engine), can range from simple physics-based models to high-fidelity models incorporating test-data. The advantage of MBD is in its ability to design, validate, and analyze the closed-loop model of the plant and the controller, often well before the actual hardware components become available. Unfortunately, even the simplest closed-loop model of an automotive powertrain subsystem is a complex cyber-physical system with highly nonlinear and hybrid dynamics, and reasoning about the correctness of such closed-loop models is a formidable task. In this talk, we introduce two challenges in reasoning about industrial-scale closed-loop control models: (1) scaling verification or bug-finding techniques to closed-loop engine control systems, and (2) formalisms to express correctness and performance requirements for such models. We survey some of the existing work done to answer these challenges, and present some promising directions for future work.