invited-talk

Formal verification of complex systems: model-based and data-driven methods

Author:

Alessandro AbateAuthors Info & Claims

MEMOCODE '17: Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design

Pages 91 - 93

https://doi.org/10.1145/3127041.3131362

Published: 29 September 2017 Publication History

Get Access

Abstract

Two known shortcomings of standard techniques in formal verification are the limited capability to provide system-level assertions, and the scalability to large, complex models, such as those needed in Cyber-Physical Systems (CPS) applications. Leveraging data, which nowadays is becoming ever more accessible, has the potential to mitigate such limitations. However, this leads to a lack of formal proofs that are needed for modern safety-critical systems.

This contribution presents a research initiative that addresses these shortcomings by bringing model-based techniques and data-driven methods together, which can help pushing the envelope of existing algorithms and tools in formal verification and thus expanding their applicability to complex engineering systems, such as CPS.

In the first part of the contribution, we discuss a new, formal, measurement-driven and model-based automated technique, for the quantitative verification of physical systems with partly unknown dynamics. We formulate this setup as a data-driven Bayesian inference problem, formally embedded within a quantitative, model-based verification procedure. We argue that the approach can be applied to complex physical systems that are key for CPS applications, dealing with spatially continuous variables, evolving under complex dynamics, driven by external inputs, and accessed under noisy measurements.

In the second part of the contribution, we concentrate on systems represented by models that evolve under probabilistic and heterogeneous (continuous/discrete - that is "hybrid" - as well as nonlinear) dynamics. Such stochastic hybrid models (also known as SHS) are a natural mathematical framework for CPS. With focus on model-based verification procedures, we provide algorithms for quantitative model checking of temporal specifications on SHS with formal guarantees. This is attained via the development of formal abstraction techniques that are based on quantitative approximations.

Theory is complemented by algorithms, all packaged in software tools that are available to users, and which are applied here in the domain of Smart Energy.

References

[1]

A. Abate, I. Bessa, D. Cattaruzza, L. Cordeiro, C. David, P. Kesseli, E. Polgreen, and D. Kroening, "Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants," CAV17, LNCS 10426, pp 462--482, 2017.

Abstract

References

Cited By

Recommendations

Formal verification of ASMs using MDGs

Model checking: recent improvements and applications

Formal Verification of Digital Systems

Comments

Information

Published In

Sponsors

Publisher

Publication History

Check for updates

Author Tags

Qualifiers

Conference

Acceptance Rates

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

Login options

Full Access

View options

PDF

eReader

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations